meanings of Blast Model Checker encyclopedia of Blast Model Checker dictionary of Blast Model Checker thesaurus on Blast Model Checker books about Blast Model Checker dreams about Blast Model Checker
 Blast Model Checker - Definition 

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

Copyright 2008 WordIQ.com - Privacy Policy  ::  Terms of Use  :: Contact Us  :: About Us
This article is licensed under the GNU Free Documentation License. It uses material from the Wikipedia article "Blast Model Checker".