Sciweavers

Share
DATE
2003
IEEE

Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis

9 years 3 months ago
Set Manipulation with Boolean Functional Vectors for Symbolic Reachability Analysis
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.
Amit Goel, Randal E. Bryant
Added 04 Jul 2010
Updated 04 Jul 2010
Type Conference
Year 2003
Where DATE
Authors Amit Goel, Randal E. Bryant
Comments (0)
books