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 61 to 80 of 129.
Sorted by year (citations)
  1. Kobayashi, Naoki: A practical linear time algorithm for trivial automata model checking of higher-order recursion schemes (2011)
  2. Kupferschmid, Stefan; Becker, Bernd: Craig interpolation in the presence of non-linear constraints (2011)
  3. Li, Li; Song, XiaoYu; Gu, Ming; Luo, XiangYu: Competent predicate abstraction in model checking (2011)
  4. Morse, Jeremy; Cordeiro, Lucas; Nicole, Denis; Fischer, Bernd: Context-bounded model checking of LTL properties for ANSI-C software (2011) ioport
  5. Siegel, Stephen F.; Zirkel, Timothy K.: TASS: the toolkit for accurate scientific software (2011)
  6. Suter, Philippe; Steiger, Robin; Kuncak, Viktor: Sets with cardinality constraints in satisfiability modulo theories (2011)
  7. Tschannen, Julian; Furia, Carlo A.; Nordio, Martin; Meyer, Bertrand: Usable verification of object-oriented programs by combining static and dynamic techniques (2011) ioport
  8. Bakewell, Adam; Dimovski, Aleksandar; Ghica, Dan R.; Lazić, Ranko: Data-abstraction refinement: a game semantic approach (2010) ioport
  9. Bošnački, Dragan; Edelkamp, Stefan: Model checking software: on some new waves and some evergreens (2010) ioport
  10. Collavizza, Hélène; Rueher, Michel; Van Hentenryck, Pascal: CPBPV: a constraint-programming framework for bounded program verification (2010)
  11. Donaldson, Alastair F.; Kroening, Daniel; Rümmer, Philipp: Automatic analysis of scratch-pad memory code for heterogeneous multicore processors (2010) ioport
  12. Dräger, Klaus; Kupriyanov, Andrey; Finkbeiner, Bernd; Wehrheim, Heike: SLAB: a certifying model checker for infinite-state concurrent systems (2010) ioport
  13. Fehnker, Ansgar; Huuck, Ralf; Seefried, Sean: Counterexample guided path reduction for static program analysis (2010)
  14. Hoenicke, Jochen; Leino, K. Rustan M.; Podelski, Andreas; Schäf, Martin; Wies, Thomas: Doomed program points (2010)
  15. Kolb, Emanuel; Šerý, Ondřej; Weiss, Roland: Applicability of the BLAST model checker: An industrial case study (2010) ioport
  16. Kolchin, A. V.: An automatic method for the dynamic construction of abstractions of states of a formal model (2010)
  17. Konnov, Igor V.; Zakharov, Vladimir A.: An invariant-based approach to the verification of asynchronous parameterized networks (2010)
  18. Monniaux, David: Automatic modular abstractions for template numerical constraints (2010)
  19. Rinderknecht, Christian; Volanschi, Nic: Theory and practice of unparsed patterns for metacompilation (2010)
  20. Amjad, Hasan; Bornat, Richard: Towards automatic stability analysis for rely-guarantee proofs (2009)