Verifying safety properties using separation and heterogeneous abstractions
- 9 June 2004
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 39 (6), 25-34
- https://doi.org/10.1145/996893.996846
Abstract
In this paper, we show how separation (decomposing a verification problem into a collection of verification subproblems) can be used to improve the efficiency and precision of verification of safety properties. We present a simple language for specifying separation strategies for decomposing a single verification problem into a set of subproblems. (The strategy specification is distinct from the safety property specification and is specified separately.) We present a general framework of heterogeneous abstraction that allows different parts of the heap to be abstracted using different degrees of precision at different points during the analysis. We show how the goals of separation (i.e., more efficient verification) can be realized by first using a separation strategy to transform (instrument) a verification problem instance (consisting of a safety property specification and an input program), and by then utilizing heterogeneous abstraction during the verification of the transformed verification problem.Keywords
This publication has 9 references indexed in Scilit:
- Finite Differencing of Logical Formulas for Static AnalysisLecture Notes in Computer Science, 2003
- Extended static checking for JavaPublished by Association for Computing Machinery (ACM) ,2002
- ESPPublished by Association for Computing Machinery (ACM) ,2002
- Deriving specialized program analyses for certifying component-client conformancePublished by Association for Computing Machinery (ACM) ,2002
- Flow-sensitive type qualifiersPublished by Association for Computing Machinery (ACM) ,2002
- Parametric shape analysis via 3-valued logicACM Transactions on Programming Languages and Systems, 2002
- Enforcing high-level protocols in low-level softwarePublished by Association for Computing Machinery (ACM) ,2001
- BanderaPublished by Association for Computing Machinery (ACM) ,2000
- Typestate: A programming language concept for enhancing software reliabilityIEEE Transactions on Software Engineering, 1986