ABSTRACT
Automatically generated tools can significantly improve programmer productivity. For example, parsers and dataflow analyzers can be automatically generated from declarative specifications in the form of grammars, which tremendously simplifies the task of implementing a compiler. In this paper, we present a method for the automatic synthesis of software verification tools. Our synthesis procedure takes as input a description of the employed proof rule, e.g., program safety checking via inductive invariants, and produces a tool that automatically discovers the auxiliary assertions required by the proof rule, e.g., inductive loop invariants and procedure summaries. We rely on a (standard) representation of proof rules using recursive equations over the auxiliary assertions. The discovery of auxiliary assertions, i.e., solving the equations, is based on an iterative process that extrapolates solutions obtained for finitary unrollings of equations. We show how our method synthesizes automatic safety and liveness verifiers for programs with procedures, multi-threaded programs, and functional programs. Our experimental comparison of the resulting verifiers with existing state-of-the-art verification tools confirms the practicality of the approach.
- A. V. Aho, M. S. Lam, R. Sethi, and J. D. Ullman. Compilers: Principles, Techniques, and Tools. Pearson, 2006. Google ScholarDigital Library
- A. Aiken. Introduction to set constraint-based program analysis. Sci. Comput. Program., 35 (2), 1999. Google ScholarDigital Library
- A. Aiken, M. Fähndrich, J. S. Foster, and Z. Su. A toolkit for constructing type- and constraint-based program analyses. In Types in Compilation, 1998. Google ScholarDigital Library
- T. Ball and S. K. Rajamani. The SLAM project: debugging system software via static analysis. In POPL, 2002. Google ScholarDigital Library
- T. Ball, A. Podelski, and S. K. Rajamani. Boolean and cartesian abstraction for model checking C programs. In TACAS, 2001. Google ScholarDigital Library
- D. Beyer. Competition on software verification - (SV-COMP). In TACAS, 2012. Google ScholarDigital Library
- D. Beyer and M. E. Keremoglu. CPAchecker: A tool for configurable software verification. In CAV, 2011. Google ScholarDigital Library
- A. R. Bradley, Z. Manna, and H. B. Sipma. Linear ranking with reachability. In CAV, 2005. Google ScholarDigital Library
- R. Bruttomesso, A. Cimatti, A. Franzén, A. Griggio, and R. Sebastiani. The MathSAT 4SMT solver. In CAV, 2008. Google ScholarDigital Library
- E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV, 2000. Google ScholarDigital Library
- B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for systems code. In PLDI, 2006. Google ScholarDigital Library
- B. Cook, A. Podelski, and A. Rybalchenko. Summarization for termination: no return! Formal Methods in System Design, 35 (3), 2009. Google ScholarDigital Library
- C. Flanagan and S. Qadeer. Thread-modular model checking. In SPIN, 2003. Google ScholarDigital Library
- T. Freeman and F. Pfenning. Refinement types for ML. In PLDI, 1991. Google ScholarDigital Library
- S. Graf and H. Saïdi. Construction of abstract state graphs with PVS. In CAV, 1997. Google ScholarDigital Library
- S. Grebenshchikov, A. Gupta, N. P. Lopes, C. Popeea, and A. Rybalchenko. HSF(C): A software verifier based on Horn clauses - (competition contribution). In TACAS, 2012. Google ScholarDigital Library
- A. Gupta, C. Popeea, and A. Rybalchenko. Solving recursion-free horn clauses over LIUIF. In APLAS, 2011 Google ScholarDigital Library
- A. Gupta, C. Popeea, and A. Rybalchenko. Threader: A constraint-based verifier for multi-threaded programs. In CAV, 2011. Google ScholarDigital Library
- A. Gupta, C. Popeea, and A. Rybalchenko. Predicate abstraction and refinement for verifying multi-threaded programs. In POPL, 2011. Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL, 2002. Google ScholarDigital Library
- T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In POPL, 2004. Google ScholarDigital Library
- K. Hoder, N. Bjørner, and L. de Moura. μZ- an efficient engine for fixed points with constraints. In CAV, 2011. Google ScholarDigital Library
- F. Ivancic, Z. Yang, M. K. Ganai, A. Gupta, I. Shlyakhter, and P. Ashar. F-Soft: Software verification platform. In CAV, 2005. Google ScholarDigital Library
- R. Jhala, R. Majumdar, and A. Rybalchenko. HMC: Verifying functional programs using abstract interpreters. In CAV, 2011. Google ScholarDigital Library
- C. B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst., 5 (4), 1983. Google ScholarDigital Library
- K. W. Knowles and C. Flanagan. Type reconstruction for general refinement types. In ESOP, 2007. Google ScholarDigital Library
- J. Kodumal and A. Aiken. Banshee: A scalable constraint-based analysis toolkit. In SAS, 2005. Google ScholarDigital Library
- M. S. Lam, J. Whaley, V. B. Livshits, M. C. Martin, D. Avots, M. Carbin, and C. Unkel. Context-sensitive program analysis as database queries. In PODS, 2005. Google ScholarDigital Library
- S. Lerner, T. D. Millstein, E. Rice, and C. Chambers. Automated soundness proofs for dataflow analyses and transformations via local rules. In POPL, 2005. Google ScholarDigital Library
- Z. Manna and A. Pnueli. Temporal verification of reactive systems: safety. 1995. Google ScholarCross Ref
- F. Martin. PAG -- An efficient program analyzer generator. STTT, 2 (1), 1998.Google Scholar
- K. L. McMillan. An interpolating theorem prover. TCS, 2005. Google ScholarDigital Library
- K. L. McMillan. Lazy abstraction with interpolants. In CAV, 2006. Google ScholarDigital Library
- M. Naik, A. Aiken, and J. Whaley. Effective static race detection for Java. In PLDI, 2006. Google ScholarDigital Library
- G. C. Necula, S. McPeak, S. P. Rahul, and W. Weimer. CIL: Intermediate language and tools for analysis and transformation of C programs. In CC, 2002. Google ScholarDigital Library
- S. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Inf., 6, 1976.Google Scholar
- A. Podelski and A. Rybalchenko. Transition invariants. In LICS, 2004. Google ScholarDigital Library
- A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In VMCAI, 2004.Google ScholarCross Ref
- C. Popeea and A. Rybalchenko. Compositional termination proofs for multi-threaded programs. In TACAS, 2012. Google ScholarDigital Library
- W. H. Press, B. P. Flannery, S. A. Teukolsky, and W. T. Vetterling. Numerical Recipes in C: The Art of Scientific Computing. 1992. Google ScholarDigital Library
- Y. S. Ramakrishna, C. R. Ramakrishnan, I. V. Ramakrishnan, S. A. Smolka, T. Swift, and D. S. Warren. Efficient model checking using tabled resolution. In CAV, 1997. Google ScholarDigital Library
- T. W. Reps, S. Horwitz, and S. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL, 1995. Google ScholarDigital Library
- P. M. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI, 2008. Google ScholarDigital Library
- G. Rosu and A. Stefanescu. Matching logic: a new program verification approach. In ICSE, 2011.Google ScholarDigital Library
- T. Rus, E. V. Wyk, and T. Halverson. Generating model checkers from algebraic specifications. Formal Methods in System Design, 20 (3), 2002. Google ScholarDigital Library
- A. Rybalchenko and V. Sofronie-Stokkermans. Constraint solving for interpolation. In VMCAI, 2007. Google ScholarDigital Library
- M. Sagiv. High Level Formalisms for Program Flow Analysis and their use in Compiling. PhD thesis, Technion, 1991.Google Scholar
- T. Terauchi. Dependent types from counterexamples. In POPL, 2010. Google ScholarDigital Library
- S. L. Torre, P. Madhusudan, and G. Parlato. Analyzing recursive programs using a fixed-point calculus. In PLDI, 2009. Google ScholarDigital Library
- H. Unno and N. Kobayashi. Dependent type inference with interpolants. In PPDP, 2009. Google ScholarDigital Library
- J. Whaley and M. S. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In PLDI, 2004. Google ScholarDigital Library
Index Terms
- Synthesizing software verifiers from proof rules
Recommendations
Synthesizing software verifiers from proof rules
PLDI '12Automatically generated tools can significantly improve programmer productivity. For example, parsers and dataflow analyzers can be automatically generated from declarative specifications in the form of grammars, which tremendously simplifies the task ...
Cooperation Between Automatic and Interactive Software Verifiers
Software Engineering and Formal MethodsAbstractThe verification community develops two kinds of verification tools: automatic verifiers and interactive verifiers. There are many such verifiers available, and there is steady progress in research. However, cooperation between the two kinds of ...
Verifying B proof rules using deep embedding and automated theorem proving
We propose a formal and mechanized framework which consists in verifying proof rules of the B method, which cannot be automatically proved by the elementary prover of Atelier B and using an external automated theorem prover called Zenon. This framework ...
Comments