Publications of year 2004

Articles in conference or workshop proceedings

  1. 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). [ PDF ] Keyword(s): Software Model Checking.
    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).
    Annotation:
    Online: http://dx.doi.org/10.1109/ICSE.2004.1317455

    @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)},
    publisher = {IEEE Computer Society Press, Los Alamitos~(CA)},
    pages = {326-335},
    year = {2004},
    isbn = {0-7695-2163-0},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2004-ICSE.Generating_Tests_from_Counterexamples.pdf},
    url = {},
    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). },
    annote = {ICSE 2004, Edinburgh, May 26-28},
    annote = { Online:  http://dx.doi.org/10.1109/ICSE.2004.1317455 
    }, }

  2. Dirk Beyer, Adam J. Chlipala, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. The Blast Query Language for Software Verification. In R. Giacobazzi, editor, Proceedings of the 11th International Static Analysis Symposium (SAS 2004, Verona, August 26-28), LNCS 3148, pages 2-18, 2004. Springer-Verlag, Heidelberg. [ PDF ] Keyword(s): Software Model Checking.
    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.
    Annotation:
    SAS 2004, Verona, August 26-28,
    Roberto Giacobazzi, editor.
    © 2006 Springer-Verlag
    Online: http://dx.doi.org/10.1007/b99688

    @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},
    series = {LNCS~3148},
    pages = {2-18},
    publisher = {Springer-Verlag, Heidelberg},
    year = {2004},
    isbn = {3-540-22791-1},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2004-SAS.The_Blast_Query_Language_for_Software_Verification.pdf},
    url = {},
    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. },
    annote = { SAS 2004, Verona, August 26-28,
    Roberto Giacobazzi, editor.
    © 2006 Springer-Verlag
    Online: http://dx.doi.org/10.1007/b99688
    }, }

  3. 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). [ PDF ] Keyword(s): Software Model Checking.
    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.
    Annotation:
    IWPC 2004, Bari, June 24-26
    Online: http://dx.doi.org/10.1109/WPC.2004.1311069

    @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)},
    publisher = {IEEE Computer Society Press, Los Alamitos~(CA)},
    pages = {251-255},
    year = {2004},
    isbn = {0-7695-2149-5},
    keyword = {Software Model Checking},
    pdf = {https://www.sosy-lab.org/research/pub/2004-IWPC.An_Eclipse_Plug-in_for_Model_Checking.pdf},
    url = {},
    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. },
    annote = {IWPC 2004, Bari, June 24-26
    Online: http://dx.doi.org/10.1109/WPC.2004.1311069
    }, }

Internal reports

  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. [ Info ] [ PDF ] Keyword(s): Structural Analysis and Comprehension.
    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.
    Annotation:
    Online: http://sunsite.berkeley.edu/TechRepPages/CSD-04-1338
    ArXiv archive: http://arxiv.org/abs/cs/0409009
    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/

    @TechReport{TR1338-UCB04,
    author = {Dirk Beyer and Andreas Noack},
    title = {{CrocoPat} 2.1 {I}ntroduction and Reference Manual},
    institution ={Computer Science Division (EECS), University of California, Berkeley},
    number = {UCB//CSD-04-1338},
    month = {July},
    year = {2004},
    note = {Also: The Computing Research Repository (CoRR), cs.PL/0409009, September 2004},
    keyword = {Structural Analysis and Comprehension},
    pdf = {https://www.sosy-lab.org/research/pub/2004-UCB-TR1338.CrocoPat_2.1_Introduction_and_Reference_Manual.pdf},
    url = {../../2004-UCB-TR1338.CrocoPat_2.1_Introduction_and_Reference_Manual/main.html},
    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. },
    annote = {Online:  http://sunsite.berkeley.edu/TechRepPages/CSD-04-1338 
    ArXiv archive: http://arxiv.org/abs/cs/0409009
    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/ }, }




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 14:34:44 2017


This document was translated from BibTEX by bibtex2html