Home | english | Impressum | Sitemap | KIT

Dynamic Frames in Java Dynamic Logic

Dynamic Frames in Java Dynamic Logic
Autor(en):

Peter H. Schmitt
Mattias Ulbrich
Benjamin Weiß

Links:
Quelle:

International Conference on Formal Verification of Object-Oriented Software (FoVeOOS 2010), Paris, France. LNCS 6528, Springer, 2011

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},
  editor       = {Bernhard Beckert and Claude March{\'e}},
  booktitle    = {Revised Selected Papers, International Conference on Formal
Verification of Object-Oriented Software
(FoVeOOS 2010)},
volume = {6528},
  series       = {LNCS},
pages = {138--152},
  publisher    = {Springer},
year = {2011}
}
@techreport{SchmittEtAl2010,
author = {Peter H. Schmitt and Mattias Ulbrich and Benjamin Wei{\ss}},
title = {Dynamic Frames in {Java} Dynamic Logic: Formalisation and Proofs},
number = {2010-11},
institution = {Department of Computer Science, Karlsruhe Institute of Technology},
year = {2010}
}