{{#invoke:Infobox|infobox}}Template:Template other{{#invoke:Check for unknown parameters | check | showblankpositional=1 | unknown = Template:Main other | preview = Page using Template:Infobox software with unknown parameter "_VALUE_"|ignoreblank=y | AsOf | author | background | bodystyle | caption | collapsetext | collapsible | developer | discontinued | engine | engines | genre | included with | language | language count | language footnote | latest preview date | latest preview version | latest release date | latest release version | latest_preview_date | latest_preview_version | latest_release_date | latest_release_version | licence | license | logo | logo alt | logo caption | logo upright | logo size | logo title | logo_alt | logo_caption | logo_upright | logo_size | logo_title | middleware | module | name | operating system | operating_system | other_names | platform | programming language | programming_language | released | replaced_by | replaces | repo | screenshot | screenshot alt | screenshot upright | screenshot size | screenshot title | screenshot_alt | screenshot_upright | screenshot_size | screenshot_title | service_name | size | standard | title | ver layout | website | qid }}Template:Main other
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.
AchievementsEdit
BLAST came first in the category DeviceDrivers64 in the 1st Competition on Software Verification (2012) that was held at TACAS 2012 in Tallinn.<ref>Template:Cite conference</ref>
BLAST came third (category DeviceDrivers64) in the 2nd Competition on Software Verification (2013) that was held at TACAS 2013 in Rome.<ref>Template:Cite conference</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>Template:Cite conference</ref>
ReferencesEdit
- Notes