---
_id: '4578'
abstract:
- lang: eng
text: 'BLAST is an automatic verification tool for checking temporal safety properties
of C programs. Blast is based on lazy predicate abstraction driven by interpolation-based
predicate discovery. In this paper, we present the Blast specification language.
The language specifies program properties at two levels of precision. At the lower
level, monitor automata are used to specify temporal safety properties of program
executions (traces). At the higher level, relational reachability queries over
program locations are used to combine lower-level trace properties. The two-level
specification language can be used to break down a verification task into several
independent calls of the model-checking engine. In this way, each call to the
model checker may have to analyze only part of the program, or part of the specification,
and may thus succeed in a reduction of the number of predicates needed for the
analysis. In addition, the two-level specification language provides a means for
structuring and maintaining specifications. '
acknowledgement: This research was supported in part by the NSF grants CCR-0085949,
CCR-0234690, and ITR-0326577.
alternative_title:
- LNCS
author:
- first_name: Dirk
full_name: Beyer, Dirk
last_name: Beyer
- first_name: Adam
full_name: Chlipala, Adam J
last_name: Chlipala
- first_name: Thomas A
full_name: Thomas Henzinger
id: 40876CD8-F248-11E8-B48F-1D18A9856A87
last_name: Henzinger
orcid: 0000−0002−2985−7724
- first_name: Ranjit
full_name: Jhala, Ranjit
last_name: Jhala
- first_name: Ritankar
full_name: Majumdar, Ritankar S
last_name: Majumdar
citation:
ama: 'Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. The BLAST query language
for software verification. In: Vol 3148. Springer; 2004:2-18. doi:10.1007/978-3-540-27864-1_2'
apa: 'Beyer, D., Chlipala, A., Henzinger, T. A., Jhala, R., & Majumdar, R. (2004).
The BLAST query language for software verification (Vol. 3148, pp. 2–18). Presented
at the SAS: Static Analysis Symposium, Springer. https://doi.org/10.1007/978-3-540-27864-1_2'
chicago: Beyer, Dirk, Adam Chlipala, Thomas A Henzinger, Ranjit Jhala, and Ritankar
Majumdar. “The BLAST Query Language for Software Verification,” 3148:2–18. Springer,
2004. https://doi.org/10.1007/978-3-540-27864-1_2.
ieee: 'D. Beyer, A. Chlipala, T. A. Henzinger, R. Jhala, and R. Majumdar, “The BLAST
query language for software verification,” presented at the SAS: Static Analysis
Symposium, 2004, vol. 3148, pp. 2–18.'
ista: 'Beyer D, Chlipala A, Henzinger TA, Jhala R, Majumdar R. 2004. The BLAST query
language for software verification. SAS: Static Analysis Symposium, LNCS, vol.
3148, 2–18.'
mla: Beyer, Dirk, et al. The BLAST Query Language for Software Verification.
Vol. 3148, Springer, 2004, pp. 2–18, doi:10.1007/978-3-540-27864-1_2.
short: D. Beyer, A. Chlipala, T.A. Henzinger, R. Jhala, R. Majumdar, in:, Springer,
2004, pp. 2–18.
conference:
name: 'SAS: Static Analysis Symposium'
date_created: 2018-12-11T12:09:34Z
date_published: 2004-08-17T00:00:00Z
date_updated: 2021-01-12T07:59:50Z
day: '17'
doi: 10.1007/978-3-540-27864-1_2
extern: 1
intvolume: ' 3148'
month: '08'
page: 2 - 18
publication_status: published
publisher: Springer
publist_id: '130'
quality_controlled: 0
status: public
title: The BLAST query language for software verification
type: conference
volume: 3148
year: '2004'
...