Publications of year 2007

Articles in journal or book chapters

  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. Invited to special issue of selected papers from FASE 2004/05. [ Info ] [ PDF ] Keyword(s): Software Model Checking.
    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.
    Annotation:
    BLAST is available at: http://www.sosy-lab.org/~dbeyer/Blast

    @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},
    year = {2007. Invited to special issue of selected papers from FASE 2004/05},
    pages = {505-525},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2007-STTT.The_Software_Model_Checker_BLAST.pdf},
    url = {http://dx.doi.org/10.1007/s10009-007-0044-z},
    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. },
    annote = {BLAST is available at:  http://www.sosy-lab.org/~dbeyer/Blast },
    
    }
    

Articles in conference or workshop proceedings

  1. 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). [ PDF ] Keyword(s): Interfaces for Component-Based Design.
    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.
    Annotation:
    Online: http://dx.doi.org/10.1109/ICWS.2007.32

    @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)},
    publisher = {IEEE Computer Society Press, Los Alamitos~(CA)},
    pages = {831-838},
    year = {2007},
    isbn = {0-7695-2924-0},
    keyword = {Interfaces for Component-Based Design},
    pdf = {https://www.sosy-lab.org/research/pub/2007-ICWS.An_Application_of_Web-Service_Interfaces.pdf},
    url = {},
    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. },
    annote = { Online:  http://dx.doi.org/10.1109/ICWS.2007.32 },
    
    }
    

  2. Dirk Beyer, Thomas A. Henzinger, Rupak Majumdar, and Andrey Rybalchenko. Invariant Synthesis for Combined Theories. In 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. [ PDF ] Keyword(s): Software Model Checking.
    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.
    Annotation:
    VMCAI 2007, Nice, January 14-16,
    , editors.
    © 2007 Springer-Verlag
    Online: http://dx.doi.org/10.1007/978-3-540-69738-1_27

    @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)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {},
    series = {LNCS~4349},
    pages = {378-394},
    year = {2007},
    isbn = {978-3-540-69735-0},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2007-VMCAI.Invariant_Synthesis_for_Combined_Theories.pdf},
    url = {},
    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. },
    annote = { VMCAI 2007, Nice, January 14-16,
    , editors.
    © 2007 Springer-Verlag
    Online: http://dx.doi.org/10.1007/978-3-540-69738-1_27 }, }

  3. 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). [ PDF ] Keyword(s): Software Model Checking.
    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.
    Annotation:
    PLDI 2007, San Diego, CA, June 10-13,
    © 2007 ACM
    Online: http://dx.doi.org/10.1145/1250734.1250769

    @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)},
    publisher = {ACM Press, New York~(NY)},
    pages = {300-309},
    year = {2007},
    isbn = {978-1-59593-633-2},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2007-PLDI.Path_Invariants.pdf},
    url = {},
    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. },
    annote = { PLDI 2007, San Diego, CA, June 10-13,
    © 2007 ACM
    Online: http://dx.doi.org/10.1145/1250734.1250769 }, }

  4. 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. [ PDF ] Keyword(s): Interfaces for Component-Based Design, Software Model Checking.
    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.
    Annotation:
    CAV 2007, Berlin, July 3-7,
    Werner Damm, Holger Hermanns, editors.
    © 2007 Springer-Verlag
    Online: http://dx.doi.org/10.1007/978-3-540-73368-3_4

    @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)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {W.~Damm and H.~Hermanns},
    series = {LNCS~4590},
    pages = {4-19},
    year = {2007},
    isbn = {978-3-540-73367-6},
    keyword = {Interfaces for Component-Based Design,Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2007-CAV.Algorithms_for_Interface_Synthesis.pdf},
    url = {},
    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. },
    annote = { CAV 2007, Berlin, July 3-7,
    Werner Damm, Holger Hermanns, editors.
    © 2007 Springer-Verlag
    Online: http://dx.doi.org/10.1007/978-3-540-73368-3_4 }, }

  5. 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. [ PDF ] Keyword(s): Software Model Checking.
    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.
    Annotation:
    CAV 2007, Berlin, July 3-7,
    Werner Damm, Holger Hermanns, editors.
    © 2007 Springer-Verlag
    Online: http://dx.doi.org/10.1007/978-3-540-73368-3_51

    @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)},
    publisher = {Springer-Verlag, Heidelberg},
    editor = {W.~Damm and H.~Hermanns},
    series = {LNCS~4590},
    pages = {504-518},
    year = {2007},
    isbn = {978-3-540-73367-6},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2007-CAV.Configurable_Software_Verification.pdf},
    url = {},
    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. },
    annote = { CAV 2007, Berlin, July 3-7,
    Werner Damm, Holger Hermanns, editors.
    © 2007 Springer-Verlag
    Online: http://dx.doi.org/10.1007/978-3-540-73368-3_51 }, }

Internal reports

  1. 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érale de Lausanne (EPFL), December 2007. [ Info ] [ PDF ] Keyword(s): Interfaces for Component-Based Design.
    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.
    Annotation:
    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

    @TechReport{TR002-EPFL07,
    author = {Dirk Beyer and Arindam Chakrabarti and Thomas A. Henzinger},
    title = {An Interface Formalism for Web Services},
    institution ={School of Computer and Communication Sciences (IC), Ecole Polytechnique F\'ed\'erale de Lausanne (EPFL)},
    number = {MTC-REPORT-2007-002},
    month = {December},
    year = {2007},
    keyword = {Interfaces for Component-Based Design},
    pdf = {https://www.sosy-lab.org/research/pub/2007-EPFL-TR002.An_Interface_Formalism_for_Web_Services.pdf},
    url = {http://infoscience.epfl.ch/search?recid=114605&ln=en},
    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. },
    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). 
    Online: http://infoscience.epfl.ch/search?recid=114605&ln=en
    }, }




Disclaimer:

This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All person copying this information are expected to adhere to the terms and constraints invoked by each author's copyright. In most cases, these works may not be reposted without the explicit permission of the copyright holder.




Last modified: Mon Dec 18 13:27:46 2017


This document was translated from BibTEX by bibtex2html