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 108 articles , 2 standard articles )

Showing results 1 to 20 of 108.
Sorted by year (citations)

1 2 3 4 5 6 next

  1. Beyer, Dirk; Dangl, Matthias; Wendler, Philipp: A unifying view on SMT-based software verification (2018)
  2. Guthmuller, Marion; Corona, Gabriel; Quinson, Martin: System-level state equality detection for the formal dynamic verification of legacy distributed applications (2018)
  3. Abal, Iago; Brabrand, Claus; Wąsowski, Andrzej: Effective bug finding in C programs with shape and effect abstractions (2017)
  4. Amin, Nada; Rompf, Tiark: LMS-verify: abstraction without regret for verified systems programming (2017)
  5. Tellez, Gadi; Brotherston, James: Automatically verifying temporal properties of pointer programs with cyclic proof (2017)
  6. Aissat, Romain; Voisin, Frédéric; Wolff, Burkhart: Infeasible paths elimination by symbolic execution techniques. Proof of correctness and preservation of paths (2016)
  7. Ferrara, Pietro: A generic framework for heap and value analyses of object-oriented programming languages (2016)
  8. Karpenkov, Egor George; Monniaux, David; Wendler, Philipp: Program analysis with local policy iteration (2016)
  9. Mordan, Vitaly; Mutilin, Vadim: Checking several requirements at once by CEGAR (2016)
  10. Sharma, Rahul; Aiken, Alex: From invariant checking to invariant inference using randomized search (2016)
  11. Khoroshilov, Alexey; Mutilin, Vadim; Novikov, Evgeny; Zakharov, Ilja: Modeling environment for static verification of Linux kernel modules (2015)
  12. Kirchner, Florent; Kosmatov, Nikolai; Prevosto, Virgile; Signoles, Julien; Yakobowski, Boris: Frama-C: a software analysis perspective (2015) ioport
  13. Zakharov, I.; Mandrykin, M.; Mutilin, V.; Novikov, E.; Petrenko, A.; Khoroshilov, A.: Configurable toolset for static verification of operating systems kernel modules (2015) ioport
  14. Zakharov, I.S.; Mutilin, V.S.; Khoroshilov, A.V.: Pattern-based environment modeling for static verification of Linux kernel modules (2015) ioport
  15. Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha: An extension of lazy abstraction with interpolation for programs with arrays (2014)
  16. de Boer, Frank S.; de Gouw, Stijn: Combining monitoring with run-time assertion checking (2014)
  17. Beyer, Dirk: Second competition on software verification. (Summary of SV-COMP 2013) (2013) ioport
  18. Beyer, Dirk; Holzer, Andreas; Tautschnig, Michael; Veith, Helmut: Information reuse for multi-goal reachability analyses (2013)
  19. Dobrev, Veselin A.; Ellis, Truman E.; Kolev, Tzanio V.; Rieben, Robert N.: High-order curvilinear finite elements for axisymmetric Lagrangian hydrodynamics (2013)
  20. Křena, Bohuslav; Vojnar, Tomáš: Automated formal analysis and verification: an overview (2013)

1 2 3 4 5 6 next