The software model checker BLAST: Applications to software engineering

D. Beyer, T.A. Henzinger, R. Jhala, R. Majumdar, International Journal on Software Tools for Technology Transfer 9 (2007) 505–525.

Download
No fulltext has been uploaded. References only!

Journal Article | Published
Author
; ; ;
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.
Publishing Year
Date Published
2007-10-01
Journal Title
International Journal on Software Tools for Technology Transfer
Volume
9
Issue
5
Page
505 - 525
IST-REx-ID

Cite this

Beyer D, Henzinger TA, Jhala R, Majumdar R. The software model checker BLAST: Applications to software engineering. International Journal on Software Tools for Technology Transfer. 2007;9(5):505-525. doi:10.1007/s10009-007-0044-z
Beyer, D., Henzinger, T. A., Jhala, R., & Majumdar, R. (2007). The software model checker BLAST: Applications to software engineering. International Journal on Software Tools for Technology Transfer, 9(5), 505–525. https://doi.org/10.1007/s10009-007-0044-z
Beyer, Dirk, Thomas A Henzinger, Ranjit Jhala, and Ritankar Majumdar. “The Software Model Checker BLAST: Applications to Software Engineering.” International Journal on Software Tools for Technology Transfer 9, no. 5 (2007): 505–25. https://doi.org/10.1007/s10009-007-0044-z.
D. Beyer, T. A. Henzinger, R. Jhala, and R. Majumdar, “The software model checker BLAST: Applications to software engineering,” International Journal on Software Tools for Technology Transfer, vol. 9, no. 5, pp. 505–525, 2007.
Beyer D, Henzinger TA, Jhala R, Majumdar R. 2007. The software model checker BLAST: Applications to software engineering. International Journal on Software Tools for Technology Transfer. 9(5), 505–525.
Beyer, Dirk, et al. “The Software Model Checker BLAST: Applications to Software Engineering.” International Journal on Software Tools for Technology Transfer, vol. 9, no. 5, Springer, 2007, pp. 505–25, doi:10.1007/s10009-007-0044-z.

Export

Marked Publications

Open Data IST Research Explorer

Search this title in

Google Scholar