BLAST model checker

From Wikipedia, the free encyclopedia
Jump to: navigation, search
BLAST
Original author(s) Dirk Beyer, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar, Berkeley
Developer(s) Mikhail Mandrykin, Vadim Mutilin, Pavel Shved, Institute for System Programming
Stable release
2.7.3[1] / 18 November 2014; 2 years ago (2014-11-18)
Written in OCaml
Operating system Linux
Type Static code analysis
License Apache License, Version 2.0
Website forge.ispras.ru/projects/blast

The Berkeley Lazy Abstraction Software Verification Tool (BLAST) is a software model checking tool for C programs. The task addressed by BLAST is the need to check whether software satisfies the behavioral requirements of its associated interfaces. BLAST employs counterexample-driven automatic abstraction refinement to construct an abstract model that is then model-checked for safety properties. The abstraction is constructed on the fly, and only to the requested precision.

Achievements[edit]

BLAST came first in the category DeviceDrivers64 in the 1st Competition on Software Verification (2012) that was held at TACAS 2012 in Tallinn.[2]

BLAST came third (category DeviceDrivers64) in the 2nd Competition on Software Verification (2013) that was held at TACAS 2013 in Rome.[3]

BLAST came first in the category DeviceDrivers64 in the 3rd Competition on Software Verification (2014) that was held at TACAS 2014 in Grenoble.[4]

References[edit]

  1. ^ http://forge.ispras.ru/projects/blast/files
  2. ^ Dirk Beyer (2012). "Competition on Software Verification (SV-COMP)" (PDF). Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and of Analysis Systems. Springer-Verlag, Heidelberg. 
  3. ^ Dirk Beyer (2013). "Second Competition on Software Verification (Summary of SV-COMP 2013)" (PDF). Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and of Analysis Systems. Springer-Verlag, Heidelberg. 
  4. ^ Dirk Beyer (2014). "Third Competition on Software Verification (Summary of SV-COMP 2014)" (PDF). Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and of Analysis Systems. Springer-Verlag, Heidelberg. 
Notes
  • Pavel Shved; Mikhail Mandrykin; Vadim Mutilin (2012). "Predicate Analysis with BLAST 2.7.". In Flanagan, Cormac; König, Barbara. Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. 7214. Springer-Verlag. pp. 525–527. ISBN 978-3-642-28756-5. 
  • Beyer, Dirk; Henzinger, Thomas A.; Jhala, Ranjit; Majumdar, Rupak (2007). "The Software Model Checker Blast". International Journal on Software Tools for Technology Transfer. 9 (5-6): 505–525. doi:10.1007/s10009-007-0044-z. 
  • Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar & Gregoire Sutre (2003). "Software Verification with Blast". In Ball, Thomas & Rajamani, Sriram K. Proceedings of the 10th SPIN Workshop on Model Checking Software (SPIN 2003). Lecture Notes in Computer Science. 2648. Springer-Verlag. pp. 235–239. ISBN 3-540-40117-2. 

External links[edit]