Intertwined forward-backward reachability analysis using interpolants
作者： Yakir Vizel , Orna Grumberg , Sharon Shoham
DOI: 10.1007/978-3-642-36742-7_22
关键词:
摘要: In this work we develop a novel SAT-based verification approach which is based on interpolation. The novelty of our in extracting interpolants both forward and backward manner exploiting them for an intertwined approximated reachability analysis. Our also mostly local avoids unrolling the checked model as much possible. This results efficient complete algorithm. We implemented algorithm compared it with McMillan's interpolation-based IC3, real-life industrial designs well examples from HWMCC'11 benchmark. many cases, outperformed methods.
springer.com
sci-hub.st 参考文章(20)
K. Etessami, Analysis of Recursive Game Graphs Using Data Flow Equations verification model checking and abstract interpretation. pp. 282- 296 ,(2004) , 10.1007/978-3-540-24622-0_23
K. L. McMillan, Interpolation and SAT-Based Model Checking computer aided verification. pp. 1- 13 ,(2003) , 10.1007/978-3-540-45069-6_1
Christian Stangier, Thomas Sidle, Invariant Checking Combining Forward and Backward Traversal formal methods in computer aided design. pp. 414- 429 ,(2004) , 10.1007/978-3-540-30494-4_29
Orna Grumberg, Sharon Shoham, Yakir Vizel, Lazy abstraction and SAT-based reachability in hardware model checking formal methods in computer-aided design. pp. 173- 181 ,(2012)
Aaron R. Bradley, SAT-based model checking without unrolling verification, model checking and abstract interpretation. pp. 70- 87 ,(2011) , 10.5555/1946284.1946291
Gianpiero Cabodi, Sergio Nocco, Stefano Quer, Mixing Forward and Backward Traversals in Guided-Prioritized BDD-Based Verification computer aided verification. pp. 471- 484 ,(2002) , 10.1007/3-540-45657-0_38
Vijay D’Silva, Mitra Purandare, Daniel Kroening, Approximation Refinement for Interpolation-Based Model Checking Lecture Notes in Computer Science. ,vol. 4905, pp. 68- 82 ,(2008) , 10.1007/978-3-540-78163-9_10
Gianpiero Cabodi, Marco Murciano, Sergio Nocco, Stefano Quer, Stepping forward with interpolants in unbounded model checking international conference on computer aided design. pp. 772- 778 ,(2006) , 10.1145/1233501.1233661
William Craig, Linear reasoning. A new form of the Herbrand-Gentzen theorem Journal of Symbolic Logic. ,vol. 22, pp. 250- 268 ,(1957) , 10.2307/2963593
Alan Mishchenko, Robert Brayton, Niklas Een, Efficient implementation of property directed reachability formal methods in computer-aided design. pp. 125- 134 ,(2011) , 10.5555/2157654.2157675