@INPROCEEDINGS{SchmittEtAl2011,
author = {Peter H. Schmitt and Mattias Ulbrich and Benjamin Wei{\ss}},
title = {Dynamic Frames in {Java} Dynamic Logic},
booktitle = {International Conference on Formal Verification
of Object-Oriented Software (FoVeOOS 2010), Revised Selected Papers},
year = {2011},
month = may,
editor = {Bernhard Beckert and Claude March{\'e}},
volume = {6528},
series = {LNCS},
pages = {138--152},
publisher = {Springer},
abstract = {In this paper we present a realisation of the concept of dynamic frames
in a dynamic logic for verifying Java programs. This is achieved
by treating sets of heap locations as first class citizens in the
logic. Syntax and formal semantics of the logic are presented, along
with sound proof rules for modularly reasoning about method calls
and heap dependent symbols using specification contracts.},
doi = {10.1007/978-3-642-18070-5_10},
links = {Technical Report:http://i57www.ira.uka.de/~ulbrich/publication.php?SchmittEtAl2010},
url = {http://lfm.iti.kit.edu/files/publications/FoVeOOS10.pdf}
}
Dynamic Frames in Java Dynamic Logic
| Author(s): | Peter H. Schmitt, Mattias Ulbrich, and Benjamin Weiß |
|---|---|
| In: | International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Revised Selected Papers |
| Publisher: | Springer |
| Series: | LNCS |
| Volume: | 6528 |
| Year: | 2011 |
| Pages: | 138-152 |
| Preprint/PDF: | SchmittEtAl2011.pdf |
| URL: | http://lfm.iti.kit.edu/files/publications/FoVeOOS10.pdf |
| DOI: | 10.1007/978-3-642-18070-5_10 |
| Links: | Technical Report |
Abstract
In this paper we present a realisation of the concept of dynamic frames in a dynamic logic for verifying Java programs. This is achieved by treating sets of heap locations as first class citizens in the logic. Syntax and formal semantics of the logic are presented, along with sound proof rules for modularly reasoning about method calls and heap dependent symbols using specification contracts.