Dynamic frames in Java dynamic logic
The work
| Authors | Peter H. Schmitt; Mattias Ulbrich; Benjamin Weiß |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2011 |
| Citekey | schmitt2011dynamic |
Where it appeared
| Published in | International Conference on Formal Verification of Object-Oriented Software (FoVeOOS) |
|---|---|
| Publisher | Springer |
| Volume | 6528 |
| Pages | 138--152 |
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.
A copy is held
pdf, 416.6 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-08-05 00:00 UTC |
| Approved by | a person 2026-08-14 11:32 UTC |
Cite it as
@inproceedings{schmitt2011dynamic,
title = {Dynamic frames in Java dynamic logic},
author = {Peter H. Schmitt and Mattias Ulbrich and Benjamin Weiß},
year = {2011},
booktitle = {International Conference on Formal Verification of Object-Oriented Software (FoVeOOS)},
publisher = {Springer},
volume = {6528},
pages = {138--152},
}
This record lives at https://refs.drheap.org/schmitt2011dynamic/ and will keep doing so.