To be or not to be created: abstract object creation in dynamic logic

Wolfgang Ahrendt

Dept. of Computer Science and Engineering
Chalmers University of Technology

Thursday, 23 August 2012, 14:00
Cybernetica Bldg (Akadeemia tee 21), room B101

Slides from the talk [pdf]

Abstract: In this talk I present a weakest precondition calculus for abstract object creation in dynamic logic, the logic underlying the KeY theorem prover. This representation allows to both specify and verify properties of objects at the abstraction level of the (object-oriented) programming language. Objects which are not (yet) created never play any role, neither in the specification nor in the verification of properties. Further, we show how to symbolically execute abstract object creation.

(This is joint work with Frank de Boer and Immo Grabe.)

This talk is given the frame of the EU FP7 HATS project.

Tarmo Uustalu
Last update 19.9.2012