Asst. Prof. André Platzer
On this page:
back to the mainpage.
1
Publications (BibTeX Source)
@comment{{This file has been generated by bib2bib 1.91}}
@comment{{Command line: /usr/bin/bib2bib -q -ob platzer.bib -c 'author : "platzer" or publists : "platzer"' names-long.bib all.bib}}
@techreport{DBLP:conf/cade/PlatzerQR09:TR,
author = {Andr{\'e} Platzer and Jan-David Quesel and Philipp R{\"u}mmer},
title = {Real World Verification},
editor = {Bernd Becker and Werner Damm and Martin Fr{\"a}nzle and
Ernst-R{\"u}diger Olderog and Andreas Podelski and Reinhard
Wilhelm},
institution = {SFB/TR 14 AVACS},
subproject = {H3},
year = {2009},
month = {June},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
number = 52,
note = {ISSN: 1860-9821, http://www.avacs.org.},
access = {open},
abstract = {Scalable handling of real arithmetic is a crucial part of
the verification of hybrid systems, mathematical algorithms, and mixed
analog/digital circuits. Despite substantial advances in
verification technology, complexity issues with classical decision
procedures are still a major obstacle for formal verification of
real-world applications, e.g., in automotive and avionic
industries. To identify strengths and weaknesses, we examine state
of the art symbolic techniques and implementations for the
universal fragment of real-closed fields: approaches based on
quantifier elimination, Gr{\"o}bner Bases, and semidefinite
programming for the Positivstellensatz. Within a uniform context
of the verification tool KeYmaera, we compare these approaches
qualitatively and quantitatively on verification benchmarks from
hybrid systems, textbook algorithms, and on geometric problems.
Finally, we introduce a new decision procedure combining
Gr{\"o}bner Bases and semidefinite programming for the real
Nullstellensatz that outperforms the individual approaches on an
interesting set of problems.},
bibtex = {atr052.bib},
pdf = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_052.pdf}
}
@inproceedings{DBLP:conf/cade/PlatzerQR09,
author = {Andr{\'e} Platzer and Jan-David Quesel and Philipp R{\"u}mmer},
title = {Real World Verification},
booktitle = {Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, McGill University, Montreal, Canada, August 2 - 7, 2009, Proceedings},
editor = {Renate Schmidt},
publisher = {Springer},
series = {LNCS},
year = {2009},
note = {To appear},
abstract = {Scalable handling of real arithmetic is a crucial part of
the verification of hybrid systems, mathematical algorithms, and mixed
analog/digital circuits. Despite substantial advances in
verification technology, complexity issues with classical decision
procedures are still a major obstacle for formal verification of
real-world applications, e.g., in automotive and avionic
industries. To identify strengths and weaknesses, we examine state
of the art symbolic techniques and implementations for the
universal fragment of real-closed fields: approaches based on
quantifier elimination, Gr{\"o}bner Bases, and semidefinite
programming for the Positivstellensatz. Within a uniform context
of the verification tool KeYmaera, we compare these approaches
qualitatively and quantitatively on verification benchmarks from
hybrid systems, textbook algorithms, and on geometric problems.
Finally, we introduce a new decision procedure combining
Gr{\"o}bner Bases and semidefinite programming for the real
Nullstellensatz that outperforms the individual approaches on an
interesting set of problems.}
}
@article{DBLP:journals/logcom/Platzer08,
author = {Andr{\'e} Platzer},
title = {Differential-Algebraic Dynamic Logic for Differential-Algebraic Programs},
journal = {Journal of Logic and Computation},
year = {2008},
note = {Accepted for publication},
doi = {10.1093/logcom/exn070},
pdf = {http://symbolaris.com/pub/DAL.pdf},
keywords = {dynamic logic, differential constraints, sequent calculus, verification of hybrid systems, differential induction, theorem proving},
abstract = {
We generalise dynamic logic to a logic for
differential-algebraic programs, i.e., discrete programs
augmented with first-order differential-algebraic formulas as
continuous evolution constraints in addition to first-order
discrete jump formulas. These programs characterise interacting
discrete and continuous dynamics of hybrid systems elegantly and
uniformly. For our logic, we introduce a calculus over real
arithmetic with discrete induction and a new \emph{differential
induction} with which differential-algebraic programs can be
verified by exploiting their differential constraints
algebraically without having to solve them. We develop the
theory of differential induction and differential refinement and
analyse their deductive power. As a case study, we present
parametric tangential roundabout maneuvers in air traffic
control and prove collision avoidance in our calculus.}
}
@article{DBLP:journals/jar/Platzer08,
author = {Andr{\'e} Platzer},
title = {Differential Dynamic Logic for Hybrid Systems.},
journal = {Journal of Automated Reasoning},
year = {2008},
volume = {41},
number = {2},
pages = {143-189},
doi = {10.1007/s10817-008-9103-8},
pdf = {http://symbolaris.com/pub/freedL.pdf},
note = {\url{http://dx.doi.org/10.1007/s10817-008-9103-8}{(c)
Springer-Verlag}},
keywords = {dynamic logic, differential equations, sequent calculus, axiomatisation, automated theorem proving, verification of hybrid systems},
abstract = {
Hybrid systems are models for complex physical systems and are
defined as dynamical systems with interacting discrete
transitions and continuous evolutions along differential
equations. With the goal of developing a theoretical and
practical foundation for deductive verification of hybrid
systems, we introduce a dynamic logic for hybrid programs, which
is a program notation for hybrid systems. As a verification
technique that is suitable for automation, we introduce a free
variable proof calculus with a novel combination of real-valued
free variables and Skolemisation for lifting quantifier
elimination for real arithmetic to dynamic logic. The calculus
is compositional, i.e., it reduces properties of hybrid programs
to properties of their parts. Our main result proves that this
calculus axiomatises the transition behaviour of hybrid systems
completely relative to differential equations. In a case study
with cooperating traffic agents of the European Train Control
System, we further show that our calculus is well-suited for
verifying realistic hybrid systems with parametric system
dynamics.
}
}
@inproceedings{DBLP:conf/cade/PlatzerQ08,
author = {Andr{\'e} Platzer and
Jan-David Quesel},
title = {{KeYmaera}: A Hybrid Theorem Prover for Hybrid Systems.},
booktitle = {Automated Reasoning, Third International Joint Conference,
IJCAR 2008, Sydney, Australia, Proceedings},
year = {2008},
pages = {171-178},
editor = {Alessandro Armando and
Peter Baumgartner and
Gilles Dowek},
publisher = {Springer},
series = {LNCS},
volume = {5195},
doi = {10.1007/978-3-540-71070-7_15},
isbn = {10.1007/978-3-540-71070-7_15},
issn = {0302-9743},
keywords = {dynamic logic, automated theorem proving, decision procedures, computer algebra, verification of hybrid systems},
abstract = {
KeYmaera is a hybrid verification tool for hybrid systems that
combines deductive, real algebraic, and computer algebraic
prover technologies. It is an automated and interactive theorem
prover for a natural specification and verification logic for
hybrid systems. KeYmaera supports differential dynamic logic,
which is a real-valued first-order dynamic logic for hybrid
programs, a program notation for hybrid automata. For
automating the verification process, KeYmaera implements a
generalized free-variable sequent calculus and automatic proof
strategies that decompose the hybrid system specification
symbolically. To overcome the complexity of real arithmetic, we
integrate real quantifier elimination following an iterative
background closure strategy. Our tool is particularly suitable
for verifying parametric hybrid systems and has been used
successfully for verifying collision avoidance in case studies
from train control and air traffic management.},
note = {\url{http://dx.doi.org/10.1007/978-3-540-71070-7_15}{(c)
Springer-Verlag}},
url = {http://symbolaris.com/pub/KeYmaera.pdf}
}
@inproceedings{DBLP:conf/cav/PlatzerC08,
author = {Andr{\'e} Platzer and
Edmund M. Clarke},
title = {Computing Differential Invariants of Hybrid Systems as Fixedpoints},
year = {2008},
month = {},
editor = {Aarti Gupta and
Sharad Malik},
booktitle = {Computer-Aided Verification, CAV 2008, Princeton, USA, Proceedings},
publisher = {Springer},
series = {LNCS},
pages = {176-189},
volume = {5123},
isbn = {},
doi = {10.1007/978-3-540-70545-1_17},
keywords = {verification of hybrid systems, differential invariants, verification logic, fixedpoint engine},
abstract = {
We introduce a fixedpoint algorithm for verifying safety
properties of hybrid systems with differential equations whose
right-hand sides are polynomials in the state variables. In
order to verify nontrivial systems without solving their
differential equations and without numerical errors, we use a
continuous generalization of induction, for which our algorithm
computes the required differential invariants. As a means for
combining local differential invariants into global system
invariants in a sound way, our fixedpoint algorithm works with a
compositional verification logic for hybrid systems. To improve
the verification power, we further introduce a saturation
procedure that refines the system dynamics successively with
differential invariants until safety becomes provable. By
complementing our symbolic verification algorithm with a robust
version of numerical falsification, we obtain a fast and sound
verification procedure. We verify roundabout maneuvers in air
traffic management and collision avoidance in train control.},
pdf = {http://symbolaris.com/pub/fpdi.pdf},
note = {\url{http://dx.doi.org/10.1007/978-3-540-70545-1_17}{(c)
Springer-Verlag}}
}
@inproceedings{DBLP:conf/hybrid/PlatzerQ08,
author = {Andr{\'e} Platzer and
Jan-David Quesel},
title = {Logical Verification and Systematic Parametric Analysis in
Train Control.},
year = {2008},
pages = {646-649},
doi = {10.1007/978-3-540-78929-1_55},
editor = {Magnus Egerstedt and
Bud Mishra},
booktitle = {Hybrid Systems: Computation and Control, 10th International
Conference, HSCC 2008, St. Louis, USA, Proceedings},
publisher = {Springer},
series = {LNCS},
volume = {4981},
isbn = {},
keywords = {parametric verification, logic for hybrid systems, symbolic
decomposition},
abstract = {
We formally verify hybrid safety properties of cooperation
protocols in a fully parametric version of the European Train
Control System (ETCS). We present a formal model using hybrid
programs and verify correctness using our logic-based
decomposition procedure. This procedure supports free parameters
and parameter discovery, which is required to determine correct
design choices for free parameters of ETCS.},
url = {http://symbolaris.com/pub/ETCS-short.pdf},
note = {\url{http://dx.doi.org/10.1007/978-3-540-78929-1_55}{(c)
Springer-Verlag}}
}
@techreport{DBLP:conf/cav/PlatzerC08:TR,
author = {Andr{\'e} Platzer and
Edmund M. Clarke},
title = {Computing Differential Invariants of Hybrid Systems as Fixedpoints},
number = {CMU-CS-08-103},
year = {2008},
month = {},
institution = {School of Computer Science, Carnegie Mellon University},
address = {Pittsburgh, PA},
keywords = {verification of hybrid systems, differential invariants, verification logic, fixedpoint engine},
abstract = {
We introduce a fixedpoint algorithm for verifying safety
properties of hybrid systems with differential equations that
have right-hand sides that are polynomials in the state
variables. In order to verify non-trivial systems without
solving their differential equations and without numerical
errors, we use a continuous generalization of induction, for
which our algorithm computes the required differential
invariants. As a means for combining local differential
invariants into global system invariants in a sound way, our
fixedpoint algorithm works with a compositional verification
logic for hybrid systems. To improve the verification power, we
further introduce a saturation procedure that refines the system
dynamics successively with differential invariants until safety
becomes provable. By complementing our symbolic verification
algorithm with a robust version of numerical falsification, we
obtain a fast and sound verification procedure. We verify
roundabout maneuvers in air traffic management and collision
avoidance in train control.},
pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2008/CMU-CS-08-103.pdf}
}
@inproceedings{DBLP:conf/verify/Platzer07,
author = {Andr{\'e} Platzer},
title = {Combining Deduction and Algebraic Constraints for Hybrid System
Analysis.},
booktitle = {4th International Verification Workshop, VERIFY'07, Workshop at
Conference on Automated Deduction (CADE), Bremen, Germany},
year = {2007},
pages = {164-178},
editor = {Bernhard Beckert},
volume = {259},
publisher = {CEUR-WS.org},
series = {},
note = {\url{http://ceur-ws.org/Vol-259}{CEUR Workshop Proceedings}},
issn = {1613-0073},
keywords = {modular prover combination, analytic tableaux, verification of
hybrid systems, dynamic logic},
abstract = {
We show how theorem proving and methods for handling real
algebraic constraints can be combined for hybrid system
verification. In particular, we highlight the interaction of
deductive and algebraic reasoning that is used for handling the
joint discrete and continuous behaviour of hybrid systems. We
illustrate proof tasks that occur when verifying scenarios with
cooperative traffic agents. From the experience with these
examples, we analyse proof strategies for dealing with the
practical challenges for integrated algebraic and deductive
verification of hybrid systems, and we propose an iterative
background closure strategy.},
url = {http://symbolaris.com/pub/cdachsa.pdf}
}
@inproceedings{DammMOOPPSW07,
author = {Werner Damm and Alfred Mikschl and Jens Oehlerking and
Ernst-R{\"u}diger Olderog and Jun Pang and Andr{\'e} Platzer and Marc
Segelken and Boris Wirtz},
title = {Automating Verification of Cooperation, Control, and Design in
Traffic Applications.},
year = {2007},
pages = {115--169},
editor = {Cliff Jones and Zhiming Liu and Jim Woodcock},
booktitle = {Formal Methods and Hybrid Real-Time Systems},
publisher = {Springer-Verlag},
series = {LNCS},
volume = {4700},
doi = {10.1007/978-3-540-75221-9_6},
issn = {},
keywords = {},
abstract = {
We present a verification methodology for cooperating traffic
agents covering analysis of cooperation strategies, realization
of strategies through control, and implementation of control.
For each layer, we provide dedicated approaches to formal
verification of safety and stability properties of the design.
The range of employed verification techniques invoked to span
this verification space includes application of pre-verified
design patterns, automatic synthesis of Lyapunov functions,
constraint generation for parameterized designs, model-checking
in rich theories, and abstraction refinement. We illustrate
this approach with a variant of the European Train Control
System (ETCS), employing layer specific verification techniques
to layer specific views of an ETCS design.},
note = {\url{http://dx.doi.org/10.1007/978-3-540-75221-9_6}{(c)
Springer-Verlag}}
}
@inproceedings{DBLP:conf/tableaux/Platzer07,
author = {Andr{\'e} Platzer},
title = {Differential Dynamic Logic for Verifying Parametric Hybrid
Systems.},
pages = {216-232},
doi = {10.1007/978-3-540-73099-6_17},
keywords = {dynamic logic, sequent calculus, verification of parametric
hybrid systems, quantifier elimination},
abstract = {
We introduce a first-order dynamic logic for reasoning about
systems with discrete and continuous state transitions, and we
present a sequent calculus for this logic. As a uniform model,
our logic supports hybrid programs with discrete and
differential actions. For handling real arithmetic during
proofs, we lift quantifier elimination to dynamic logic. To
obtain a modular combination, we use side deductions for
verifying interacting dynamics. With this, our logic supports
deductive verification of hybrid systems with symbolic
parameters and first-order definable flows. Using our calculus,
we prove a parametric inductive safety constraint for speed
supervision in a train control system.},
booktitle = {Automated Reasoning with Analytic Tableaux and Related Methods,
International
Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6,
2007, Proceedings},
year = {2007},
editor = {Nicola Olivetti},
volume = {4548},
series = {LNCS},
publisher = {Springer-Verlag},
isbn = {},
note = {\url{http://dx.doi.org/10.1007/978-3-540-73099-6_17}{(c)
Springer-Verlag}},
url = {http://symbolaris.com/pub/dL.pdf}
}
@techreport{DBLP:conf/lfcs/Platzer07:TR,
author = {Andr{\'e} Platzer},
title = {A Temporal Dynamic Logic for Verifying Hybrid System
Invariants.},
number = {12},
year = {2007},
month = {February},
editor = {B. Becker and W. Damm and M. Fr{\"a}nzle and E.-R. Olderog
and A. Podelski and R. Wilhelm},
type = {Reports of SFB/TR 14 AVACS},
series = {ATR},
note = {ISSN: 1860-9821, http://www.avacs.org.},
url = {http://www.avacs.org/Publikationen/Open/avacs_technical_report_012.pdf},
}
@inproceedings{DBLP:conf/lfcs/Platzer07,
author = {Andr{\'e} Platzer},
title = {A Temporal Dynamic Logic for Verifying Hybrid System
Invariants.},
editor = {S. Artemov and A. Nerode},
doi = {10.1007/978-3-540-72734-7_32},
booktitle = {Logical Foundations of Computer Science, International
Symposium, LFCS 2007, New York, USA,
Proceedings},
publisher = {Springer},
series = {LNCS},
year = {2007},
pages = {457--471},
volume = {4514},
note = {\url{http://dx.doi.org/10.1007/978-3-540-72734-7_32}{(c)
Springer-Verlag}},
url = {http://symbolaris.com/pub/dTL.pdf},
keywords = {dynamic logic, sequent calculus, logic for hybrid systems,
temporal logic, deductive verification of embedded systems},
abstract = {
We combine first-order dynamic logic for reasoning about possible
behaviour of hybrid systems with temporal logic for reasoning
about the temporal behaviour during their operation. Our logic
supports verification of hybrid programs with first-order
definable flows and provides a uniform treatment of discrete and
continuous evolution. For our combined logic, we generalise the
semantics of dynamic modalities to refer to hybrid traces instead
of final states. Further, we prove that this gives a conservative
extension of dynamic logic. On this basis, we provide a modular
verification calculus that reduces correctness of temporal
behaviour of hybrid systems to non-temporal reasoning. Using this
calculus, we analyse safety invariants in a train control system
and symbolically synthesise parametric safety constraints.
}
}
@inproceedings{DBLP:conf/hybrid/Platzer07,
author = {Andr{\'e} Platzer},
title = {Differential Logic for Reasoning about Hybrid Systems.},
year = {2007},
editor = {A. Bemporad and A. Bicchi and G. Buttazzo},
booktitle = {Hybrid Systems: Computation and Control, 10th International
Conference, HSCC 2007, Pisa, Italy, Proceedings},
publisher = {Springer-Verlag},
series = {LNCS},
pages = {746--749},
doi = {10.1007/978-3-540-71493-4_75},
volume = {4416},
note = {\url{http://dx.doi.org/10.1007/978-3-540-71493-4_75}{(c)
Springer-Verlag}},
url = {http://symbolaris.com/pub/dL-short.pdf},
keywords = {dynamic logic, hybrid systems, parametric verification},
abstract = {
We propose a first-order dynamic logic for reasoning about hybrid
systems. As a uniform model for discrete and continuous evolutions
in hybrid systems, we introduce hybrid programs with differential
actions. Our logic can be used to specify and verify correctness
statements about hybrid programs, which are suitable for symbolic
processing by calculus rules. Using first-order variables, our
logic supports systems with symbolic parameters. With dynamic
modalities, it is prepared to handle multiple system components.
}
}
@inproceedings{DBLP:conf/hybrid/PlatzerC07,
author = {Andr{\'e} Platzer and Edmund M. Clarke},
title = {The Image Computation Problem in Hybrid Systems Model Checking.},
year = {2007},
doi = {10.1007/978-3-540-71493-4_37},
editor = {A. Bemporad and A. Bicchi and G. Buttazzo},
booktitle = {Hybrid Systems: Computation and Control, 10th International
Conference, HSCC 2007, Pisa, Italy, Proceedings},
publisher = {Springer-Verlag},
series = {LNCS},
pages = {473--486},
volume = {4416},
keywords = {model checking, hybrid systems, image computation},
note = {\url{http://dx.doi.org/10.1007/978-3-540-71493-4_37}{(c)
Springer-Verlag}},
url = {http://symbolaris.com/pub/happroximation.pdf},
abstract = {
In this paper, we analyze limits of approximation techniques for
(non-linear) continuous image computation in model checking hybrid
systems. In particular, we show that even a single step of
continuous image computation is not semidecidable numerically even
for a very restricted class of functions. Moreover, we show that
symbolic insight about derivative bounds provides sufficient
additional information for approximation refinement model
checking. Finally, we prove that purely numerical algorithms can
perform continuous image computation with arbitrarily high
probability. Using these results, we analyze the prerequisites for
a safe operation of the roundabout maneuver in air traffic
collision avoidance.
}
}
@inproceedings{DBLP:journals/entcs/KemperP07,
author = {Stephanie Kemper and Andr{\'e} Platzer},
title = {SAT-based Abstraction Refinement for Real-time Systems},
booktitle = {Formal Aspects of Component Software, Third International
Workshop, FACS 2006, Prague, Czech Republic, Proceedings},
year = {2007},
editor = {Frank S. de Boer and Vladimir Mencl},
journal = {Electr. Notes Theor. Comput. Sci.},
volume = {182},
series = {ENTCS},
issn = {1571-0661},
pages = {107-122},
doi = {10.1016/j.entcs.2006.09.034},
url = {http://symbolaris.com/pub/SAAtRe.pdf},
keywords = {abstraction refinement, model checking, real-time systems,
SAT, Craig interpolation},
abstract = {
In this paper, we present an abstraction refinement approach for
model checking safety properties of real-time systems using
SAT-solving. With a faithful embedding of bounded model checking
for systems of timed automata into propositional logic and linear
arithmetic, we achieve both, quick abstraction techniques and a
linear-size representation of parallel composition. In this
logical setting, we introduce an abstraction that works uniformly
for clocks, events, and states. When necessary, abstractions are
refined by analysing spurious counterexamples using a promising
extension of counterexample-guided abstraction refinement with
syntactic information about Craig interpolants. To support
generalisations, our overall approach identifies the algebraic and
logical principles required for logic-based abstraction
refinement.
}
}
@inproceedings{DBLP:journals/entcs/Platzer07,
author = {Andr{\'e} Platzer},
title = {Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems},
booktitle = {Proc., LICS International Workshop on Hybrid Logic, HyLo
2006, Seattle, USA},
year = {2007},
editor = {Patrick Blackburn and Thomas Bolander and Torben Bra\"{u}ner
and Valeria de Paiva and J{\o}rgen Villadsen},
series = {ENTCS},
journal = {Electr. Notes Theor. Comput. Sci.},
issn = {1571-0661},
volume = {174},
number = {6},
month = {Jun},
pages = {63-77},
doi = {10.1016/j.entcs.2006.11.026},
url = {http://symbolaris.com/pub/hdL.pdf},
keywords = {hybrid logic, dynamic logic, sequent calculus, compositional
verification, real-time hybrid dynamic systems},
abstract = {
We introduce a hybrid variant of a dynamic logic with continuous
state transitions along differential equations, and we present a
sequent calculus for this extended hybrid dynamic logic. With the
addition of satisfaction operators, this hybrid logic provides
improved system introspection by referring to properties of states
during system evolution. In addition to this, our calculus
introduces state-based reasoning as a paradigm for delaying
expansion of transitions using nominals as symbolic state
labels. With these extensions, our hybrid dynamic logic advances
the capabilities for compositional reasoning about (semialgebraic)
hybrid dynamic systems. Moreover, the constructive reasoning
support for goal-oriented analytic verification of hybrid dynamic
systems carries over from the base calculus to our extended
calculus.
}
}
@inproceedings{DBLP:conf/cade/BeckertP06,
author = {Bernhard Beckert and Andr{\'e} Platzer},
title = {Dynamic Logic with Non-rigid Functions: A Basis for
Object-oriented Program Verification},
booktitle = {Automated Reasoning, Third International Joint Conference,
IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings},
year = {2006},
editor = {U. Furbach and N. Shankar},
volume = {4130},
series = {LNCS},
subseries = {LNAI},
pages = {266--280},
doi = {10.1007/11814771_23},
issn = {0302-9743},
isbn = {3-540-37187-7},
publisher = {Springer-Verlag},
keywords = {dynamic logic, sequent calculus, program logic, software
verification, logical foundations of programming languages,
object-orientation},
note = {\url{http://dx.doi.org/10.1007/11814771_23}{(c)
Springer-Verlag}},
url = {http://symbolaris.com/pub/odl.pdf},
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.
}
}
