Editing BLAST model checker

{{Infobox software
| name                   = BLAST
| logo                   = 
| screenshot             =
| caption                = 
| author                 = Dirk Beyer, Thomas Henzinger, Ranjit Jhala, Rupak Majumdar, [[University of California, Berkeley|Berkeley]]
| developer              = Mikhail Mandrykin, Vadim Mutilin, Pavel Shved, [[Institute for System Programming]]
| released               =
| latest release version = 2.7.3<ref>{{Cite web | url=http://forge.ispras.ru/projects/blast/files |title = Files - BLAST - Open-Source Projects}}</ref>
| 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 Software 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 (programming language)|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 (arithmetic)|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]].<ref>{{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
}}</ref>

BLAST came third (category DeviceDrivers64) in the 2nd Competition on Software Verification (2013) that was held at TACAS 2013 in [[Rome]].<ref>{{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
}}</ref>

BLAST came first in the category DeviceDrivers64 in the 3rd Competition on Software Verification (2014), that was held at TACAS 2014 in [[Grenoble]].<ref>{{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
}}</ref>

==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:Model checkers]]
[[Category:Static program analysis tools]]
[[Category:Software using the Apache license]]


{{programming-software-stub}}