BLAST model checker
{{Infobox software
| name = BLAST
| logo =
| screenshot =
| caption =
| author = Dirk Beyer, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar, Berkeley
| developer = Mikhail Mandrykin, Vadim Mutilin, Pavel Shved, Institute for System Programming
| released =
| latest release version = 2.7.3{{Cite web | url=http://forge.ispras.ru/projects/blast/files |title = Files - BLAST - Open-Source Projects}}
| latest release date = {{Start date and age|df=yes|2015|10|30}}
| latest preview version =
| latest preview date =
| programming language = OCaml
| operating system = Linux
| language =
| genre = Static code analysis
| license = Apache License, Version 2.0
| website = {{URL|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
BLAST came first in the category DeviceDrivers64 in the 1st Competition on Software Verification (2012) that was held at TACAS 2012 in Tallinn.{{cite conference
| author=Dirk Beyer
| title=Competition on Software Verification (SV-COMP)
| book-title=Proceedings of the 18th International Conference on Tools and Algorithms for the Construction and of Analysis Systems
| publisher=Springer-Verlag, Heidelberg
| year=2012
| url=http://www.sosy-lab.org/~dbeyer/Publications/2012-TACAS.Competition_on_Software_Verification.pdf
}}
BLAST came third (category DeviceDrivers64) in the 2nd Competition on Software Verification (2013) that was held at TACAS 2013 in Rome.{{cite conference
| author=Dirk Beyer
| title=Second Competition on Software Verification (Summary of SV-COMP 2013)
| book-title=Proceedings of the 19th International Conference on Tools and Algorithms for the Construction and of Analysis Systems
| publisher=Springer-Verlag, Heidelberg
| year=2013
| url=http://www.sosy-lab.org/~dbeyer/Publications/2013-TACAS.Second_Competition_on_Software_Verification.pdf
}}
BLAST came first in the category DeviceDrivers64 in the 3rd Competition on Software Verification (2014), that was held at TACAS 2014 in Grenoble.{{cite conference
| author=Dirk Beyer
| title=Third Competition on Software Verification (Summary of SV-COMP 2014)
| book-title=Proceedings of the 20th International Conference on Tools and Algorithms for the Construction and of Analysis Systems
| publisher=Springer-Verlag, Heidelberg
| year=2014
| url=http://www.sosy-lab.org/~dbeyer/Publications/2014-TACAS.Status_Report_on_Software_Verification.pdf
}}
References
{{Reflist}}
;Notes
{{refbegin}}
- {{cite book |author=Pavel Shved |author2=Mikhail Mandrykin |author3=Vadim Mutilin|chapter= Predicate Analysis with BLAST 2.7.|title=Tools and Algorithms for the Construction and Analysis of Systems|publisher=Springer-Verlag|pages =525–527|year=2012|series=Lecture Notes in Computer Science|volume = 7214|isbn=978-3-642-28756-5|
editor1-first=Cormac|editor1-last=Flanagan|editor2-first= Barbara| editor2-last=König}}
- {{cite journal|doi=10.1007/s10009-007-0044-z|last1=Beyer|first1=Dirk|last2=Henzinger|first2=Thomas A.|last3=Jhala|first3=Ranjit|last4=Majumdar|first4=Rupak|title=The Software Model Checker Blast|journal=International Journal on Software Tools for Technology Transfer|volume=9|issue=5–6|pages=505–525|year= 2007|s2cid=1662778}}
- {{cite book|author=Thomas A. Henzinger|author2=Ranjit Jhala|author3=Rupak Majumdar|author4=Gregoire Sutre|name-list-style=amp|chapter= Software Verification with Blast|title=Proceedings of the 10th SPIN Workshop on Model Checking Software (SPIN 2003)|publisher=Springer-Verlag|pages =235–239|year=2003|series=Lecture Notes in Computer Science|volume = 2648|isbn=3-540-40117-2|editor1-first=Thomas|editor1-last= Ball|editor2-first= Sriram K.| editor2-last=Rajamani}}
{{refend}}
External links
- [http://mtc.epfl.ch/software-tools/blast/ BLAST 2.5 website]
- [http://forge.ispras.ru/projects/blast/ BLAST 2.7 website]
Category:Free software testing tools
Category:Static program analysis tools
Category:Software using the Apache license
{{programming-software-stub}}