Joint ICE-Rose and ICE-TCS lecture - by Frank de Boer - Abstract Object Creation in Dynamic Logic: To Be or Not To Be Created

The next ICE- TCS  talk for this semester is joint with ICE-Rose and will be delivered on Tuesday, the 18th of August, by Frank de Boer (CWI and Universiteit Utrecht, The Netherlands).

The talk, entitled "Abstract Object Creation in Dynamic Logic: To Be or Not To Be Created", will be held in room K5 at Reykjavík University (Kringlan 1) from 14:00 till 15:00.

ABSTRACT

I will present an integration of a weakest precondition calculus for abstract object creation in dynamic logic and the underlying theorem prover of the KeY tool.  This integration 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.