Abstract
The automation of verification techniques based on firstorder logic specifications has benefited greatly from verification infrastructures such as Boogie and Why. These offer an intermediate language that can express diverse language features and verification techniques, as well as back-end tools such as verification condition generators. However, these infrastructures are not well suited for verification techniques based on separation logic and other permission logics, because they do not provide direct support for permissions and because existing tools for these logics often prefer symbolic execution over verification condition generation. Consequently, tool support for these logics is typically developed independently for each technique, dramatically increasing the burden of developing automatic tools for permission-based verification. In this paper, we present a verification infrastructure whose intermediate language supports an expressive permission model natively. We provide tool support, including two back-end verifiers, one based on symbolic execution, and one on verification condition generation; this facilitates experimenting with the two prevailing techniques in automated verification. Various existing verification techniques can be implemented via this infrastructure, alleviating much of the burden of building permissionbased verifiers, and allowing the developers of higher-level techniques to focus their efforts at the appropriate level of abstraction. Show more
Permanent link
https://doi.org/10.3929/ethz-a-010151765Publication status
publishedPublisher
ETH-ZürichSubject
VERIFICATION (SOFTWARE ENGINEERING); VERIFIKATION (SOFTWARE ENGINEERING)Organisational unit
03653 - Müller, Peter / Müller, Peter
02150 - Dep. Informatik / Dep. of Computer Science
More
Show all metadata
ETH Bibliography
yes
Altmetrics