Integrating Deductive Verification and Symbolic Execution for Abstract Object Creation in Dynamic Logic

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

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 are 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.