The software model checker Blast |
| |
Authors: | Dirk Beyer Thomas A Henzinger Ranjit Jhala Rupak Majumdar |
| |
Affiliation: | (1) Simon Fraser University, Surrey, BC, Canada;(2) EPFL, Lausanne, Switzerland;(3) University of California, San Diego, USA;(4) University of California, Los Angeles, USA |
| |
Abstract: | Blast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal
safety property, Blast either statically proves that the program satisfies the safety property, or provides an execution path that exhibits a violation
of the property (or, since the problem is undecidable, does not terminate). Blast constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based
predicate discovery. This paper gives an introduction to Blast and demonstrates, through two case studies, how it can be applied to program verification and test-case generation. In the
first case study, we use Blast to statically prove memory safety for C programs. We use CCured, a type-based memory-safety analyzer, to annotate a program with run-time assertions that check for safe memory operations.
Then, we use Blast to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate execution
scenarios that violate the assertions for the remaining run-time checks. In our second case study, we use Blast to automatically generate test suites that guarantee full coverage with respect to a given predicate. Given a C program and
a target predicate p, Blast determines the program locations q for which there exists a program execution that reaches q with p true, and automatically generates a set of test vectors that cause such executions. Our experiments show that Blast can provide automated, precise, and scalable analysis for C programs. |
| |
Keywords: | Model checking Software verification Software specification Memory safety Test-case generation |
本文献已被 SpringerLink 等数据库收录! |
|