Subsumer-First: Steering Symbolic Reachability Analysis

13 years 6 months ago
Subsumer-First: Steering Symbolic Reachability Analysis
Abstract. Symbolic reachability analysis provides a basis for the verification of software systems by offering algorithmic support for the exploration of the program state space when searching for proofs or counterexamples. The choice of exploration strategy employed by the analysis has direct impact on its success, whereas the ability to find short counterexamples quickly and—as a complementary task—to efficiently perform the exhaustive state space traversal are of utmost importance for the majority of verification efforts. Existing exploration strategies can optimize only one of these objectives which leads to a sub-optimal reachability analysis, e.g., breadth-first search may sacrifice the exploration efficiency and chaotic iteration can miss minimal counterexamples. In this paper we present subsumer-first, a new approach for steering symbolic reachability analysis that targets both minimal counterexample discovery and efficiency of exhaustive exploration. Our approach ...
Andrey Rybalchenko, Rishabh Singh
Added 27 May 2010
Updated 27 May 2010
Type Conference
Year 2009
Where SPIN
Authors Andrey Rybalchenko, Rishabh Singh
Comments (0)