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 41 to 60 of 129.
Sorted by year (citations)
  1. Albarghouthi, Aws; Gurfinkel, Arie; Chechik, Marsha: Whale: an interpolation-based algorithm for inter-procedural verification (2012)
  2. Albarghouthi, Aws; Gurfinkel, Arie; Chechik, Marsha: From under-approximations to over-approximations and back (2012)
  3. Christakis, Maria; Müller, Peter; Wüstholz, Valentin: Collaborative verification and testing with explicit assumptions (2012)
  4. Cimatti, Alessandro; Narasamdya, Iman; Roveri, Marco: Software model checking with explicit scheduler and symbolic threads (2012)
  5. Cook, Byron; Koskinen, Eric; Vardi, Moshe: Temporal property verification as a program analysis task (2012)
  6. Ermis, Evren; Hoenicke, Jochen; Podelski, Andreas: Splitting via interpolants (2012)
  7. Gallardo, M. M.; Joubert, C.; Merino, P.; Sanán, D.: A model-extraction approach to verifying concurrent C programs with CADP (2012) ioport
  8. Jaffar, Joxan; Murali, Vijayaraghavan; Navas, Jorge A.; Santosa, Andrew E.: TRACER: a symbolic execution tool for verification (2012)
  9. Mandrykin, M. U.; Mutilin, V. S.; Novikov, E. M.; Khoroshilov, A. V.; Shved, P. E.: Using Linux device drivers for static verification tools benchmarking (2012) ioport
  10. Neatherway, Robin P.; Ramsay, Steven J.; Ong, Chih-Hao Luke: A traversal-based algorithm for higher-order model checking (2012)
  11. Shved, Pavel; Mandrykin, Mikhail; Mutilin, Vadim: Predicate analysis with BLAST 2.7 (competition contribution) (2012) ioport
  12. Shved, P. E.; Mutilin, V. S.; Mandrykin, M. U.: Experience of improving the BLAST static verification tool (2012)
  13. Westergaard, Michael: Verifying parallel algorithms and programs using coloured Petri nets (2012)
  14. Alglave, Jade; Donaldson, Alastair F.; Kroening, Daniel; Tautschnig, Michael: Making software verification tools really work (2011) ioport
  15. Braghin, Chiara; Sharygina, Natasha; Barone-Adesi, Katerina: A model checking-based approach for security policy verification of mobile systems (2011)
  16. Cimatti, Alessandro; Narasamdya, Iman; Roveri, Marco: Boosting lazy abstraction for SystemC with partial order reduction (2011)
  17. de Melo, Ana C. V.; Silveira, Paulo: Improving data perturbation testing techniques for web services (2011) ioport
  18. Donaldson, Alastair F.; Kroening, Daniel; Rümmer, Philipp: Automatic analysis of DMA races using model checking and (k)-induction (2011)
  19. Gaudel, Marie-Claude: Checking models, proving programs, and testing systems (2011) ioport
  20. Kim, Moonzoo; Kim, Yunho: Automated analysis of industrial embedded software (2011) ioport