Matthias Heizmann
Andreas Podelski
ABSTRACT
In this paper, we explore the potential of the theory of nested words for partial correctness proofs of recursive programs. Our conceptual contribution is a simple framework that allows us to shine a new light on classical concepts such as Floyd/Hoare proofs and predicate abstraction in the context of recursive programs. Our technical contribution is an interpolant-based software model checking method for recursive programs. The method avoids the costly construction of the abstract transformer by constructing a nested word automaton from an inductive sequence of `nested interpolants' (i.e., interpolants for a nested word which represents an infeasible error trace).
- R. Alur, K. Etessami, and P. Madhusudan. A temporal logic of nested calls and returns. In TACAS '04, pages 467--481. Springer, 2004.Google Scholar
Cross Ref
- R. Alur and P. Madhusudan. Adding nesting structure to words. In DLT '06, pages 1--13. Springer, 2006. Google ScholarDigital Library
- R. Alur and P. Madhusudan. Adding nesting structure to words. JACM, 56(3), 2009. Google ScholarDigital Library
- K.-R. Apt, F. de Boer, and E.-R. Olderog. Verification of Sequential and Concurrent Programs. Third, extended edition. Springer, 2009. Google ScholarDigital Library
- T. Ball and S. K. Rajamani. The SLAM project: debugging system software via static analysis. In POPL '02, pages 1--3. ACM, 2002. Google ScholarDigital Library
- M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In FMCO '05, pages 364--387. Springer, 2005. Google ScholarDigital Library
- N. Beckman, A. V. Nori, S. K. Rajamani, and R. J. Simmons. Proofs from tests. In ISSTA '08, pages 3--14. ACM, 2008. Google ScholarDigital Library
- I. Brückner, K. Dräger, B. Finkbeiner, and H. Wehrheim. Slicing abstractions. In FSEN '07, pages 17--32. Springer, 2007. Google ScholarDigital Library
- S. Chaki, E. M. Clarke, A. Groce, S. Jha, and H. Veith. Modular verification of software components in C. IEEE Trans. Software Eng., 30(6):388--402, 2004. Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV '00, pages 154--169. Springer, 2000. Google ScholarDigital Library
- J. Esparza, S. Kiefer, and S. Schwoon. Abstraction refinement with Craig interpolation and symbolic pushdown systems. JSAT, 5:27--56, June 2008. Special Issue on Constraints to Formal Verification.Google Scholar
- B. S. Gulavani, S. Chakraborty, A. V. Nori, and S. K. Rajamani. Automatically refining abstract interpretations. In TACAS '08, pages 443--458. Springer, 2008. Google ScholarDigital Library
- M. Heizmann, J. Hoenicke, and A. Podelski. Refinement of trace abstraction. In SAS '09, pages 69--85. Springer, 2009. Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In POPL '04, pages 232--244. ACM, 2004. Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL '02, pages 58--70. ACM, 2002. Google ScholarDigital Library
- F. Ivancic, I. Shlyakhter, A. Gupta, and M. K. Ganai. Model checking C programs using F-SOFT. In ICCD '05, pages 297--308. IEEE Computer Society, 2005. Google ScholarDigital Library
- R. Jhala and K. L. McMillan. Interpolant-based transition relation approximation. In CAV '05, pages 39--51. Springer, 2005. Google ScholarDigital Library
- R. Jhala and K. L. McMillan. A practical and complete approach to predicate refinement. In TACAS '06, pages 459--473. Springer, 2006. Google ScholarDigital Library
- K. L. McMillan. Lazy abstraction with interpolants. In CAV '06, pages 123--136. Springer, 2006. Google ScholarDigital Library
- A. Podelski and A. Rybalchenko. ARMC: The logical choice for software model checking with abstraction refinement. In PADL '07, pages 245--259. Springer, 2007. Google ScholarDigital Library
- T. W. Reps, S. Horwitz, and S. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL '95, pages 49--61. ACM, 1995. Google ScholarDigital Library
Index Terms
- Nested interpolants
Recommendations
Nested interpolants
POPL '10In this paper, we explore the potential of the theory of nested words for partial correctness proofs of recursive programs. Our conceptual contribution is a simple framework that allows us to shine a new light on classical concepts such as Floyd/Hoare ...
Path invariants
PLDI '07: Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and ImplementationThe success of software verification depends on the ability to find a suitable abstraction of a program automatically. We propose a method for automated abstraction refinement which overcomes some limitations of current predicate discovery schemes. In ...
Data-abstraction refinement: a game semantic approach
This paper presents a semantic framework for data abstraction and refinement for verifying safety properties of open programs with integer types. The presentation is focused on an Algol-like programming language that incorporates data abstraction in its ...
Comments