NationMaster - Encyclopedia: BLAST model checker

BLAST is a software model checking tool for C programs. The goal of BLAST is to be able to check that software satisfies behavioral properties of the interfaces it uses. BLAST uses counterexample-driven automatic abstraction refinement to construct an abstract model which is model checked for safety properties. The abstraction is constructed on the fly, and only to the requested precision.

References

Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Gregoire Sutre. Software Verification with Blast. In Proceedings of the 10th SPIN Workshop on Model Checking Software (SPIN 2003), LNCS 2648, Springer-Verlag, pages 235-239, 2003.

External links

Blast: Home Page (http://www-cad.eecs.berkeley.edu/~blast/)

Results from FactBites:

Model checking - Wikipedia, the free encyclopedia (269 words)
	Model checking is a method to algorithmically verify formal systems.
	This is achieved by verifying if the model, often deriving from a hardware or software design, satisfies a formal specification.
	The model is usually expressed as a transition system, i.e directed graph consisting of nodes (or vertices) and edges.

More results at FactBites »

COMMENTARY

Share your thoughts, questions and commentary here

Want to know more?
Search encyclopedia, statistics and forums:

Feeds | Contact
The Wikipedia article included on this page is licensed under the GFDL.
Images may be subject to relevant owners' copyright.
All other elements are (c) copyright NationMaster.com 2003-5. All Rights Reserved.
Usage implies agreement with terms, 1022, m