BibTeX Database Entries
@MISC{Platzer_2004,
author = {Andr{\'e} Platzer},
title = {Using a Program Verification Calculus for Constructing
Specifications from Implementations},
howpublished = {Minor thesis,
University of Karlsruhe, Department of Computer Science.
Institute for Logic, Complexity and Deduction Systems},
OPTmonth = {Feb},
year = {2004},
school = {University of Karlsruhe, Department of Computer Science.
Institute for Logic, Complexity and Deduction Systems},
pages = {83},
abstract = {
In this thesis we examine the possibility of automatically constructing
the program specification from an implementation, both from a theoretical
perspective and as a practical approach with a sequent calculus.
As a setting for program specifications we choose dynamic logic for
the Java programming language. We show that---despite the undecidable
nature of program analysis---the strongest specification of any program
can always be constructed algorithmically. Further we outline a practical
approach embedded into a sequent calculus for dynamic logic and with
a higher focus on readability. Therefor, the central aspect of describing
unbounded state changes incorporates the concept of modifies lists
for expressing the modifiable portion of the state space. The underlying
deductions are carried out by the theorem prover of the KeY System.},
pdf = {http://symbolaris.com/logic/Minoranthe.pdf},
}
@MASTERSTHESIS{Platzer_2004b,
author = {Andr{\'e} Platzer},
title = {An Object-oriented Dynamic Logic with Updates},
school = {University of Karlsruhe, Department of Computer Science.
Institute for Logic, Complexity and Deduction Systems},
year = {2004},
OPTmonth = {Sep},
pages = {193},
abstract = {
With the goal of this thesis being to create a dynamic logic for
object-oriented languages, ODL is developed along with a sound and
relatively complete calculus. The dynamic logic contains only the
absolute logical essentials of object-orientation, yet still allows a
``natural'' representation of all other features of common
object-oriented programming languages. ODL is an extension of a dynamic
logic for imperative While programs by function modification and dynamic
type checks. A generalisation of substitutions, called updates, constitute
the central technical device for dealing with object aliasing arising from
function modification and for retaining a manageable calculus in practical
application scenarios. Further, object enumerators realise object creation
in a natural yet powerful way. Finally, completeness is proven relative
to first-order arithmetic. Along with the soundness result, this
proof constitutes the central part of this thesis and even copes
with states containing uncomputable functions.},
pdf = {http://i12www.ira.uka.de/~key/doc/2004/odlMasterThesis.pdf},
}
@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 = {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 and
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.},
}
@INPROCEEDINGS{DBLP:journals/entcs/Platzer07,
author = {Andr{\'e} Platzer},
title = {Towards a Hybrid Dynamic Logic for Hybrid Dynamic Systems},
booktitle = {LICS International Workshop on Hybrid Logic, HyLo'06,
Seattle, USA, Proceedings},
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},
pdf = {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: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},
annote = {Appeared as UNU-IIST Report No.~344
\url{http://www.iist.unu.edu/newrh/III/1/docs/techreports/report344.html}},
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. We present a faithful embedding of bounded
model checking for systems of timed automata into
propositional logic with linear arithmetic and prove
correctness. With this logical representation, we achieve a
linear-size representation of parallel composition and
introduce a quick abstraction technique 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:conf/hybrid/Platzer07,
author = {Andr{\'e} Platzer},
title = {Differential Logic for Reasoning about Hybrid Systems},
booktitle = {HSCC},
longbooktitle = {Hybrid Systems: Computation and Control, 10th
International Conference, HSCC 2007, Pisa, Italy, Proceedings},
year = {2007},
pages = {746-749},
doi = {10.1007/978-3-540-71493-4_75},
editor = {Alberto Bemporad and Antonio Bicchi and Giorgio Buttazzo},
publisher = {Springer},
series = {LNCS},
volume = {4416},
isbn = {978-3-540-71492-7},
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},
booktitle = {HSCC},
longbooktitle = {Hybrid Systems: Computation and Control, 10th
International Conference, HSCC 2007, Pisa, Italy, Proceedings},
year = {2007},
pages = {473-486},
doi = {10.1007/978-3-540-71493-4_37},
editor = {Alberto Bemporad and Antonio Bicchi and Giorgio Buttazzo},
publisher = {Springer},
series = {LNCS},
volume = {4416},
isbn = {978-3-540-71492-7},
keywords = {model checking, hybrid systems, image computation},
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:conf/lfcs/Platzer07,
author = {Andr{\'e} Platzer},
title = {A Temporal Dynamic Logic for Verifying Hybrid System
Invariants},
booktitle = {LFCS},
longbooktitle = {Logical Foundations of Computer Science, 5th International
Symposium, LFCS'07, New York, USA, June 4-7, 2007,
Proceedings},
year = {2007},
pages = {457-471},
doi = {10.1007/978-3-540-72734-7_32},
editor = {Sergei N. Art{\"e}mov and
Anil Nerode},
publisher = {Springer},
series = {LNCS},
volume = {4514},
isbn = {978-3-540-72732-3},
keywords = {dynamic logic, temporal logic, sequent calculus, logic for
hybrid systems, 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.
}
}
@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 = {Feb},
editor = {Bernd Becker and
Werner Damm and
Martin Fr{\"a}nzle and
Ernst-R{\"u}diger Olderog and
Andreas Podelski and
Reinhard Wilhelm},
institution = {Reports of {SFB/TR~14 AVACS}},
OPTtype = {Reports of {SFB/TR~14 AVACS}},
series = {ATR},
note = {ISSN: 1860-9821, http://www.avacs.org.},
pdf={http://www.avacs.org/Publikationen/Open/avacs_technical_report_012.pdf},
}
@INPROCEEDINGS{Platzer2007Dagstuhl,
author = {Andr{\'e} Platzer},
title = {Differential Logic for Hybrid System Verification --
Reasoning about Interacting Discrete and Continuous Change},
booktitle = {Dagstuhl ``zehn plus eins'' -- Zehn
Informatik-Graduiertenkollegs und ein
Informatik-Forschungskolleg stellen sich vor},
year = {2007},
pages = {80},
address = {Aachen},
month = {Jun},
publisher = {Verlagshaus Mainz}
}
@INPROCEEDINGS{DBLP:conf/tableaux/Platzer07,
author = {Andr{\'e} Platzer},
title = {Differential Dynamic Logic for Verifying Parametric
Hybrid Systems.},
booktitle = {TABLEAUX},
longbooktitle = {Automated Reasoning with Analytic Tableaux and Related
Methods, 16th International Conference, TABLEAUX 2007,
Aix en Provence, France, July 3-6, 2007, Proceedings},
year = {2007},
pages = {216-232},
doi = {10.1007/978-3-540-73099-6_17},
editor = {Nicola Olivetti},
volume = {4548},
series = {LNCS},
publisher = {Springer},
isbn = {978-3-540-73098-9},
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.}
}
@TECHREPORT{DBLP:conf/tableaux/Platzer07:TR,
author = {Andr{\'e} Platzer},
title = {Differential Dynamic Logic for Verifying Parametric
Hybrid Systems.},
number = {15},
year = {2007},
month = {May},
editor = {Bernd Becker and
Werner Damm and
Martin Fr{\"a}nzle and
Ernst-R{\"u}diger Olderog and
Andreas Podelski and
Reinhard Wilhelm},
institution = {Reports of {SFB/TR~14 AVACS}},
OPTtype = {Reports of {SFB/TR~14 AVACS}},
series = {ATR},
note = {ISSN: 1860-9821, http://www.avacs.org.},
pdf={http://www.avacs.org/Publikationen/Open/avacs_technical_report_015.pdf},
}
@INPROCEEDINGS{DBLP:conf/verify/Platzer07,
author = {Andr{\'e} Platzer},
title = {Combining Deduction and Algebraic Constraints for Hybrid
System Analysis.},
booktitle = {VERIFY'07 at CADE, Bremen, Germany},
longbooktitle = {4th International Verification Workshop VERIFY'07,
at CADE-21, Bremen, Germany, July 15-16, 2007},
year = {2007},
pages = {164-178},
editor = {Bernhard Beckert},
volume = {259},
publisher = {CEUR-WS.org},
series = {CEUR Workshop Proceedings},
issn = {1613-0073},
pdf = {http://ceur-ws.org/Vol-259/paper14.pdf},
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.}
}
@INPROCEEDINGS{DBLP:conf/birthday/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},
booktitle = {Formal Methods and Hybrid Real-Time Systems},
longbooktitle = {Formal Methods and Hybrid Real-Time Systems, Essays in
Honor of Dines Bj{\o}rner and Chaochen Zhou on the
Occasion of Their 70th Birthdays},
year = {2007},
pages = {115-169},
doi = {10.1007/978-3-540-75221-9_6},
editor = {Cliff B. Jones and
Zhiming Liu and
Jim Woodcock},
publisher = {Springer},
series = {LNCS},
volume = {4700},
isbn = {978-3-540-75220-2},
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.},
}
@ARTICLE{DBLP:journals/jar/Platzer08,
author = {Andr{\'e} Platzer},
title = {Differential Dynamic Logic for Hybrid Systems.},
medjournal = {J. Autom. Reasoning},
journal = {J Autom Reas},
longjournal = {Journal of Automated Reasoning},
year = {2008},
volume = {41},
number = {2},
pages = {143-189},
doi = {10.1007/s10817-008-9103-8},
issn = {0168-7433},
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/hybrid/PlatzerQ08,
author = {Andr{\'e} Platzer and
Jan-David Quesel},
title = {Logical Verification and Systematic Parametric Analysis in
Train Control.},
booktitle = {HSCC},
longbooktitle = {Hybrid Systems: Computation and Control, 10th International
Conference, HSCC 2008, St. Louis, USA, Proceedings},
year = {2008},
pages = {646-649},
doi = {10.1007/978-3-540-78929-1_55},
editor = {Magnus Egerstedt and
Bud Mishra},
publisher = {Springer},
series = {LNCS},
volume = {4981},
isbn = {978-3-540-78928-4},
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.}
}
@ARTICLE{DBLP:journals/logcom/Platzer10,
author = {Andr{\'e} Platzer},
title = {Differential-Algebraic Dynamic Logic for
Differential-Algebraic Programs},
journal = {J. Log. Comput.},
longjournal = {Journal of Logic and Computation},
year = {2010},
volume = {20},
number = {1},
pages = {309-352},
note = {Advance Access published on November 18, 2008},
doi = {10.1093/logcom/exn070},
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.},
}
@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{Platzer2008Dagstuhl,
author = {Andr{\'e} Platzer},
title = {Differential Dynamic Logics. Automated Theorem Proving for
Hybrid Systems},
booktitle = {Proceedings des gemeinsamen Workshops der Graduiertenkollegs
2008, Dagstuhl},
year = {2008},
editor = {Malte Diehl and
Henrik Lipskoch and
Roland Meyer and
Christian Storm},
series = {Trustworthy Software Systems},
pages = {29},
address = {Berlin},
month = {may},
publisher = {Gito Verlag},
isbn = {978-3-940019-39-4},
location = {May 19--21, 2008, Dagstuhl, Germany}
}
@INPROCEEDINGS{DBLP:conf/cav/PlatzerC08,
author = {Andr{\'e} Platzer and
Edmund M. Clarke},
title = {Computing Differential Invariants of Hybrid Systems as
Fixedpoints},
booktitle = {CAV},
longbooktitle = {Computer Aided Verification, 20th International Conference,
CAV 2008, Princeton, NJ, USA, July 7-14, 2008, Proceedings},
year = {2008},
pages = {176-189},
month = {},
editor = {Aarti Gupta and
Sharad Malik},
publisher = {Springer},
series = {LNCS},
volume = {5123},
isbn = {978-3-540-70543-7},
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.}
}
@INPROCEEDINGS{DBLP:conf/cade/PlatzerQ08,
author = {Andr{\'e} Platzer and
Jan-David Quesel},
title = {{KeYmaera}: A Hybrid Theorem Prover for Hybrid Systems.},
booktitle = {IJCAR},
longbooktitle = {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},
isbn = {978-3-540-71069-1},
issn = {0302-9743},
subseries = {LNAI},
doi = {10.1007/978-3-540-71070-7_15},
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.}
}
@PHDTHESIS{Platzer08,
author = {Andr{\'e} Platzer},
title = {Differential Dynamic Logics:
Automated Theorem Proving for Hybrid Systems},
school = {Department of Computing Science, University of Oldenburg},
year = {2008},
pages = {299},
}
@INPROCEEDINGS{ClarkeKPR08,
author = {Edmund M. Clarke and
Bruce Krogh and
Andr{\'e} Platzer and
Raj Rajkumar},
title = {Analysis and Verification Challenges for Cyber-Physical
Transportation Systems},
year = {2008},
booktitle = {NITRD National Workshop for Research on Transportation
Cyber-Physical Systems: Automotive, Aviation, and Rail},
pdf =
{http://www.ee.washington.edu/research/nsl/aar-cps/AndrePlatzer-20081020163241.pdf},
abstract = {
Substantial technological and engineering advances in various
disciplines make it possible more than ever before to provide
autonomous control choices for cars, trains, and
aircraft. Correct automatic control can improve overall safety
tremendously. Yet, ensuring a safe operation of those control
assistants under all circumstances requires analysis techniques
that are prepared for the rising complexity resulting from
combinations of several computerized safety measures. We
identify cases where cyber-physical transportation systems pose
particularly demanding challenges for future research in formal
analysis techniques.
}
}
@ARTICLE{DBLP:journals/fmsd/PlatzerC09,
author = {Andr{\'e} Platzer and Edmund M. Clarke},
title = {Computing Differential Invariants of Hybrid Systems as
Fixedpoints},
journal = {Form. Methods Syst. Des.},
longjournal = {Formal Methods in System Design},
year = {2009},
volume = {35},
number = {1},
pages = {98-120},
doi = {10.1007/s10703-009-0079-8},
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. With this compositional approach
we exploit locality in system designs. 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 and car control.}
}
@INPROCEEDINGS{DBLP:conf/cade/PlatzerQR09,
author = {Andr{\'e} Platzer and
Jan-David Quesel and
Philipp R{\"u}mmer},
title = {Real World Verification},
booktitle = {CADE},
longbooktitle = {International Conference on Automated Deduction, CADE'09,
Montreal, Canada, Proceedings},
year = {2009},
pages = {485-501},
editor = {Renate A. Schmidt},
publisher = {Springer},
series = {LNCS},
volume = {5663},
doi = {10.1007/978-3-642-02959-2_35},
keywords = {real-closed fields, decision procedures, hybrid systems,
software verification},
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\"obner 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\"obner Bases and
semidefinite programming for the real Nullstellensatz that
outperforms the individual approaches on an interesting set of
problems.}
}
@ARTICLE{DBLP:journals/ki/Platzer10,
author = {Andr{\'e} Platzer},
title = {Differential Dynamic Logics:
Automated Theorem Proving for Hybrid Systems},
journal = {K\"unstliche Intelligenz},
year = {2010},
doi = {10.1007/s13218-010-0014-6},
abstract = {
Designing and analyzing hybrid systems, which are models for
complex physical systems, is expensive and error-prone. The
dissertation presented in this article introduces a verification
logic that is suitable for analyzing the behavior of hybrid
systems. It presents a proof calculus and a new deductive
verification tool for hybrid systems that has been used
successfully to verify aircraft and train control.}
}
@TECHREPORT{DBLP:conf/cmsb/JhaCLLPZ09:TR,
author = {Sumit Kumar Jha and
Edmund Clarke and
Christopher Langmead and
Axel Legay and
Andr{\'e} Platzer and
Paolo Zuliani},
title = {Statistical Model Checking for Complex Stochastic Models in
Systems Biology},
number = {CMU-CS-09-110},
year = {2009},
month = {},
institution = {School of Computer Science, Carnegie Mellon University},
address = {Pittsburgh, PA},
pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2009/CMU-CS-09-110.pdf}
}
@INPROCEEDINGS{DBLP:conf/cmsb/JhaCLLPZ09,
author = {Sumit Kumar Jha and
Edmund Clarke and
Christopher Langmead and
Axel Legay and
Andr{\'e} Platzer and
Paolo Zuliani},
title = {A {Bayesian} Approach to Model Checking Biological Systems},
booktitle = {CMSB},
year = {2009},
pages = {218-234},
editor = {Pierpaolo Degano and
Roberto Gorrieri},
longbooktitle = {Computational Methods in Systems Biology, 7th International
Conference, CMSB 2009, Bologna, Italy, Proceedings},
publisher = {Springer},
series = {LNCS},
volume = {5688},
doi = {10.1007/978-3-642-03845-7_15},
abstract = {
Recently, there has been considerable interest in the use of Model
Checking for Systems Biology. Unfortunately, the state space of
stochastic biological models is often too large for classical Model
Checking techniques. For these models, a statistical approach to Model
Checking has been shown to be an effective alternative. Extending our
earlier work, we present the first algorithm for performing statistical
Model Checking using Bayesian Sequential Hypothesis Testing. We show
that our Bayesian approach outperforms current statistical Model
Checking techniques, which rely on tests from Classical (aka
Frequentist) statistics, by requiring fewer system simulations. Another
advantage of our approach is the ability to incorporate prior Biological
knowledge about the model being verified. We demonstrate our algorithm
on a variety of models from the Systems Biology literature and show that
it enables faster verification than state-of-the-art techniques, even
when no prior knowledge is available.
}
}
@TECHREPORT{DBLP:conf/cade/PlatzerQR09:TR,
author = {Andr{\'e} Platzer and
Jan-David Quesel and
Philipp R{\"u}mmer},
title = {Real World Verification},
number = {52},
year = {2009},
month = {Jun},
editor = {Bernd Becker and
Werner Damm and
Martin Fr{\"a}nzle and
Ernst-R{\"u}diger Olderog and
Andreas Podelski and
Reinhard Wilhelm},
institution = {Reports of {SFB/TR~14 AVACS}},
OPTtype = {Reports of {SFB/TR~14 AVACS}},
series = {ATR},
note = {ISSN: 1860-9821, http://www.avacs.org.},
pdf={http://www.avacs.org/Publikationen/Open/avacs_technical_report_052.pdf},
}
@ARTICLE{DBLP:journals/expert/Platzer09,
author = {Andr{\'e} Platzer},
title = {Verification of Cyberphysical Transportation Systems},
journal = {IEEE Intelligent Systems},
volume = {24},
number = {4},
year = {2009},
pages = {10-13},
doi = {10.1109/MIS.2009.81},
issn = {1541-1672},
keywords = {cyber-physical transportation systems, train control,
air traffic control, logic-based analysis, verification},
abstract = {
Cyberphysical system technology has an important share in modern
intelligent transportation systems, including next generation
flight, rail, and car control. This control technology is
intended to help improve performance objectives like throughput
and improve overall system safety. To ensure that these
transportation systems operate correctly, new analysis
techniques are needed that consider physical movement combined
with computational control to establish properties like
collision freedom. Logic-based analysis can verify the correct
functioning of these cyberphysical systems.}
}
@INPROCEEDINGS{DBLP:conf/fm/PlatzerC09,
author = {Andr{\'e} Platzer and
Edmund M. Clarke},
title = {Formal Verification of Curved Flight Collision Avoidance
Maneuvers:
A Case Study},
booktitle = {FM},
year = {2009},
pages = {547-562},
doi = {10.1007/978-3-642-05089-3_35},
editor = {Ana Cavalcanti and
Dennis Dams},
longbooktitle = {FM 2009: Formal Methods, 16th International Symposium on
Formal Methods, Eindhoven, Netherlands, November 2-6, 2009,
Proceedings},
publisher = {Springer},
series = {LNCS},
volume = {5850},
keywords = {formal verification of hybrid systems, deduction,
air traffic control, logic for hybrid systems},
abstract = {
Aircraft collision avoidance maneuvers are important and complex
applications. Curved flight exhibits nontrivial continuous behavior. In
combination with the control choices during air traffic maneuvers, this
yields hybrid systems with challenging interactions of discrete and
continuous dynamics. As a case study illustrating the use of a new proof
assistant for a logic for nonlinear hybrid systems, we analyze collision
freedom of roundabout maneuvers in air traffic control, where
appropriate curved flight, good timing, and compatible maneuvering are
crucial for guaranteeing safe spatial separation of aircraft throughout
their flight. We show that formal verification of hybrid systems can
scale to curved flight maneuvers required in aircraft control
applications. We introduce a fully flyable variant of the roundabout
collision avoidance maneuver and verify safety properties by
compositional verification.
}
}
@TECHREPORT{DBLP:conf/fm/PlatzerC09:TR,
author = {Andr{\'e} Platzer and
Edmund M. Clarke},
title = {Formal Verification of Curved Flight Collision Avoidance
Maneuvers:
A Case Study},
number = {CMU-CS-09-147},
year = {2009},
month = {},
institution = {School of Computer Science, Carnegie Mellon University},
address = {Pittsburgh, PA},
pdf = {http://reports-archive.adm.cs.cmu.edu/anon/2008/CMU-CS-09-147.pdf}
}
@INPROCEEDINGS{DBLP:conf/icfem/PlatzerQ09,
author = {Andr{\'e} Platzer and
Jan-David Quesel},
title = {European Train Control System:
A Case Study in Formal Verification},
booktitle = {ICFEM},
year = {2009},
pages = {246-265},
doi = {10.1007/978-3-642-10373-5_13},
editor = {Karin Breitman and
Ana Cavalcanti},
longbooktitle = {Formal Methods and Software Engineering, 11th International
Conference on Formal Engineering Methods, ICFEM 2009,
Rio de Janeiro, Brasil, December 9-12, 2009. Proceedings},
booktitle = {ICFEM},
publisher = {Springer},
series = {LNCS},
volume = {5885},
isbn = {},
keywords = {formal verification of hybrid systems, train control,
theorem proving, parameter constraint identification,
disturbances},
abstract = {
Complex physical systems have several degrees of freedom. They only
work correctly when their control parameters obey corresponding
constraints. Based on the informal specification of the European Train
Control System (ETCS), we design a controller for its cooperation
protocol. For its free parameters, we successively identify
constraints that are required to ensure collision freedom. We formally
prove the parameter constraints to be sharp by characterizing them
equivalently in terms of reachability properties of the hybrid system
dynamics. Using our deductive verification tool KeYmaera, we formally
verify controllability, safety, liveness, and reactivity properties of
the ETCS protocol that entail collision freedom. We prove that the
ETCS protocol remains correct even in the presence of perturbation by
disturbances in the dynamics. We verify that safety is preserved when
a PI controlled speed supervision is used.}
}
@TECHREPORT{DBLP:conf/icfem/PlatzerQ09:TR,
author = {Andr{\'e} Platzer and
Jan-David Quesel},
title = {European Train Control System:
A Case Study in Formal Verification},
number = {54},
year = {2009},
month = {Sep},
editor = {Bernd Becker and
Werner Damm and
Martin Fr{\"a}nzle and
Ernst-R{\"u}diger Olderog and
Andreas Podelski and
Reinhard Wilhelm},
institution = {Reports of {SFB/TR~14 AVACS}},
OPTtype = {Reports of {SFB/TR~14 AVACS}},
series = {ATR},
note = {ISSN: 1860-9821, http://www.avacs.org.},
pdf={http://www.avacs.org/Publikationen/Open/avacs_technical_report_054.pdf},
}
@INPROCEEDINGS{DBLP:conf/hybrid/ZulianiPC10,
author = {Paolo Zuliani and
Andr{\'e} Platzer and
Edmund M. Clarke},
title = {Bayesian Statistical Model Checking with Application to
Stateflow/Simulink Verification.},
booktitle = {HSCC},
longbooktitle = {Hybrid Systems: Computation and Control, 13th International
Conference, HSCC 2010, Stockholm, Sweden, Proceedings},
year = {2010},
pages = {},
doi = {},
editor = {Karl-Henrik Johansson and
Wang Yi},
publisher = {ACM},
series = {},
volume = {},
year = {2010},
isbn = {},
}
Copyright of publications is with the publisher (and/or author) as indicated. Author's versions of papers are posted with permission of the publisher for your personal use. Not for redistribution or commercial purpose. Slides are copyright © by the author.