AI helps you reading Science

AI generates interpretation videos

AI extracts and analyses the key points of the paper to generate videos automatically


pub
Go Generating

AI Traceability

AI parses the academic lineage of this thesis


Master Reading Tree
Generate MRT

AI Insight

AI extracts a summary of this paper


Weibo:
We presented a logical step towards the automatic generation of software verification tools

Synthesizing software verifiers from proof rules

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

Cited by: 201|Views146
EI

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

 

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