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.