Software and Computational Systems Lab

Publications about BLAST

1. Dirk Beyer, Thomas A. Henzinger, Grégory Théoduloz, and Damien Zufferey. Shape Refinement through Explicit Heap Analysis. In D.S. Rosenblum and G. Taentzer, editors, Proceedings of the 13th International Conference on Fundamental Approaches to Software Engineering (FASE 2010, Paphos, Cyprus, March 22-26), LNCS 6013, pages 263-277, 2010. Springer-Verlag, Heidelberg. doi:10.1007/978-3-642-12029-9_19 Keyword(s): BLAST, Software Model Checking Publisher's Version PDF
   Abstract

   Shape analysis is a promising technique to prove program properties about recursive data structures. The challenge is to automatically determine the data-structure type, and to supply the shape analysis with the necessary information about the data structure. We present a stepwise approach to the selection of instrumentation predicates for a TVLA-based shape analysis, which takes us a step closer towards the fully automatic verification of data structures. The approach uses two techniques to guide the refinement of shape abstractions: (1) during program exploration, an explicit heap analysis collects sample instances of the heap structures, which are used to identify the data structures that are manipulated by the program; and (2) during abstraction refinement along an infeasible error path, we consider different possible heap abstractions and choose the coarsest one that eliminates the infeasible path. We have implemented this combined approach for automatic shape refinement as an extension of the software model checker BLAST. Example programs from a data-structure library that manipulate doubly-linked lists and trees were successfully verified by our tool.
   BibTeX Entry

   @inproceedings{FASE10, author = {Dirk Beyer and Thomas A.~Henzinger and Gr{\'e}gory Th{\'e}oduloz and Damien Zufferey}, title = {Shape Refinement through Explicit Heap Analysis}, booktitle = {Proceedings of the 13th International Conference on Fundamental Approaches to Software Engineering (FASE~2010, Paphos, Cyprus, March 22-26)}, editor = {D.S.~Rosenblum and G.~Taentzer}, pages = {263-277}, year = {2010}, series = {LNCS~6013}, publisher = {Springer-Verlag, Heidelberg}, isbn = {978-3-642-12028-2}, doi = {10.1007/978-3-642-12029-9_19}, sha256 = {60468f681028a3ac427897405ee5c99894c5baa340896454d378d55267be304f}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2010-FASE.Shape_Refinement_through_Explicit_Heap_Analysis.pdf}, abstract = {Shape analysis is a promising technique to prove program properties about recursive data structures. The challenge is to automatically determine the data-structure type, and to supply the shape analysis with the necessary information about the data structure. We present a stepwise approach to the selection of instrumentation predicates for a TVLA-based shape analysis, which takes us a step closer towards the fully automatic verification of data structures. The approach uses two techniques to guide the refinement of shape abstractions: (1) during program exploration, an explicit heap analysis collects sample instances of the heap structures, which are used to identify the data structures that are manipulated by the program; and (2) during abstraction refinement along an infeasible error path, we consider different possible heap abstractions and choose the coarsest one that eliminates the infeasible path. We have implemented this combined approach for automatic shape refinement as an extension of the software model checker BLAST. Example programs from a data-structure library that manipulate doubly-linked lists and trees were successfully verified by our tool.}, keyword = {BLAST,Software Model Checking}, }
2. Dirk Beyer, Thomas A. Henzinger, and Grégory Théoduloz. Program Analysis with Dynamic Precision Adjustment. In Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008, L'Aquila, September 15-19), pages 29-38, 2008. IEEE Computer Society Press, Los Alamitos (CA). doi:10.1109/ASE.2008.13 Keyword(s): BLAST, Software Model Checking Publisher's Version PDF Presentation
   Abstract

   We present and evaluate a framework and tool for combining multiple program analyses which allows the dynamic (on-line) adjustment of the precision of each analysis depending on the accumulated results. For example, the explicit tracking of the values of a variable may be switched off in favor of a predicate abstraction when and where the number of different variable values that have been encountered has exceeded a specified threshold. The method is evaluated on verifying the SSH client/server software and shows significant gains compared with predicate abstraction-based model checking.
   BibTeX Entry

   @inproceedings{ASE08, author = {Dirk Beyer and Thomas A.~Henzinger and Gr{\'e}gory Th{\'e}oduloz}, title = {Program Analysis with Dynamic Precision Adjustment}, booktitle = {Proceedings of the 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE~2008, L'Aquila, September 15-19)}, pages = {29-38}, year = {2008}, publisher = {IEEE Computer Society Press, Los Alamitos~(CA)}, isbn = {978-1-4244-2187-9}, doi = {10.1109/ASE.2008.13}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2008-ASE.Program_Analysis_with_Dynamic_Precision_Adjustment.pdf}, presentation = {https://www.sosy-lab.org/research/prs/2009-04-16_UCB_CPAplus.pdf}, abstract = {We present and evaluate a framework and tool for combining multiple program analyses which allows the dynamic (on-line) adjustment of the precision of each analysis depending on the accumulated results. For example, the explicit tracking of the values of a variable may be switched off in favor of a predicate abstraction when and where the number of different variable values that have been encountered has exceeded a specified threshold. The method is evaluated on verifying the SSH client/server software and shows significant gains compared with predicate abstraction-based model checking.}, keyword = {BLAST,Software Model Checking}, annote = {}, }
3. 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.
4. 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
   
5. 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 = {}, }
6. Dirk Beyer, Thomas A. Henzinger, and Grégory Théoduloz. Lazy Shape Analysis. In T. Ball and R.B. Jones, editors, Proceedings of the 18th International Conference on Computer Aided Verification (CAV 2006, Seattle, WA, August 17-20), LNCS 4144, pages 532-546, 2006. Springer-Verlag, Heidelberg. doi:10.1007/11817963_48 Keyword(s): BLAST, Software Model Checking Publisher's Version PDF Supplement
   Abstract

   Many software model checkers are based on predicate abstraction. If the verification goal depends on pointer structures, the approach does not work well, because it is difficult to find adequate predicate abstractions for the heap. In contrast, shape analysis, which uses graph-based heap abstractions, can provide a compact representation of recursive data structures. We integrate shape analysis into the software model checker BLAST. Because shape analysis is expensive, we do not apply it globally. Instead, we ensure that, like predicates, shape graphs are computed and stored locally, only where necessary for proving the verification goal. To achieve this, we extend lazy abstraction refinement, which so far has been used only for predicate abstractions, to three-valued logical structures. This approach does not only increase the precision of model checking, but it also increases the efficiency of shape analysis. We implemented the technique by extending BLAST with calls to TVLA.
   BibTeX Entry

   @inproceedings{CAV06, author = {Dirk Beyer and Thomas A.~Henzinger and Gr{\'e}gory Th{\'e}oduloz}, title = {Lazy Shape Analysis}, booktitle = {Proceedings of the 18th International Conference on Computer Aided Verification (CAV~2006, Seattle, WA, August 17-20)}, editor = {T.~Ball and R.B.~Jones}, pages = {532-546}, year = {2006}, series = {LNCS~4144}, publisher = {Springer-Verlag, Heidelberg}, isbn = {3-540-37406-X}, doi = {10.1007/11817963_48}, sha256 = {83aadf3fff8dfe5462691e635eb3f21fda3bd09638cf78a94d71ca87efbd5390}, url = {http://www.sosy-lab.org/~dbeyer/blast_sa/}, pdf = {https://www.sosy-lab.org/research/pub/2006-CAV.Lazy_Shape_Analysis.pdf}, abstract = {Many software model checkers are based on predicate abstraction. If the verification goal depends on pointer structures, the approach does not work well, because it is difficult to find adequate predicate abstractions for the heap. In contrast, shape analysis, which uses graph-based heap abstractions, can provide a compact representation of recursive data structures. We integrate shape analysis into the software model checker BLAST. Because shape analysis is expensive, we do not apply it globally. Instead, we ensure that, like predicates, shape graphs are computed and stored locally, only where necessary for proving the verification goal. To achieve this, we extend lazy abstraction refinement, which so far has been used only for predicate abstractions, to three-valued logical structures. This approach does not only increase the precision of model checking, but it also increases the efficiency of shape analysis. We implemented the technique by extending BLAST with calls to TVLA.}, keyword = {BLAST,Software Model Checking}, annote = {An extended version of this paper appeared in Proc. Dagstuhl Seminar 06081, IBFI Schloss Dagstuhl, 2006: <BR> <a href="http://drops.dagstuhl.de/portals/06081/"> http://drops.dagstuhl.de/portals/06081/</a> <BR> Supplementary material: <a href="http://www.sosy-lab.org/~dbeyer/blast_sa/"> http://www.sosy-lab.org/~dbeyer/blast_sa/</a>}, }
   Additional Infos

   An extended version of this paper appeared in Proc. Dagstuhl Seminar 06081, IBFI Schloss Dagstuhl, 2006:
   http://drops.dagstuhl.de/portals/06081/
   Supplementary material: http://www.sosy-lab.org/~dbeyer/blast_sa/
7. Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. Checking Memory Safety with Blast. In M. Cerioli, editors, Proceedings of the Eighth International Conference on Fundamental Approaches to Software Engineering (FASE 2005, Edinburgh, April 2-10), LNCS 3442, pages 2-18, 2005. Springer-Verlag, Heidelberg. doi:10.1007/978-3-540-31984-9_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. Given a C program and a temporal safety property, BLAST statically proves that either the program satisfies the safety property or the program has an execution trace that exhibits a violation of the property. BLAST constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. We show how BLAST can be used to statically prove memory safety for C programs. We take a two-step approach. First, we use CCured, a type-based memory safety analyzer, to annotate with run-time checks all program points that cannot be proved memory safe by the type system. Second, we use BLAST to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate for the remaining run-time checks execution traces that witness them fail. Our experience shows that BLAST can remove many of the run-time checks added by CCured and provide useful information to the programmer about many of the remaining checks.
   BibTeX Entry

   @inproceedings{FASE05, author = {Dirk Beyer and Thomas A. Henzinger and Ranjit Jhala and Rupak Majumdar}, title = {Checking Memory Safety with {{\sc Blast}}}, booktitle = {Proceedings of the Eighth International Conference on Fundamental Approaches to Software Engineering (FASE~2005, Edinburgh, April 2-10)}, editor = {M.~Cerioli}, pages = {2-18}, year = {2005}, series = {LNCS~3442}, publisher = {Springer-Verlag, Heidelberg}, isbn = {3-540-25420-X}, doi = {10.1007/978-3-540-31984-9_2}, sha256 = {8216a41d893b4e987c3a19b82a0c8be06aa7f5bc9b35ef26ab226b95aea241b3}, url = {}, pdf = {https://www.sosy-lab.org/research/pub/2005-FASE.Checking_Memory_Safety_with_Blast.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 statically proves that either the program satisfies the safety property or the program has an execution trace that exhibits a violation of the property. BLAST constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. We show how BLAST can be used to statically prove memory safety for C programs. We take a two-step approach. First, we use CCured, a type-based memory safety analyzer, to annotate with run-time checks all program points that cannot be proved memory safe by the type system. Second, we use BLAST to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate for the remaining run-time checks execution traces that witness them fail. Our experience shows that BLAST can remove many of the run-time checks added by CCured and provide useful information to the programmer about many of the remaining checks.}, keyword = {BLAST,Software Model Checking}, annote = {}, }
8. 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 = {}, }
9. 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 = {}, }
10. 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 = {}, }

11. Grégory Théoduloz. Software Verification by Combining Program Analyses of Adjustable Precision. PhD Thesis, EPFL, MTC Lab, supervised by Prof. Thomas Henzinger, 2010. Keyword(s): BLAST, Software Model Checking PDF
    BibTeX Entry

    @misc{GregoryCPA, author = {Gr{\'e}gory Th{\'e}oduloz}, title = {Software Verification by Combining Program Analyses of Adjustable Precision}, year = {2010}, pdf = {https://doi.org/10.5075/epfl-thesis-4781}, keyword = {BLAST,Software Model Checking}, howpublished = {PhD Thesis, EPFL, MTC Lab, supervised by Prof. Thomas Henzinger}, }
12. Damien Zufferey. Master's Thesis, EPFL, MTC Lab, with Prof. Thomas Henzinger, 2009. Keyword(s): BLAST, Software Model Checking
    BibTeX Entry

    @misc{ZuffereyShape, author = {Damien Zufferey}, title = {}, year = {2009}, pdf = {}, keyword = {BLAST,Software Model Checking}, annote = {}, howpublished = {Master's Thesis, EPFL, MTC Lab, with Prof. Thomas Henzinger}, }
13. Grégory Théoduloz. Integrating Shape Analysis into the Model Checker Blast. Master's Thesis, EPFL, MTC Lab, with Prof. Thomas Henzinger, 2006. Keyword(s): BLAST, Software Model Checking
    BibTeX Entry

    @misc{TheodulozShape, author = {Gr{\'e}gory Th{\'e}oduloz}, title = {Integrating Shape Analysis into the Model Checker \textsc{Blast}}, year = {2006}, pdf = {}, keyword = {BLAST,Software Model Checking}, annote = {Won the EPFL Unicible Award 2006 and the ELCA Informatique Prize}, howpublished = {Master's Thesis, EPFL, MTC Lab, with Prof. Thomas Henzinger}, }
    Additional Infos

    Won the EPFL Unicible Award 2006 and the ELCA Informatique Prize