Software and Computational Systems Lab

Publications of year 2007

1. Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. The Software Model Checker Blast: Applications to Software Engineering. International Journal on Software Tools for Technology Transfer (STTT), 9(5-6):505-525, 2007. doi:10.1007/s10009-007-0044-z Invited to special issue of selected papers from FASE 2004/05 Keyword(s): Software Model Checking Publisher's Version PDF Presentation
   Abstract

   BLAST is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, BLAST either statically proves that the program satisfies the safety property, or provides an execution path that exhibits a violation of the property (or, since the problem is undecidable, does not terminate). BLAST constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. This paper gives an introduction to BLAST and demonstrates, through two case studies, how it can be applied to program verification and test-case generation. In the first case study, we use BLAST to statically prove memory safety for C programs. We use CCured, a type-based memory-safety analyzer, to annotate a program with run-time assertions that check for safe memory operations. Then, we use BLAST to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate execution scenarios that violate the assertions for the remaining run-time checks. In our second case study, we use BLAST to automatically generate test suites that guarantee full coverage with respect to a given predicate. Given a C program and a target predicate p, BLAST determines the program locations q for which there exists a program execution that reaches q with p true, and automatically generates a set of test vectors that cause such executions. Our experiments show that BLAST can provide automated, precise, and scalable analysis for C programs.
   BibTeX Entry

   @article{STTT07, author = {Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar}, title = {The Software Model Checker {{\sc Blast}}: Applications to Software Engineering}, journal = {International Journal on Software Tools for Technology Transfer (STTT)}, volume = {9}, number = {5-6}, pages = {505-525}, year = {2007}, doi = {10.1007/s10009-007-0044-z}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2007-STTT.The_Software_Model_Checker_BLAST.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2008-05-08_EPFL_BLAST_Dirk.pdf}, abstract = {BLAST is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, BLAST either statically proves that the program satisfies the safety property, or provides an execution path that exhibits a violation of the property (or, since the problem is undecidable, does not terminate). BLAST constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. This paper gives an introduction to BLAST and demonstrates, through two case studies, how it can be applied to program verification and test-case generation. In the first case study, we use BLAST to statically prove memory safety for C programs. We use CCured, a type-based memory-safety analyzer, to annotate a program with run-time assertions that check for safe memory operations. Then, we use BLAST to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate execution scenarios that violate the assertions for the remaining run-time checks. In our second case study, we use BLAST to automatically generate test suites that guarantee full coverage with respect to a given predicate. Given a C program and a target predicate p, BLAST determines the program locations q for which there exists a program execution that reaches q with p true, and automatically generates a set of test vectors that cause such executions. Our experiments show that BLAST can provide automated, precise, and scalable analysis for C programs.}, keyword = {Software Model Checking}, annote = {BLAST is available at: <a href="http://www.sosy-lab.org/~dbeyer/Blast/"> http://www.sosy-lab.org/~dbeyer/Blast</a>}, note = {Invited to special issue of selected papers from FASE 2004/05}, }
   Additional Infos

   BLAST is available at: http://www.sosy-lab.org/~dbeyer/Blast

2. Dirk Beyer, Arindam Chakrabarti, Thomas A. Henzinger, and Sanjit A. Seshia. An Application of Web-Service Interfaces. In Proceedings of the 2007 IEEE International Conference on Web Services (ICWS 2007, Salt Lake City, UT, July 9-13), pages 831-838, 2007. IEEE Computer Society Press, Los Alamitos (CA). doi:10.1109/ICWS.2007.32 Keyword(s): Interfaces for Component-Based Design Publisher's Version PDF
   Abstract

   We present a case study to illustrate our formalism for the specification and verification of the method-invocation behavior of web-service applications constructed from asynchronously interacting multi-threaded distributed components. Our model is expressive enough to allow the representation of recursion and dynamic thread creation, and yet permits the algorithmic analysis of the following two questions: (1) Does a given service satisfy a safety specification? (2) Can a given service be substituted by a another service in an arbitrary context? Our case study is based on the Amazon.com E-Commerce Services (ECS) platform.
   BibTeX Entry

   @inproceedings{ICWS07, author = {Dirk Beyer and Arindam Chakrabarti and Thomas A.~Henzinger and Sanjit A. Seshia}, title = {An Application of Web-Service Interfaces}, booktitle = {Proceedings of the 2007 IEEE International Conference on Web Services (ICWS~2007, Salt Lake City, UT, July 9-13)}, pages = {831-838}, year = {2007}, publisher = {IEEE Computer Society Press, Los Alamitos~(CA)}, isbn = {0-7695-2924-0}, doi = {10.1109/ICWS.2007.32}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2007-ICWS.An_Application_of_Web-Service_Interfaces.pdf}, abstract = {We present a case study to illustrate our formalism for the specification and verification of the method-invocation behavior of web-service applications constructed from asynchronously interacting multi-threaded distributed components. Our model is expressive enough to allow the representation of recursion and dynamic thread creation, and yet permits the algorithmic analysis of the following two questions: (1) Does a given service satisfy a safety specification? (2) Can a given service be substituted by a another service in an arbitrary context? Our case study is based on the Amazon.com E-Commerce Services (ECS) platform.}, keyword = {Interfaces for Component-Based Design}, annote = {}, }
3. Dirk Beyer, Thomas A. Henzinger, and Vasu Singh. Algorithms for Interface Synthesis. In W. Damm and H. Hermanns, editors, Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007, Berlin, July 3-7), LNCS 4590, pages 4-19, 2007. Springer-Verlag, Heidelberg. doi:10.1007/978-3-540-73368-3_4 Keyword(s): Interfaces for Component-Based Design, Software Model Checking Publisher's Version PDF
   Abstract

   A temporal interface for a software component is a finite automaton that specifies the legal sequences of calls to functions that are provided by the component. We compare and evaluate three different algorithms for automatically extracting temporal interfaces from program code: (1) a game algorithm that computes the interface as a representation of the most general environment strategy to avoid a safety violation; (2) a learning algorithm that repeatedly queries the program to construct the minimal interface automaton; and (3) a CEGAR algorithm that iteratively refines an abstract interface hypothesis by adding relevant program variables. For comparison purposes, we present and implement the three algorithms in a unifying formal setting. While the three algorithms compute the same output and have similar worst-case complexities, their actual running times may differ considerably for a given input program. On the theoretical side, we provide for each of the three algorithms a family of input programs on which that algorithm outperforms the two alternatives. On the practical side, we evaluate the three algorithms experimentally on a variety of Java libraries.
   BibTeX Entry

   @inproceedings{CAV07b, author = {Dirk Beyer and Thomas A.~Henzinger and Vasu Singh}, title = {Algorithms for Interface Synthesis}, booktitle = {Proceedings of the 19th International Conference on Computer Aided Verification (CAV~2007, Berlin, July 3-7)}, editor = {W.~Damm and H.~Hermanns}, pages = {4-19}, year = {2007}, series = {LNCS~4590}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-540-73367-6}, doi = {10.1007/978-3-540-73368-3_4}, sha256 = {c8d7d6300d354fb38917b44cb9fbd3ebbad1737d75107ccc124af001677679ec}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2007-CAV.Algorithms_for_Interface_Synthesis.pdf}, abstract = {A temporal interface for a software component is a finite automaton that specifies the legal sequences of calls to functions that are provided by the component. We compare and evaluate three different algorithms for automatically extracting temporal interfaces from program code: (1) a game algorithm that computes the interface as a representation of the most general environment strategy to avoid a safety violation; (2) a learning algorithm that repeatedly queries the program to construct the minimal interface automaton; and (3) a CEGAR algorithm that iteratively refines an abstract interface hypothesis by adding relevant program variables. For comparison purposes, we present and implement the three algorithms in a unifying formal setting. While the three algorithms compute the same output and have similar worst-case complexities, their actual running times may differ considerably for a given input program. On the theoretical side, we provide for each of the three algorithms a family of input programs on which that algorithm outperforms the two alternatives. On the practical side, we evaluate the three algorithms experimentally on a variety of Java libraries.}, keyword = {Interfaces for Component-Based Design,Software Model Checking}, annote = {}, }
4. Dirk Beyer, Thomas A. Henzinger, and Grégory Théoduloz. Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis. In W. Damm and H. Hermanns, editors, Proceedings of the 19th International Conference on Computer Aided Verification (CAV 2007, Berlin, July 3-7), LNCS 4590, pages 504-518, 2007. Springer-Verlag, Heidelberg. doi:10.1007/978-3-540-73368-3_51 Keyword(s): BLAST, Software Model Checking Publisher's Version PDF Presentation
   Abstract

   In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers are still mostly concerned with precision, e.g., the removal of spurious counterexamples; for this purpose they build and refine reachability trees. Lattice-based program analyzers, on the other hand, are primarily concerned with efficiency. We designed an algorithm and built a tool that can be configured to perform not only a purely tree-based or a purely lattice-based analysis, but offers many intermediate settings that have not been evaluated before. The algorithm and tool take one or more abstract interpreters, such as a predicate abstraction and a shape analysis, and configure their execution and interaction using several parameters. Our experiments show that such customization may lead to dramatic improvements in the precision-efficiency spectrum.
   BibTeX Entry

   @inproceedings{CAV07a, author = {Dirk Beyer and Thomas A.~Henzinger and Gr{\'e}gory Th{\'e}oduloz}, title = {Configurable Software Verification: Concretizing the Convergence of Model Checking and Program Analysis}, booktitle = {Proceedings of the 19th International Conference on Computer Aided Verification (CAV~2007, Berlin, July 3-7)}, editor = {W.~Damm and H.~Hermanns}, pages = {504-518}, year = {2007}, series = {LNCS~4590}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-540-73367-6}, doi = {10.1007/978-3-540-73368-3_51}, sha256 = {1c5d0f57fdded4d659c5a86984e19307c50d7770442fa908db20430a22e4b276}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2007-CAV.Configurable_Software_Verification.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2007-07-07_CAV07_Configurable-Program-Analysis.pdf}, abstract = {In automatic software verification, we have observed a theoretical convergence of model checking and program analysis. In practice, however, model checkers are still mostly concerned with precision, e.g., the removal of spurious counterexamples; for this purpose they build and refine reachability trees. Lattice-based program analyzers, on the other hand, are primarily concerned with efficiency. We designed an algorithm and built a tool that can be configured to perform not only a purely tree-based or a purely lattice-based analysis, but offers many intermediate settings that have not been evaluated before. The algorithm and tool take one or more abstract interpreters, such as a predicate abstraction and a shape analysis, and configure their execution and interaction using several parameters. Our experiments show that such customization may lead to dramatic improvements in the precision-efficiency spectrum.}, keyword = {BLAST,Software Model Checking}, annote = {<a href="https://www.sosy-lab.org/research/pub/2007-CAV.Configurable_Software_Verification.Errata.txt"> Errata</a> available.}, }
   Additional Infos

   Errata available.
5. Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, and Andrey Rybalchenko. Path Invariants. In Proceedings of the 2007 ACM Conference on Programming Language Design and Implementation (PLDI 2007, San Diego, CA, June 10-13), pages 300-309, 2007. ACM Press, New York (NY). doi:10.1145/1250734.1250769 Keyword(s): BLAST, Software Model Checking Publisher's Version PDF
   Abstract

   The 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 current schemes, the cause of a false alarm is identified as an infeasible error path, and the abstraction is refined in order to remove that path. By contrast, we view the cause of a false alarm -the spurious counterexample- as a full-fledged program, namely, a fragment of the original program whose control-flow graph may contain loops and represent unbounded computations. There are two advantages to using such path programs as counterexamples for abstraction refinement. First, we can bring the whole machinery of program analysis to bear on path programs, which are typically small compared to the original program. Specifically, we use constraint-based invariant generation to automatically infer invariants of path programs -so-called path invariants. Second, we use path invariants for abstraction refinement in order to remove not one infeasibility at a time, but at once all (possibly infinitely many) infeasible error computations that are represented by a path program. Unlike previous predicate discovery schemes, our method handles loops without unrolling them; it infers abstractions that involve universal quantification and naturally incorporates disjunctive reasoning.
   BibTeX Entry

   @inproceedings{PLDI07, author = {Dirk Beyer and Thomas A.~Henzinger and Rupak Majumdar and Andrey Rybalchenko}, title = {Path Invariants}, booktitle = {Proceedings of the 2007 ACM Conference on Programming Language Design and Implementation (PLDI~2007, San Diego, CA, June 10-13)}, pages = {300-309}, year = {2007}, publisher = {ACM Press, New York~(NY)}, isbn = {978-1-59593-633-2}, doi = {10.1145/1250734.1250769}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2007-PLDI.Path_Invariants.pdf}, abstract = {The 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 current schemes, the cause of a false alarm is identified as an infeasible error path, and the abstraction is refined in order to remove that path. By contrast, we view the cause of a false alarm ---the spurious counterexample--- as a full-fledged program, namely, a fragment of the original program whose control-flow graph may contain loops and represent unbounded computations. There are two advantages to using such path programs as counterexamples for abstraction refinement. First, we can bring the whole machinery of program analysis to bear on path programs, which are typically small compared to the original program. Specifically, we use constraint-based invariant generation to automatically infer invariants of path programs ---so-called path invariants. Second, we use path invariants for abstraction refinement in order to remove not one infeasibility at a time, but at once all (possibly infinitely many) infeasible error computations that are represented by a path program. Unlike previous predicate discovery schemes, our method handles loops without unrolling them; it infers abstractions that involve universal quantification and naturally incorporates disjunctive reasoning.}, keyword = {BLAST,Software Model Checking}, annote = {Video: <a href="https://www.youtube.com/watch?v=vUN0n23zVuw"> https://www.youtube.com/watch?v=vUN0n23zVuw</a><BR>}, }
   Additional Infos

   Video: https://www.youtube.com/watch?v=vUN0n23zVuw
   
6. Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, and Andrey Rybalchenko. Invariant Synthesis for Combined Theories. In B. Cook and A. Podelski, editors, Proceedings of the Eighth International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI 2007, Nice, January 14-16), LNCS 4349, pages 378-394, 2007. Springer-Verlag, Heidelberg. doi:10.1007/978-3-540-69738-1_27 Keyword(s): BLAST, Software Model Checking Publisher's Version PDF
   Abstract

   We present a constraint-based algorithm for the synthesis of invariants expressed in the combined theory of linear arithmetic and uninterpreted function symbols. Given a set of programmer-specified invariant templates, our algorithm reduces the invariant synthesis problem to a sequence of arithmetic constraint satisfaction queries. Since the combination of linear arithmetic and uninterpreted functions is a widely applied predicate domain for program verification, our algorithm provides a powerful tool to statically and automatically reason about program correctness. The algorithm can also be used for the synthesis of invariants over arrays and set data structures, because satisfiability questions for the theories of sets and arrays can be reduced to the theory of linear arithmetic with uninterpreted functions. We have implemented our algorithm and used it to find invariants for a low-level memory allocator written in C.
   BibTeX Entry

   @inproceedings{VMCAI07, author = {Dirk Beyer and Thomas A.~Henzinger and Rupak Majumdar and Andrey Rybalchenko}, title = {Invariant Synthesis for Combined Theories}, booktitle = {Proceedings of the Eighth International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI~2007, Nice, January 14-16)}, editor = {B.~Cook and A.~Podelski}, pages = {378-394}, year = {2007}, series = {LNCS~4349}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-540-69735-0}, doi = {10.1007/978-3-540-69738-1_27}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2007-VMCAI.Invariant_Synthesis_for_Combined_Theories.pdf}, abstract = {We present a constraint-based algorithm for the synthesis of invariants expressed in the combined theory of linear arithmetic and uninterpreted function symbols. Given a set of programmer-specified invariant templates, our algorithm reduces the invariant synthesis problem to a sequence of arithmetic constraint satisfaction queries. Since the combination of linear arithmetic and uninterpreted functions is a widely applied predicate domain for program verification, our algorithm provides a powerful tool to statically and automatically reason about program correctness. The algorithm can also be used for the synthesis of invariants over arrays and set data structures, because satisfiability questions for the theories of sets and arrays can be reduced to the theory of linear arithmetic with uninterpreted functions. We have implemented our algorithm and used it to find invariants for a low-level memory allocator written in C.}, keyword = {BLAST,Software Model Checking}, annote = {}, }

7. Dirk Beyer, Arindam Chakrabarti, and Thomas A. Henzinger. An Interface Formalism for Web Services. Technical report MTC-REPORT-2007-002, School of Computer and Communication Sciences (IC), Ecole Polytechnique Féd́̊ale de Lausanne (EPFL), December 2007. Keyword(s): Interfaces for Component-Based Design PDF Supplement
   Abstract

   Web application development using distributed components and web services presents new software integration challenges, because solutions often cross vendor, administrative, and other boundaries across which neither binary nor source code can be shared. We present a methodology that addresses this problem through a formalism for specifying and manipulating behavioral interfaces of multi-threaded open software components that communicate with each other through method calls. An interface constrains both the implementation and the user of a web service to fulfill certain assumptions that are specified by the interface. Our methodology consists of three increasingly expressive classes of interfaces. Signature interfaces specify the methods that can be invoked by the user, together with parameters. Consistency interfaces add propositional constraints, enhancing signature interfaces with the ability to specify choice and causality. Protocol interfaces specify, in addition, temporal ordering constraints on method invocations. We provide approaches to check if two or more interfaces are compatible; if a web service can be safely substituted for another one; and if a web service satisfies a specification that represents a desired behavioral property.
   BibTeX Entry

   @techreport{TR002-EPFL07, author = {Dirk Beyer and Arindam Chakrabarti and Thomas A. Henzinger}, title = {An Interface Formalism for Web Services}, number = {MTC-REPORT-2007-002}, year = {2007}, url = {http://infoscience.epfl.ch/search?recid=114605&ln=en}, pdf = {https://www.sosy-lab.org/research/pub/2007-EPFL-TR002.An_Interface_Formalism_for_Web_Services.pdf}, abstract = {Web application development using distributed components and web services presents new software integration challenges, because solutions often cross vendor, administrative, and other boundaries across which neither binary nor source code can be shared. We present a methodology that addresses this problem through a formalism for specifying and manipulating behavioral interfaces of multi-threaded open software components that communicate with each other through method calls. An interface constrains both the implementation and the user of a web service to fulfill certain assumptions that are specified by the interface. Our methodology consists of three increasingly expressive classes of interfaces. Signature interfaces specify the methods that can be invoked by the user, together with parameters. Consistency interfaces add propositional constraints, enhancing signature interfaces with the ability to specify choice and causality. Protocol interfaces specify, in addition, temporal ordering constraints on method invocations. We provide approaches to check if two or more interfaces are compatible; if a web service can be safely substituted for another one; and if a web service satisfies a specification that represents a desired behavioral property.}, keyword = {Interfaces for Component-Based Design}, annote = {A preliminary version of this paper was presented at the First International Workshop on Foundations of Interface Technologies (FIT 2005, San Francisco, CA, August 21). <BR> Online: <a href="http://infoscience.epfl.ch/search?recid=114605&ln=en"> http://infoscience.epfl.ch/search?recid=114605&ln=en</a> <BR>}, institution = {School of Computer and Communication Sciences (IC), Ecole Polytechnique F\'ed\'erale de Lausanne (EPFL)}, month = {December}, }
   Additional Infos

   A preliminary version of this paper was presented at the First International Workshop on Foundations of Interface Technologies (FIT 2005, San Francisco, CA, August 21).
   Online: http://infoscience.epfl.ch/search?recid=114605&ln=en
   

8. CPAchecker: Configurable Software Verification. 2007. Keyword(s): Software Development Project, CPAchecker, Software Model Checking Supplement
   BibTeX Entry

   @misc{CPAchecker, title = {{{\sc CPAchecker}}: Configurable Software Verification}, year = {2007}, url = {http://www.sosy-lab.org/~dbeyer/CPAchecker/}, keyword = {Software Development Project,CPAchecker,Software Model Checking}, role = {Principal designer, architect, implementation, and maintenance}, }