BLAST

BLAST (Berkeley Lazy Abstraction Software verification Tool) is a static software verification tool for C language that solves the reachability problem, i.e. whether a given program location can be reached from an entry point (main function) by a valid execution. Verification of safety properties may be reduced to the reachability, and BLAST is used for such verification in the Linux Driver Verification project. You may download source code or binary releases of BLAST for Linux on the Files page. The repository checkout instructions are located at the Repository tab. You may file a bug here as well. BLAST and all the components it relies on are free software. The BLAST itself is released under Apache 2.0 license (see source:LICENSE); for information about the components see source:NOTICE file. The BLAST has been developed for ten years by a number of people. The version maintained here is based on BLAST v2.5 released in 2008 by Dirk Beyer, Rupak Majumdar, Ranjit Jhala, and Thomas A. Henzinger. For a full list of contributors, refer to the source:README file.


References in zbMATH (referenced in 129 articles , 2 standard articles )

Showing results 101 to 120 of 129.
Sorted by year (citations)
  1. Beyer, Dirk; Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak: The software model checker blast (2007) ioport
  2. Brückner, Ingo; Dräger, Klaus; Finkbeiner, Bernd; Wehrheim, Heike: Slicing abstractions (2007)
  3. Cousot, Patrick; Ganty, Pierre; Raskin, Jean-François: Fixpoint-guided abstraction refinements (2007)
  4. Habermehl, Peter; Iosif, Radu; Rogalewicz, Adam; Vojnar, Tomáš: Proving termination of tree manipulating programs (2007)
  5. Sakunkonchak, Thanyapat; Komatsu, Satoshi; Fujita, Masahiro: Using counterexample analysis to minimize the number of predicates for predicate abstraction (2007)
  6. Smith, Michael J. A.: Stochastic modelling of communication protocols from source code (2007)
  7. Anand, Saswat; Păsăreanu, Corina S.; Visser, Willem: Symbolic execution with abstract subsumption checking (2006)
  8. Armando, Alessandro; Mantovani, Jacopo; Platania, Lorenzo: Bounded model checking of software using SMT solvers instead of SAT solvers (2006)
  9. Edelkamp, Stefan; Jabbar, Shahid; Lluch Lafuente, Alberto: Heuristic search for the analysis of graph transition systems (2006)
  10. Falke, Stephan; Kapur, Deepak: Inductive decidability using implicit induction (2006)
  11. Xia, Songtao; Di Vito, Ben; Munoz, Cesar: Predicate abstraction of programs with non-linear computation (2006)
  12. Arons, Tamarah; Elster, Elad; Fix, Limor; Mador-Haim, Sela; Mishaeli, Michael; Shalev, Jonathan; Singerman, Eli; Tiemeyer, Andreas; Vardi, Moshe Y.; Zuck, Lenore D.: Formal verification of backward compatibility of microcode (2005)
  13. Bourahla, Mustapha; Benmohamed, Mohamed: Model checking multi-agent systems (2005)
  14. Daum, Matthias; Maus, Stefan; Schirmer, Norbert; Seghir, M. Nassim: Integration of a software model checker into Isabelle (2005)
  15. Dimovski, Aleksandar; Ghica, Dan R.; Lazić, Ranko: Data-abstraction refinement: A game semantic approach (2005)
  16. Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak: The BLAST software verification system (2005) ioport
  17. McMillan, K. L.: An interpolating theorem prover (2005)
  18. Naik, Mayur; Palsberg, Jens: A type system equivalent to a model checker (2005)
  19. Talpin, Jean-Pierre; Guernic, Paul Le; Shukla, Sandeep Kumar; Gupta, Rajesh: A compositional behavioral modeling framework for embedded system design and conformance checking (2005)
  20. Xie, Tao; Marinov, Darko; Schulte, Wolfram; Notkin, David: Symstra: A framework for generating object-oriented unit tests using symbolic execution (2005)