Abstract
The automated inference of quantified invariants is considered one of the next challenges in software verification. The question of the right precision-efficiency tradeoff for the corresponding program analyses here boils down to the question of the right treatment of disjunction below and above the universal quantifier. In the closely related setting of shape analysis one uses the focus operator in order to adapt the treatment of disjunction (and thus the efficiency-precision tradeoff) to the individual program statement. One promising research direction is to design parameterized versions of the focus operator which allow the user to fine-tune the focus operator not only to the individual program statements but also to the specific verification task. We carry this research direction one step further. We fine-tune the focus operator to each individual step of the analysis (for a specific verification task). This fine-tuning must be done automatically. Our idea is to use counterexamples for this purpose. We realize this idea in a tool that automatically infers quantified invariants for the verification of a variety of heap-manipulating programs.
- T. Ball, B. Cook, S. Das, and S.K. Rajamani. Refining approximations in software predicate abstraction. In TACAS'04, pages 388--403, 2004.Google ScholarCross Ref
- T. Ball, A. Podelski, and S.K. Rajamani. Boolean and Cartesian abstraction for model checking C programs. In TACAS'01, pages 268--283, 2001. Google ScholarDigital Library
- T. Ball and S.K. Rajamani. The SLAM project: debugging system software via static analysis. In POPL'02, pages 1--3, 2002. Google ScholarDigital Library
- J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. O'Hearn, T. Wies, and H. Yang. Shape analysis for composite data structures. In CAV'07, pages 178--192, 2007. Google ScholarDigital Library
- D. Beyer, T.A. Henzinger, R. Majumdar, and A. Rybalchenko. Path invariants. In PLDI, pages 300--309, 2007. Google ScholarDigital Library
- D. Beyer, T.A. Henzinger, and G. Théoduloz. Lazy shape analysis. In CAV'06, pages 532--546, 2006. Google ScholarDigital Library
- J.D. Bingham and Z. Rakamaric. A logic and decision procedure for predicate abstraction of heap-manipulating programs. In VMCAI'06, pages 207--221, 2006. Google ScholarDigital Library
- I. Bogudlov, T. Lev-Ami, T.W. Reps, and M. Sagiv. Revamping TVLA: Making Parametric Shape Analysis Competitive. In CAV'07, pages 221--225, 2007. Google ScholarDigital Library
- A. Bouajjani, P. Habermehl, A. Rogalewicz, and T. Vojnar. Abstract regular tree model checking. ENTCS, 149(1):37--48, 2006. Google ScholarDigital Library
- A. Bouajjani, P. Habermehl, A. Rogalewicz, and T. Vojnar. Abstract regular tree model checking of complex dynamic data structures. In SAS'06, pages 52--70, 2006. Google ScholarDigital Library
- R.E. Bryant. Graph-Based Algorithms for Boolean Function Manipulation. TC, 35(10):677--691, 1986. Google ScholarDigital Library
- S. Chaki, E.M. Clarke, A. Groce, S. Jha, and H. Veith. Modular verification of software components in C. In ICSE'03, pages 385--395, 2003. Google ScholarDigital Library
- B.-Y.E. Chang, X. Rival, and G.C. Necula. Shape analysis with structural invariant checkers. In SAS'07, pages 384--401, 2007. 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, 2000. Google ScholarDigital Library
- P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In POPL'77, pages 238--252, 1977. Google ScholarDigital Library
- P. Cousot and R. Cousot. Formal language, grammar and set-constraint-based program analysis by abstract interpretation. In FPCA'95, pages 170--181, 1995. Google ScholarDigital Library
- S. Das and D.L. Dill. Successive approximation of abstract transition relations. In LICS'01, pages 51--60, 2001. Google ScholarDigital Library
- L. de Moura and N. Bjørner. Z3: An Efficient SMT Solver. In TACAS'08, 2008. Google ScholarDigital Library
- D. Distefano, P. O'Hearn, and H. Yang. A local shape analysis based on separation logic. In TACAS'06, pages 287--302, 2006. Google ScholarDigital Library
- C. Flanagan and S. Qadeer. Predicate abstraction for software verification. In POPL'02, pages 191--202, 2002. Google ScholarDigital Library
- D. Gopan, T.W. Reps, and S. Sagiv. A framework for numeric analysis of array operations. In POPL'05, pages 338--350, 2005. Google ScholarDigital Library
- S. Graf and H. Saïdi. Construction of Abstract State Graphs with PVS. In CAV'97, pages 72--83, 1997. Google ScholarDigital Library
- S. Gulwani, B. McCloskey, and A. Tiwari. Lifting abstract interpreters to quantified logical domains. In POPL'08, pages 235--246, 2008. Google ScholarDigital Library
- B. Guo, N. Vachharajani, and D.I. August. Shape analysis with inductive recursion synthesis. In PLDI'07, pages 256--265, 2007. Google ScholarDigital Library
- T.A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy Abstraction. In POPL'02, pages 58--70, 2002. Google ScholarDigital Library
- T.A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Software verification with Blast. In SPIN 03: Model Checking of Software, pages 235--239. 2003. Google ScholarDigital Library
- R. Jhala and K.L. McMillan. Array abstractions from proofs. In CAV'07, pages 193--206, 2007. Google ScholarDigital Library
- N. Klarlund and A. Møller. MONA Version 1.4 User Manual. BRICS Notes Series NS-01-1, University of Aarhus, January 2001.Google Scholar
- L. Kovacs and A. Voronkov. Finding loop invariants for programs over arrays using a theorem prover. In FASE'09, pages 470--485, 2009. Google ScholarDigital Library
- V. Kuncak. Modular Data Structure Verification. PhD thesis, EECS Department, Massachusetts Institute of Technology, February 2007. Google ScholarDigital Library
- S.K. Lahiri and R.E. Bryant. Constructing quantified invariants via predicate abstraction. In VMCAI'04, pages 267--281, 2004.Google ScholarCross Ref
- S.K. Lahiri and R.E. Bryant. Indexed predicate discovery for unbounded system verification. In CAV'04, 2004.Google ScholarCross Ref
- S.K. Lahiri and S. Qadeer. Back to the future: revisiting precise program verification using SMT solvers. In POPL'08, pages 171--182, 2008. Google ScholarDigital Library
- P. Lam, V. Kuncak, and M. Rinard. Hob: A tool for verifying data structure consistency. In CC'05, 2005. Google ScholarDigital Library
- T. Lev-Ami. TVLA: A Framework for Kleene Based Logic Static Analyses. Master's thesis, Tel-Aviv University, Israel, 2000.Google Scholar
- T. Lev-Ami, N. Immerman, and M. Sagiv. Abstraction for shape analysis with fast and precise transformers. In CAV'06, pages 533--546, 2006. Google ScholarDigital Library
- A. Loginov, T. Reps, and M. Sagiv. Abstraction refinement via inductive learning. In CAV'05, 2005. Google ScholarDigital Library
- S. Magill, J. Berdine, E.M. Clarke, and B. Cook. Arithmetic strengthening for shape analysis. In SAS'07, pages 419--436, 2007. Google ScholarDigital Library
- R. Manevich. Partially Disjunctive Shape Analysis. PhD thesis, Tel-Aviv University, Israel, 2009.Google Scholar
- R. Manevich, J. Berdine, B. Cook, G. Ramalingam, and M. Sagiv. Shape analysis by graph decomposition. In TACAS'07, pages 3--18, 2007. Google ScholarDigital Library
- R. Manevich, M. Sagiv, G. Ramalingam, and J. Field. Partially disjunctive heap abstraction. In SAS'04, pages 265--279, 2004.Google ScholarCross Ref
- M. Marron, D. Kapur, D. Stefanovic, and M.V. Hermenegildo. A static heap analysis for shape and connectivity. In LCPC, pages 345--363, 2006. Google ScholarDigital Library
- K.L. McMillan. Quantified invariant generation using an interpolating saturation prover. In TACAS'08, volume 4963, pages 413--427, 2008. 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, 2007. Google ScholarDigital Library
- A. Podelski and T. Wies. Boolean Heaps. In SAS'05, pages 267--282, 2005. Google ScholarDigital Library
- T. Reps, M. Sagiv, and A. Loginov. Finite differencing of logical formulas for static analysis. In ESOP'03, pages 380--398, 2003. Google ScholarDigital Library
- N. Rinetzky, A. Poetzsch-Heffter, G. Ramalingam, M. Sagiv, and E. Yahav. Modular shape analysis for dynamically encapsulated programs. In ESOP'07, pages 220--236, 2007. Google ScholarDigital Library
- M. Sagiv, T. Reps, and R. Wilhelm. Parametric shape analysis via 3-valued logic. TOPLAS, 24(3):217--298, 2002. Google ScholarDigital Library
- M.N. Seghir, A. Podelski, and T. Wies. Abstraction refinement for quantified array assertions. In SAS'09, 2009. Google ScholarDigital Library
- S. Srivastava and S. Gulwani. Program verification using templates over predicate abstraction. In PLDI'09, 2009. Google ScholarDigital Library
- T. Wies. Symbolic Shape Analysis. PhD thesis, University of Freiburg, Freiburg, Germany, 2009.Google Scholar
- T. Wies, V. Kuncak, P. Lam, A. Podelski, and M. Rinard. Field Constraint Analysis. In VMCAI'06, 2006. Google ScholarDigital Library
- H. Yang, O. Lee, J. Berdine, C. Calcagno, B. Cook, D. Distefano, and P.W. O'Hearn. Scalable shape analysis for systems code. In CAV'08, pages 385--398, 2008. Google ScholarDigital Library
- G. Yorsh, A.M. Rabinovich, M. Sagiv, A. Meyer, and A. Bouajjani. A Logic of Reachable Patterns in Linked Data-Structures. In FOSSACS'06, pages 94--110, 2006. Google ScholarDigital Library
- G. Yorsh, T. Reps, and M. Sagiv. Symbolically computing most-precise abstract operations for shape analysis. In TACAS'04, 2004.Google ScholarCross Ref
- K. Zee, V. Kuncak, and M. Rinard. Full Functional Verification for Linked Data Structures. In PLDI'08, pages 349--361, 2008. Google ScholarDigital Library
- K. Zee, V. Kuncak, and M.C. Rinard. An integrated proof language for imperative programs. In PLDI'09, pages 338--351, 2009. Google ScholarDigital Library
Index Terms
- Counterexample-guided focus
Recommendations
Counterexample-guided focus
POPL '10: Proceedings of the 37th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languagesThe automated inference of quantified invariants is considered one of the next challenges in software verification. The question of the right precision-efficiency tradeoff for the corresponding program analyses here boils down to the question of the ...
Efficient Verification of Sequential and Concurrent C Programs
There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. ...
Counterexample-guided predicate abstraction of hybrid systems
Tools and algorithms for the construction and analysis of systems (TACAS 2003)Predicate abstraction has emerged to be a powerful technique for extracting finite-state models from infinite-state systems, and has been recently shown to enhance the effectiveness of the teachability computation techniques for hybrid systems. Given a ...
Comments