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 81 to 100 of 129.
Sorted by year (citations)
  1. Anand, Saswat; Păsăreanu, Corina S.; Visser, Willem: Symbolic execution with abstraction (2009) ioport
  2. Armando, Alessandro; Mantovani, Jacopo; Platania, Lorenzo: Bounded model checking of software using SMT solvers instead of SAT solvers (2009) ioport
  3. Bakewell, Adam; Ghica, Dan R.: Compositional predicate abstraction from game semantics (2009)
  4. Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto: Interpolant generation for UTVPI (2009)
  5. del Mar Gallardo, María; Merino, Pedro; Sanán, David: Model checking dynamic memory allocation in operating systems (2009)
  6. Eggers, Andreas; Kalinnik, Natalia; Kupferschmid, Stefan; Teige, Tino: Challenges in constraint-based analysis of hybrid systems (2009)
  7. Emmi, Michael; Jhala, Ranjit; Kohler, Eddie; Majumdar, Rupak: Verifying reference counting implementations (2009)
  8. Fehnker, Ansgar; Huuck, Ralf; Seefried, Sean: Incremental false path elimination for static software analysis (2009)
  9. Holzer, Andreas; Schallhart, Christian; Tautschnig, Michael; Veith, Helmut: Query-driven program testing (2009)
  10. Kuliamin, V. V.: Integration of verification methods for program systems (2009)
  11. Pérez, Juan Antonio Navarro; Rybalchenko, Andrey; Singh, Atul: Cardinality abstraction for declarative networking applications (2009)
  12. Prantl, Adrian; Knoop, Jens; Kirner, Raimund; Kadlec, Albrecht; Schordan, Markus: From trusted annotations to verified knowledge (2009) ioport
  13. Tuch, Harvey: Formal verification of C systems code. Structured types, separation logic and theorem proving (2009)
  14. Lynch, Christopher; Tang, Yuefeng: Interpolants for linear arithmetic in SMT (2008)
  15. Rensink, Arend: Explicit state model checking for graph grammars (2008)
  16. Sekizawa, Toshifusa; Tanabe, Yoshinori; Yuasa, Yoshifumi; Takahashi, Koichi: MLAT: a tool for heap analysis based on predicate abstraction by modal logic (2008)
  17. Udrea, Octavian; Lumezanu, Cristian; Foster, Jeffrey S.: Rule-based static analysis of network protocol implementations (2008)
  18. Zybin, R. S.; Kuliamin, V. V.; Ponomarenko, A. V.; Rubanov, V. V.; Chernov, E. S.: Automation of broad sanity test generation (2008)
  19. Armando, Alessandro; Benerecetti, Massimo; Mantovani, Jacopo: Abstraction refinement of linear programs with arrays (2007)
  20. Betin-Can, Aysu; Bultan, Tevfik: Highly dependable concurrent programming using design for verification (2007)