Anzeige
Erschienen in:
2005 | OriginalPaper | Buchkapitel
The BLAST Software Verification System
verfasst von : Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar
Erschienen in: Model Checking Software
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Blast
is a verification system for checking safety properties of C programs.
Blast
implements a lazy-abstraction algorithm, which integrates automatic abstraction refinement and model checking [8]. The input to
Blast
is a C program and a safety monitor written in a specification language with C like syntax [1]. The lazy-abstraction algorithm returns either an error trace of the program together with a corresponding test case [2], or a proof that the program satisfies the safety property [6] (or, since the problem is undecidable, the algorithm may fail to terminate).
Blast
automatically constructs and refines a parsimonious predicate abstraction of the input program, using an interpolation-based decision procedure to find, based on counterexample analysis, the relevant predicates for each individual control location [5].
Blast
has successfully verified and found violations of interface safety properties of large device driver programs [6,5], memory safety properties [3], race conditions in nesC programs (using an extension for concurrent programs) [4], and file handling properties of large open-source programs [9]. Extensions to
Blast
support program testing [2] and incremental programming [7].
Blast
is available from http://www.eecs.berkeley.edu/ blast.