## AI helps you reading Science

## AI Insight

AI extracts a summary of this paper

Weibo:

# Synthesizing software verifiers from proof rules

PLDI, no. 6 (2012): 405-416

EI

Keywords

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 synthes...More

Code:

Data:

Introduction

- Developing tools that deal with programs, e.g., parsers, compilers, analyzers, or verifiers, is a difficult yet necessary task for increasing programmer productivity.
- Static analyzers can be generated from attribute grammars [47], dataflow equations [29, 31], equations in the form of set constraints [2, 3, 27], or equations as Datalog rules [28, 34, 51]
- These approaches take an analysis specification as a set of equations and produce an analyzer that infers program properties by solving the equations

Highlights

- Developing tools that deal with programs, e.g., parsers, compilers, analyzers, or verifiers, is a difficult yet necessary task for increasing programmer productivity
- Copyright c 2012 ACM 978-1-4503-1205-9/12/06. . . 10.00 tool generator is developed for a given problem domain, it can be used to synthesize various tools that deal with particular problem instances in the given domain
- For the first three categories of benchmarks (Numerical Recipes, ntdrivers and ssh-simplified), we used HSF with the summarization proof rule described in Section 2
- We presented a logical step towards the automatic generation of software verification tools
- Our verifier generator takes as input a proof rule written as Horn-like clauses and produces a verifier that automates the proof rule
- The experimental evaluation shows that automatically generated verifiers are competitive with existing state-of-the-art verification tools that are manually developed and tuned

Methods

- The authors present an experimental comparison between verifiers developed using the HSF algorithm and state-of-the-art verification tools developed using traditional methods.

The authors' tool HSF is implemented in Prolog and compiled with the SICStus Prolog 4.2.0 compiler. - The authors present an experimental comparison between verifiers developed using the HSF algorithm and state-of-the-art verification tools developed using traditional methods.
- The authors' tool HSF is implemented in Prolog and compiled with the SICStus Prolog 4.2.0 compiler.
- For C programs, the authors use the CIL library [35] and an additional frontend step that produces clauses for various proof rules.
- For verifying OCaml programs, the authors use DSolve [43] to generate automatically subtyping constraints and the code translates these constraints to Hornlike clauses.

Results

- The authors' experiments were run on an Intel Core 2 Duo machine, clocked at 3.0 GHz, with 4 GB of RAM, and running Linux 2.6.38.
- For the first three categories of benchmarks (Numerical Recipes, ntdrivers and ssh-simplified), the authors used HSF with the summarization proof rule described in Section 2.
- The authors used BLAST 2.5 with the MathSat solver [9] and the following standard options: -craig 2 -dfs -predH 7 -nosimplemem -alias "", as suggested by the tool’s authors.
- The use of the MathSat solver led to Blast failing all the Numerical Recipes benchmarks, so instead the authors report statistics using the latest publicly available version of Blast that uses the Simplify solver.
- For CPAchecker, the authors used the revision r3842 from the tool repository and used the predicate abstraction with large block encoding configuration as suggested by the tool’s authors

Conclusion

- The authors presented a logical step towards the automatic generation of software verification tools.
- The authors' verifier generator takes as input a proof rule written as Horn-like clauses and produces a verifier that automates the proof rule.
- The experimental evaluation shows that automatically generated verifiers are competitive with existing state-of-the-art verification tools that are manually developed and tuned

- Table1: Timings for the benchmarks. The left-side of the page shows statistics for sequential programs, with multi-threaded programs, functional programs and terminating loops on the right-side of the page. “T/O” stands for time out after 10 minutes, while “FAIL” indicates that the tool failed to return a verification result

Related work

- Section 1 points to existing approaches to generate various analyses based on dataflow domains that led to powerful program analysis frameworks [3, 27,28,29, 31, 34, 47, 51].

Verifiers have also been a target for automated tool construction. XSB [41] is a programmable fixed-point engine used for implementing model checkers for a concurrent language based on CCS with properties specified in a fragment of mu-calculus. Model checkers have been generated from algebraic specifications of a source language and various fragments of temporal logic [45]. More recently, verifier generators have been developed for Boolean programs (GETAFIX [49]) and programs for which Datalog style bottom up inference terminates (μZ [22]). For programs with unbounded data domains, MatchC [44] provides a verifier based on matching logic specifications that directly build upon the operational semantics of the source language. The verification is facilitated by (pattern) loop invariants provided by the programmer. In comparison, our approach adds an abstraction refinement loop, which is crucial for handling unbounded datatypes, and allows automation of proof rules for termination and liveness properties.

Reference

- A. V. Aho, M. S. Lam, R. Sethi, and J. D. Ullman. Compilers: Principles, Techniques, and Tools. Pearson, 2006.
- A. Aiken. Introduction to set constraint-based program analysis. Sci. Comput. Program., 35(2), 1999.
- A. Aiken, M. Fahndrich, J. S. Foster, and Z. Su. A toolkit for constructing type- and constraint-based program analyses. In Types in Compilation, 1998.
- T. Ball and S. K. Rajamani. The SLAM project: debugging system software via static analysis. In POPL, 2002.
- T. Ball, A. Podelski, and S. K. Rajamani. Boolean and cartesian abstraction for model checking C programs. In TACAS, 2001.
- D. Beyer. Competition on software verification - (SV-COMP). In TACAS, 2012.
- D. Beyer and M. E. Keremoglu. CPAchecker: A tool for configurable software verification. In CAV, 2011.
- A. R. Bradley, Z. Manna, and H. B. Sipma. Linear ranking with reachability. In CAV, 2005.
- R. Bruttomesso, A. Cimatti, A. Franzen, A. Griggio, and R. Sebastiani. The MathSAT 4SMT solver. In CAV, 2008.
- E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. Counterexample-guided abstraction refinement. In CAV, 2000.
- B. Cook, A. Podelski, and A. Rybalchenko. Termination proofs for systems code. In PLDI, 2006.
- B. Cook, A. Podelski, and A. Rybalchenko. Summarization for termination: no return! Formal Methods in System Design, 35(3), 2009.
- C. Flanagan and S. Qadeer. Thread-modular model checking. In SPIN, 2003.
- T. Freeman and F. Pfenning. Refinement types for ML. In PLDI, 1991.
- S. Graf and H. Saıdi. Construction of abstract state graphs with PVS. In CAV, 1997.
- 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.
- A. Gupta, C. Popeea, and A. Rybalchenko. Solving recursion-free horn clauses over LI+UIF. In APLAS, 2011.
- A. Gupta, C. Popeea, and A. Rybalchenko. Threader: A constraintbased verifier for multi-threaded programs. In CAV, 2011.
- A. Gupta, C. Popeea, and A. Rybalchenko. Predicate abstraction and refinement for verifying multi-threaded programs. In POPL, 2011.
- T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. In POPL, 2002.
- T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions from proofs. In POPL, 2004.
- K. Hoder, N. Bjørner, and L. de Moura. μZ- an efficient engine for fixed points with constraints. In CAV, 2011.
- F. Ivancic, Z. Yang, M. K. Ganai, A. Gupta, I. Shlyakhter, and P. Ashar. F-Soft: Software verification platform. In CAV, 2005.
- R. Jhala, R. Majumdar, and A. Rybalchenko. HMC: Verifying functional programs using abstract interpreters. In CAV, 2011.
- C. B. Jones. Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst., 5(4), 1983.
- K. W. Knowles and C. Flanagan. Type reconstruction for general refinement types. In ESOP, 2007.
- J. Kodumal and A. Aiken. Banshee: A scalable constraint-based analysis toolkit. In SAS, 2005.
- 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.
- S. Lerner, T. D. Millstein, E. Rice, and C. Chambers. Automated soundness proofs for dataflow analyses and transformations via local rules. In POPL, 2005.
- Z. Manna and A. Pnueli. Temporal verification of reactive systems: safety. 1995.
- F. Martin. PAG – An efficient program analyzer generator. STTT, 2 (1), 1998.
- K. L. McMillan. An interpolating theorem prover. TCS, 2005.
- K. L. McMillan. Lazy abstraction with interpolants. In CAV, 2006.
- M. Naik, A. Aiken, and J. Whaley. Effective static race detection for Java. In PLDI, 2006.
- 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.
- S. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Inf., 6, 1976.
- A. Podelski and A. Rybalchenko. Transition invariants. In LICS, 2004.
- A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In VMCAI, 2004.
- C. Popeea and A. Rybalchenko. Compositional termination proofs for multi-threaded programs. In TACAS, 2012.
- W. H. Press, B. P. Flannery, S. A. Teukolsky, and W. T. Vetterling. Numerical Recipes in C: The Art of Scientific Computing. 1992.
- 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.
- T. W. Reps, S. Horwitz, and S. Sagiv. Precise interprocedural dataflow analysis via graph reachability. In POPL, 1995.
- P. M. Rondon, M. Kawaguchi, and R. Jhala. Liquid types. In PLDI, 2008.
- G. Rosu and A. Stefanescu. Matching logic: a new program verification approach. In ICSE, 2011.
- T. Rus, E. V. Wyk, and T. Halverson. Generating model checkers from algebraic specifications. Formal Methods in System Design, 20(3), 2002.
- A. Rybalchenko and V. Sofronie-Stokkermans. Constraint solving for interpolation. In VMCAI, 2007.
- M. Sagiv. High Level Formalisms for Program Flow Analysis and their use in Compiling. PhD thesis, Technion, 1991.
- T. Terauchi. Dependent types from counterexamples. In POPL, 2010.
- S. L. Torre, P. Madhusudan, and G. Parlato. Analyzing recursive programs using a fixed-point calculus. In PLDI, 2009.
- H. Unno and N. Kobayashi. Dependent type inference with interpolants. In PPDP, 2009.
- J. Whaley and M. S. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In PLDI, 2004.

Tags

Comments

数据免责声明

页面数据均来自互联网公开来源、合作出版商和通过AI技术自动分析结果，我们不对页面数据的有效性、准确性、正确性、可靠性、完整性和及时性做出任何承诺和保证。若有疑问，可以通过电子邮件方式联系我们：report@aminer.cn