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 (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]

  • 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, and 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]