loading...
Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis
Munich, Germany March 03-March 07
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/DATE.2003.10123Design, Automation and Test in Europe ...
 This Article 
 
PDF
HTML
IEEE Xplore Subscribers
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Amit Goel, Carnegie Mellon University
Randal E. Bryant, Carnegie Mellon University
Symbolic techniques usually use characteristic functions for representing sets of states. Boolean functional vectors provide an alternate set representation which is suitable for symbolic simulation. Their use in symbolic reachability analysis and model checking is limited, however, by the lack of algorithms for performing set operations. We present algorithms for set union, intersection and quantification that work with a canonical Boolean functional vector representation and show how this enables efficient symbolic simulation based reachability analysis. Our experimental results for reachability analysis indicate that the Boolean functional vector representation is often more compact than the corresponding characteristic function, thus giving significant performance improvements on some benchmarks.
Citation:
Amit Goel, Randal E. Bryant, "Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis," date, vol. 1, pp.10816, Design, Automation and Test in Europe Conference and Exhibition (DATE'03), 2003
Usage of this product signifies your acceptance of the Terms of Use.