Abstraction Refinement for Termination
作者： Byron Cook , Andreas Podelski , Andrey Rybalchenko
DOI: 10.1007/11547662_8
关键词: Abstraction model checking 、 Abstraction inversion 、 Abstraction 、 Computer science 、 Theoretical computer science 、 Mathematical proof 、 Liveness 、 Counterexample 、 Abstract interpretation 、 Predicate abstraction
摘要: Abstraction can often lead to spurious counterexamples. Counterexample-guided abstraction refinement is a method of strengthening abstractions based on the analysis these For invariance properties, counterexample finite trace that violates invariant; it if possible in but not original system. When proving termination or other liveness properties infinite-state systems, useful notion counterexamples has remained an open problem. this reason, no counterexample-guided algorithm was known for termination. In paper, we address problem and present first automatic proofs. We exploit recent results transition invariants predicate abstraction. identify two reasons spuriousness: are too coarse, candidate strong. Our successively weakens refines
springer.com
mpg.de
core.ac.uk
avacs.org 参考文章(33)
Zohar Manna, Amir Pnueli, Temporal Verification of Reactive Systems Springer New York. ,(1995) , 10.1007/978-1-4612-4222-2
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
Robin Milner, Bigraphical Reactive Systems international conference on concurrency theory. pp. 16- 35 ,(2001) , 10.1007/3-540-44685-0_2
Jens Palsberg, Andrey Rybalchenko, Martín Abadi, Andreas Podelski, Transition predicate abstraction and fair termination Untitled Event. pp. 124- 139 ,(2005)
Michael A. Colóon, Henny B. Sipma, Synthesis of Linear Ranking Functions tools and algorithms for construction and analysis of systems. pp. 67- 81 ,(2001) , 10.1007/3-540-45319-9_6
Y. Lakhnech, S. Bensalem, S. Berezin, S. Owre, Incremental Verification by Abstraction tools and algorithms for construction and analysis of systems. pp. 98- 112 ,(2001) , 10.1007/3-540-45319-9_8
Andreas Podelski, Andrey Rybalchenko, A Complete Method for the Synthesis of Linear Ranking Functions verification model checking and abstract interpretation. pp. 239- 251 ,(2004) , 10.1007/978-3-540-24622-0_20
Andreas Podelski, Ina Schaefer, Mooly Sagiv, Silke Wagner, Summaries for While Programs with Recursion Untitled Event. pp. 94- 107 ,(2005)
Zohar Manna, Amir Pnueli, Temporal Verification of Reactive Systems: Safety ,(1995)
Aaron R. Bradley, Zohar Manna, Henny B. Sipma, Termination of Polynomial Programs Lecture Notes in Computer Science. pp. 113- 129 ,(2005) , 10.1007/978-3-540-30579-8_8