Verification condition generation for permission logics with abstract predicates and abstraction functions
Kassios, Ioannis T.
Summers, Alexander J.
Rights / licenseIn Copyright - Non-Commercial Use Permitted
Abstract predicates are the primary abstraction mechanism for program logics based on access permissions, such as separation logic and implicit dynamic frames. In addition to abstract predicates, it is useful to also support classical abstraction functions, for instance, to encode side-effect-free methods of the program and use them in specifications. However, combining abstract predicates and abstraction functions in a verification condition generator leads to subtle interactions, which complicate reasoning about heap modifications. Such complications may compromise soundness or cause divergence of the prover in the context of automated verification. In this paper, we present an encoding of abstract predicates and abstraction functions in the verification condition generator Boogie. Our encoding is sound and handles recursion in a way that is suitable for automatic verification using SMT solvers. It is implemented in the automatic verifier Chalice Show more
External linksSearch via SFX
Journal / seriesTechnical Report / Department of Computer Science, ETH Zurich
SubjectVERIFICATION (SOFTWARE ENGINEERING); PRÄDIKATENLOGIK (MATHEMATISCHE LOGIK); VERIFIKATION (SOFTWARE ENGINEERING); SEMANTIK VON PROGRAMMIERSPRACHEN + SYNTAX VON PROGRAMMIERSPRACHEN; PREDICATE LOGIC (MATHEMATICAL LOGIC); SEMANTICS OF PROGRAMMING LANGUAGES + SYNTAX OF PROGRAMMING LANGUAGES; SEMANTICS OF LOGICAL LANGUAGES (MATHEMATICAL LOGIC); SEMANTIK LOGISCHER SPRACHEN (MATHEMATISCHE LOGIK)
Organisational unit03653 - Müller, Peter / Müller, Peter
02150 - Dep. Informatik / Dep. of Computer Science
MoreShow all metadata