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

The work

AuthorsStijn de Gouw; Frank S. de Boer; Wolfgang Ahrendt; Richard Bubel
Editors
Typearticle
Year2016
Citekeygouw2016integrating

Where it appeared

Published inSoftware and Systems Modeling
Volume15
Issue4
Pages1117--1140

Identifiers

DOI10.1007/s10270-014-0446-9

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.

A copy is held

pdf, 1.7 MB. Not published — it may be under copyright. The facts and links here are.

How it got here

How it got hereagent via bibtex
Added2026-08-05 00:00 UTC
Approved bya person 2026-08-16 15:35 UTC

Filed under

ahrendt bubel deboer degouw verifying-real-java

Cite it as

@article{gouw2016integrating,
  title        = {Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic},
  author       = {Stijn de Gouw and Frank S. de Boer and Wolfgang Ahrendt and Richard Bubel},
  year         = {2016},
  journal      = {Software and Systems Modeling},
  volume       = {15},
  number       = {4},
  pages        = {1117--1140},
  doi          = {10.1007/s10270-014-0446-9},
}

This record lives at https://refs.drheap.org/gouw2016integrating/ and will keep doing so.