2009
Abstract Object Creation in Dynamic Logic
Publication
Publication
Presented at the
World Congress on Formal Methods, Eindhoven
In this paper we give a representation of 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.
| Additional Metadata | |
|---|---|
| Springer | |
| A. Cavalcanti , D.R. Dams | |
| Lecture Notes in Computer Science | |
| Modelling and Analysis of evolutionary structures for distributed services , Highly Adaptable and Trustworthy Software using Forma Methods | |
| World Congress on Formal Methods | |
| Organisation | Computer Security |
|
Grabe, I., de Boer, F., & Ahrendt, W. (2009). Abstract Object Creation in Dynamic Logic. In A. Cavalcanti & D. R. Dams (Eds.), Proceedings of 2nd World Congress on Formal Methods 2009 (16) (pp. 612–627). Springer. |
|