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 ...

• Type: Conference
• Year: 2009
• Where: SPIN
• Authors: Andrey Rybalchenko, Rishabh Singh
• Keywords: Exploration, Reachability Analysis, SPIN 2009, Symbolic Reachability Analysis, Theoretical Computer Science