Paper Info
Title
Intertwined forward-backward reachability analysis using interpolants
Abstract
In this work we develop a novel SAT-based verification approach which is based on interpolation. The novelty of our approach is in extracting interpolants in both forward and backward manner and exploiting them for an intertwined approximated forward and backward reachability analysis. Our approach is also mostly local and avoids unrolling of the checked model as much as possible. This results in an efficient and complete SAT-based verification algorithm. We implemented our algorithm and compared it with both McMillan's interpolation-based algorithm and with IC3, on real-life industrial designs as well as on examples from the HWMCC'11 benchmark. In many cases, our algorithm outperformed both methods.
Year
DOI
Venue
2013
10.1007/978-3-642-36742-7_22
TACAS
Keywords
Field
DocType
reachability analysis,novel sat-based verification approach,real-life industrial design,complete sat-based verification algorithm,interpolation-based algorithm,intertwined forward-backward reachability analysis
Discrete mathematics,Computer science,Interpolation,Algorithm,Theoretical computer science,Reachability,Novelty,Propositional formula,Safety property
Conference
Volume
ISSN
Citations 
7795
0302-9743
9
PageRank 
References 
Authors
0.58
12
3
Name
Order
Citations
PageRank
Yakir Vizel1858.79
Orna Grumberg24361351.99
Sharon Shoham334226.67