| 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]
/ 30 October 2015 |
| Written in | OCaml |
| Operating system | Linux |
| Type | Static code analysis |
| License | Apache License, Version 2.0 |
| Website | forge |
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]
- ^ "Files - BLAST - Open-Source Projects".
- ^ 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.
- ^ 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.
- ^ 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 (eds.). Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Vol. 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. S2CID 1662778.
- Thomas A. Henzinger; Ranjit Jhala; Rupak Majumdar & Gregoire Sutre (2003). "Software Verification with Blast". In Ball, Thomas & Rajamani, Sriram K. (eds.). Proceedings of the 10th SPIN Workshop on Model Checking Software (SPIN 2003). Lecture Notes in Computer Science. Vol. 2648. Springer-Verlag. pp. 235–239. ISBN 3-540-40117-2.
External links[edit]