Dynamic Frames in Java Dynamic Logic

Reviewed Paper In Proceedings

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:

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.

BibTeX

@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}
}