Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic

Stijn de Gouw, Frank S. de Boer, Wolfgang Ahrendt, Richard Bubel

Research output: Contribution to journalArticleAcademicpeer-review

Abstract

We present a fully abstract weakest precondition calculus and its integration with symbolic execution. Our assertion language allows both specifying and verifying properties of objects at the abstraction level of the programming language, abstracting from a specific implementation of object creation. Objects which are not (yet) created never play any role. The corresponding proof theory is discussed and justified formally by soundness theorems. The usage of the assertion language and proof rules is illustrated with an example of a linked list reachability property. All proof rules presented are fully implemented in a version of the KeY verification system for Java programs.
Original languageEnglish
Pages (from-to)1117-1140
Number of pages24
JournalSoftware and System Modeling
Volume15
Issue number4
DOIs
Publication statusPublished - 2016
Externally publishedYes

Fingerprint

Symbolic Execution
Dynamic Logic
Computer programming languages
Assertion
Proof Theory
Precondition
Soundness
Reachability
Java
Programming Languages
Calculus
Theorem
Object
Language

Cite this

Gouw, Stijn de ; Boer, Frank S. de ; Ahrendt, Wolfgang ; Bubel, Richard. / Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic. In: Software and System Modeling. 2016 ; Vol. 15, No. 4. pp. 1117-1140.
@article{129d14570a0a489289c92384bb87db34,
title = "Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic",
abstract = "We present a fully abstract weakest precondition calculus and its integration with symbolic execution. Our assertion language allows both specifying and verifying properties of objects at the abstraction level of the programming language, abstracting from a specific implementation of object creation. Objects which are not (yet) created never play any role. The corresponding proof theory is discussed and justified formally by soundness theorems. The usage of the assertion language and proof rules is illustrated with an example of a linked list reachability property. All proof rules presented are fully implemented in a version of the KeY verification system for Java programs.",
author = "Gouw, {Stijn de} and Boer, {Frank S. de} and Wolfgang Ahrendt and Richard Bubel",
year = "2016",
doi = "10.1007/s10270-014-0446-9",
language = "English",
volume = "15",
pages = "1117--1140",
journal = "Software and Systems Modeling",
issn = "1619-1366",
publisher = "Springer Verlag",
number = "4",

}

Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic. / Gouw, Stijn de; Boer, Frank S. de; Ahrendt, Wolfgang; Bubel, Richard.

In: Software and System Modeling, Vol. 15, No. 4, 2016, p. 1117-1140.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic

AU - Gouw, Stijn de

AU - Boer, Frank S. de

AU - Ahrendt, Wolfgang

AU - Bubel, Richard

PY - 2016

Y1 - 2016

N2 - We present a fully abstract weakest precondition calculus and its integration with symbolic execution. Our assertion language allows both specifying and verifying properties of objects at the abstraction level of the programming language, abstracting from a specific implementation of object creation. Objects which are not (yet) created never play any role. The corresponding proof theory is discussed and justified formally by soundness theorems. The usage of the assertion language and proof rules is illustrated with an example of a linked list reachability property. All proof rules presented are fully implemented in a version of the KeY verification system for Java programs.

AB - We present a fully abstract weakest precondition calculus and its integration with symbolic execution. Our assertion language allows both specifying and verifying properties of objects at the abstraction level of the programming language, abstracting from a specific implementation of object creation. Objects which are not (yet) created never play any role. The corresponding proof theory is discussed and justified formally by soundness theorems. The usage of the assertion language and proof rules is illustrated with an example of a linked list reachability property. All proof rules presented are fully implemented in a version of the KeY verification system for Java programs.

U2 - 10.1007/s10270-014-0446-9

DO - 10.1007/s10270-014-0446-9

M3 - Article

VL - 15

SP - 1117

EP - 1140

JO - Software and Systems Modeling

JF - Software and Systems Modeling

SN - 1619-1366

IS - 4

ER -