Software and Computational Systems Lab

Publications of year 2004

1. Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. The Blast Query Language for Software Verification. In R. Giacobazzi, editors, Proceedings of the 11th International Static Analysis Symposium (SAS 2004, Verona, August 26-28), LNCS 3148, pages 2-18, 2004. Springer-Verlag, Heidelberg. doi:10.1007/978-3-540-27864-1_2 Keyword(s): BLAST, Software Model Checking Publisher's Version PDF
   Abstract

   BLAST is an automatic verification tool for checking temporal safety properties of C programs. BLAST is based on lazy predicate abstraction driven by interpolation-based predicate discovery. In this paper, we present the BLAST specification language. The language specifies program properties at two levels of precision. At the lower level, monitor automata are used to specify temporal safety properties of program executions (traces). At the higher level, relational reachability queries over program locations are used to combine lower-level trace properties. The two-level specification language can be used to break down a verification task into several independent calls of the model-checking engine. In this way, each call to the model checker may have to analyze only part of the program, or part of the specification, and may thus succeed in a reduction of the number of predicates needed for the analysis. In addition, the two-level specification language provides a means for structuring and maintaining specifications.
   BibTeX Entry

   @inproceedings{SAS04, author = {Dirk Beyer and Adam J. Chlipala and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar}, title = {The {{\sc Blast}} Query Language for Software Verification}, booktitle = {Proceedings of the 11th International Static Analysis Symposium (SAS~2004, Verona, August 26-28)}, editor = {R.~Giacobazzi}, pages = {2-18}, year = {2004}, series = {LNCS~3148}, publisher = {Springer-Verlag, Heidelberg}, isbn = {3-540-22791-1}, doi = {10.1007/978-3-540-27864-1_2}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2004-SAS.The_Blast_Query_Language_for_Software_Verification.pdf}, abstract = {BLAST is an automatic verification tool for checking temporal safety properties of C programs. BLAST is based on lazy predicate abstraction driven by interpolation-based predicate discovery. In this paper, we present the BLAST specification language. The language specifies program properties at two levels of precision. At the lower level, monitor automata are used to specify temporal safety properties of program executions (traces). At the higher level, relational reachability queries over program locations are used to combine lower-level trace properties. The two-level specification language can be used to break down a verification task into several independent calls of the model-checking engine. In this way, each call to the model checker may have to analyze only part of the program, or part of the specification, and may thus succeed in a reduction of the number of predicates needed for the analysis. In addition, the two-level specification language provides a means for structuring and maintaining specifications.}, keyword = {BLAST,Software Model Checking}, annote = {}, }
2. Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. An Eclipse Plug-in for Model Checking. In Proceedings of the 12th IEEE International Workshop on Program Comprehension (IWPC 2004, Bari, June 24-26), pages 251-255, 2004. IEEE Computer Society Press, Los Alamitos (CA). doi:10.1109/WPC.2004.1311069 Keyword(s): BLAST, Software Model Checking Publisher's Version PDF
   Abstract

   While model checking has been successful in uncovering subtle bugs in code, its adoption in software engineering practice has been hampered by the absence of a simple interface to the programmer in an integrated development environment. We describe an integration of the software model checker BLAST into the Eclipse development environment. We provide a verification interface for practical solutions for some typical program analysis problems -assertion checking, reachability analysis, dead code analysis, and test generation- directly on the source code. The analysis is completely automatic, and assumes no knowledge of model checking or formal notation. Moreover, the interface supports incremental program verification to support incremental design and evolution of code.
   BibTeX Entry

   @inproceedings{IWPC04, author = {Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar}, title = {An {Eclipse} Plug-in for Model Checking}, booktitle = {Proceedings of the 12th IEEE International Workshop on Program Comprehension (IWPC~2004, Bari, June 24-26)}, pages = {251-255}, year = {2004}, publisher = {IEEE Computer Society Press, Los Alamitos~(CA)}, isbn = {0-7695-2149-5}, doi = {10.1109/WPC.2004.1311069}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2004-IWPC.An_Eclipse_Plug-in_for_Model_Checking.pdf}, abstract = {While model checking has been successful in uncovering subtle bugs in code, its adoption in software engineering practice has been hampered by the absence of a simple interface to the programmer in an integrated development environment. We describe an integration of the software model checker BLAST into the Eclipse development environment. We provide a verification interface for practical solutions for some typical program analysis problems --assertion checking, reachability analysis, dead code analysis, and test generation-- directly on the source code. The analysis is completely automatic, and assumes no knowledge of model checking or formal notation. Moreover, the interface supports incremental program verification to support incremental design and evolution of code.}, keyword = {BLAST,Software Model Checking}, annote = {}, }
3. Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Generating Tests from Counterexamples. In Proceedings of the 26th IEEE International Conference on Software Engineering (ICSE 2004, Edinburgh, May 26-28), pages 326-335, 2004. IEEE Computer Society Press, Los Alamitos (CA). doi:10.1109/ICSE.2004.1317455 Keyword(s): BLAST, Software Model Checking Publisher's Version PDF
   Abstract

   We have extended the software model checker BLAST to automatically generate test suites that guarantee full coverage with respect to a given predicate. More precisely, given a C program and a target predicate p, BLAST determines the set L of program locations which program execution can reach with p true, and automatically generates a set of test vectors that exhibit the truth of p at all locations in L. We have used BLAST to generate test suites and to detect dead code in C programs with up to 30K lines of code. The analysis and test-vector generation is fully automatic (no user intervention) and exact (no false positives).
   BibTeX Entry

   @inproceedings{ICSE04, author = {Dirk Beyer and Adam J. Chlipala and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar}, title = {Generating Tests from Counterexamples}, booktitle = {Proceedings of the 26th IEEE International Conference on Software Engineering (ICSE~2004, Edinburgh, May 26-28)}, pages = {326-335}, year = {2004}, publisher = {IEEE Computer Society Press, Los Alamitos~(CA)}, isbn = {0-7695-2163-0}, doi = {10.1109/ICSE.2004.1317455}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2004-ICSE.Generating_Tests_from_Counterexamples.pdf}, abstract = {We have extended the software model checker BLAST to automatically generate test suites that guarantee full coverage with respect to a given predicate. More precisely, given a C program and a target predicate p, BLAST determines the set L of program locations which program execution can reach with p true, and automatically generates a set of test vectors that exhibit the truth of p at all locations in L. We have used BLAST to generate test suites and to detect dead code in C programs with up to 30K lines of code. The analysis and test-vector generation is fully automatic (no user intervention) and exact (no false positives).}, keyword = {BLAST,Software Model Checking}, annote = {}, }

1. Dirk Beyer and Andreas Noack. CrocoPat 2.1 Introduction and Reference Manual. Technical report UCB//CSD-04-1338, Computer Science Division (EECS), University of California, Berkeley, July 2004. Also: The Computing Research Repository (CoRR), cs.PL/0409009, September 2004 Keyword(s): Structural Analysis and Comprehension PDF Supplement
   Abstract

   CrocoPat is an efficient, powerful and easy-to-use tool for manipulating relations of arbitrary arity, including directed graphs. This manual provides an introduction to and a reference for CrocoPat and its programming language RML. It includes several application examples, in particular from the analysis of structural models of software systems.
   BibTeX Entry

   @techreport{TR1338-UCB04, author = {Dirk Beyer and Andreas Noack}, title = {{CrocoPat} 2.1 {I}ntroduction and Reference Manual}, number = {UCB//CSD-04-1338}, year = {2004}, url = {../../2004-UCB-TR1338.CrocoPat_2.1_Introduction_and_Reference_Manual/main.html}, pdf = {https://arxiv.org/abs/cs/0409009}, abstract = {CrocoPat is an efficient, powerful and easy-to-use tool for manipulating relations of arbitrary arity, including directed graphs. This manual provides an introduction to and a reference for CrocoPat and its programming language RML. It includes several application examples, in particular from the analysis of structural models of software systems.}, keyword = {Structural Analysis and Comprehension}, annote = {Online: <a href="http://sunsite.berkeley.edu/TechRepPages/CSD-04-1338"> http://sunsite.berkeley.edu/TechRepPages/CSD-04-1338</a> <BR> A tutorial and user's guide for CrocoPat, defines and explains the syntax and semantics of the extended language. <BR> CrocoPat is available at: <a href="http://www.sosy-lab.org/~dbeyer/CrocoPat/"> http://www.sosy-lab.org/~dbeyer/CrocoPat/</a>}, institution = {Computer Science Division (EECS), University of California, Berkeley}, month = {July}, note = {Also: The Computing Research Repository (CoRR), cs.PL/0409009, September 2004}, }
   Additional Infos

   Online: http://sunsite.berkeley.edu/TechRepPages/CSD-04-1338
   A tutorial and user's guide for CrocoPat, defines and explains the syntax and semantics of the extended language.
   CrocoPat is available at: http://www.sosy-lab.org/~dbeyer/CrocoPat/

1. Chic: Checking Interface Compatibility. 2004. Keyword(s): Software Development Project, Interfaces for Component-Based Design Supplement
   BibTeX Entry

   @misc{Chic, title = {{{\sc Chic}}: Checking Interface Compatibility}, year = {2004}, url = {http://www.sosy-lab.org/~dbeyer/Chic/}, keyword = {Software Development Project,Interfaces for Component-Based Design}, role = {Contributor, new formalism, and verification algorithm}, }