Editing BLAST model checker (section)

{{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]].