@inproceedings{DBLP:conf/cade/BeckertP06,
pdf = {pub/odl.pdf},
slides = {pub/odl-slides.pdf},
author = {['Bernhard Beckert', 'André Platzer']},
title = {Dynamic Logic with Non-rigid Functions:
A Basis for Object-oriented Program
Verification.},
booktitle = {IJCAR},
longbooktitle = {Automated Reasoning, Third International
Joint Conference, IJCAR 2006, Seattle, WA,
USA, Proceedings},
year = {2006},
pages = {266-280},
doi = {10.1007/11814771_23},
editor = {['Ulrich Furbach', 'Natarajan Shankar']},
publisher = {Springer},
series = {LNCS},
volume = {4130},
isbn = {3-540-37187-7},
issn = {0302-9743},
subseries = {LNAI},
keywords = {dynamic logic, sequent calculus, program
logic, software verification, logical
foundations of programming languages,
object-orientation},
abstract = {
We introduce a dynamic logic that is enriched by
non-rigid functions, i.e., functions that may change
their value from state to state (during program
execution), and we present a (relatively) complete
sequent calculus for this logic. In conjunction with
dynamically typed object enumerators, non-rigid
functions allow to embed notions of object-orientation
in dynamic logic, thereby forming a basis for
verification of object-oriented programs. A semantical
generalisation of substitutions, called state update,
which we add to the logic, constitutes the central
technical device for dealing with object aliasing
during function modification. With these few
extensions, our dynamic logic captures the essential
aspects of the complex verification system KeY and,
hence, constitutes a foundation for object-oriented
verification with the principles of reasoning that
underly the successful KeY case studies.}
}