
Publications By Type or By Year or By Area or Guide 
Key Publications
Reading guide for select publications by André Platzer. This page provides pointers to the most important publications, as well as a short description of what to read when.

André Platzer.
Logical Foundations of CyberPhysical Systems.
Springer, Cham, 2018. 659 pages. ISBN 9783319635873.
[bib  ✂  doi  slides  video  book  web  errata  abstract]
This textbook is breaking with the myth that cyberphysical systems are too challenging to be taught at the undergraduate level. Teaching CPSrelated topics is notoriously challenging, but also creates an opportunity to discover and explore other areas of science with the intrinsic motivation it takes to succeed. This is the only textbook teaching undergraduate students the core principles behind CPS analysis. It shows them how to develop models and controls; identify safety specifications and critical properties; reason rigorously about CPS models; leverage multidynamical systems compositionality to tame CPS complexity; verify CPS models of appropriate scale in logic; and develop an intuition for operational effects. The textbook covers logic for hybrid systems, for differential equations, and for hybrid games, as well as comprehensive CPS correctness arguments. It is supported with homework exercises, YouTube lecture videos, and slides. 
André Platzer.
The complete proof theory of hybrid systems.
ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pp. 541550. IEEE 2012. © IEEE
[bib  ✂  pdf  doi  slides  TR  abstract]
Identifies a fundamental constructive prooftheoretical relationship equating discrete, continuous, and hybrid dynamical systems by provably equivalently reducing properties of hybrid systems in Differential Dynamic Logic to both continuous systems and also reducing them to discrete systems. This proves that Differential Dynamic Logic has a sound and complete axiomatization of hybrid systems relative to continuous systems as well as a sound and complete axiomatization of hybrid systems relative to discrete systems. This fundamental cornerstone sheds light on the nature of hybridness and enables flexible and provably perfect combinations of discrete reasoning with continuous reasoning that lift to all aspects of hybrid systems and their fragments. The result forms the underlying foundation for subsequent insights at JACM'20 exploiting completeness characterizations. 
André Platzer.
A complete uniform substitution calculus for differential dynamic logic.
Journal of Automated Reasoning 59(2), pp. 219265, 2017. © The author
[bib  ✂  pdf  doi  mypdf  arXiv  abstract]
Introduces a relatively complete proof calculus for Differential Dynamic Logic (dL) based entirely on uniform substitution. Uniform substitutions instantiate predicate symbols by formulas (due to Church for firstorder logic) and continue to shine for dL. They enable substantially simpler theorem provers (KeYmaera X) by reducing axiom/rule schemata to axioms. Introduces differentials, which are inspired by Élie Cartan's seminal differential forms, but depart in crucial ways to draw sound conclusions from syntactic manipulations mixing dynamic statements about differential equations and static statements about differentials. They enable axiomatic proofs for differential equations with modular reasoning about i) the effect of differential equations on the derivatives of state variables, ii) the effect of evolution domains on differential equations, iii) the temporal effect of differential equations, and iv) static equations of differential forms. 
André Platzer and Yong Kiam Tan.
Differential equation invariance axiomatization.
J. ACM 67(1), 6:16:66, 2020. © The authors
[bib  ✂  pdf  doi  mypdf  slides  video  arXiv  LICS'18  abstract]
Fundamental result proving completeness of the Differential Dynamic Logic axiomatization for differential equation invariants, i.e., all true real arithmetic invariants of polynomial differential equation systems are provable and all false ones are disprovable, giving a logical decision procedure. First, all true algebraic properties of polynomial differential equation systems are shown to be provable by exploiting differential ghosts, which introduce additional variables that can be chosen to evolve freely along new differential equations. Completeness for real arithmetic invariants then reduces to local progress properties using algebraic completeness. Thanks to the parsimonious axiomatization of Differential Dynamic Logic, soundness and completeness extend to Noetherian functions. 
Stefan Mitsch, Khalil Ghorbal, David Vogelbacher, and André Platzer.
Formal verification of obstacle avoidance and navigation of ground robots.
International Journal of Robotics Research 36(12), pp. 13121340, 2017. © The authors
[bib  ✂  pdf  doi  kyx  arXiv  abstract]
Applies Differential Dynamic Logic and KeYmaera X to answer fundamental safety questions for ground robot navigation by identifying under which circumstances which control decision makes a ground robot provably safely avoid both static and dynamic obstacles. Proves correctness of the resulting controllers for static safety, passive safety, passive friendly safety, and passive orientation safety. The paper proves safety despite limited sensor uncertainty and actuator disturbance and also proves liveness results for robot controllers. These safe controllers for mobile ground robots also form an important basis for safe autonomous driving or more generally making autonomous CPS on the ground safe.
Quickly: What to Read When
This page gives suggestions of what papers to read for what purposes. In a nutshell:
 Technical Survey:
 Invited Tutorial at LICS'12 [22] surveys many important aspects, easily readable.
 Exemplaric Survey:
 SCP [58] surveys some important aspects of differential dynamic logic and its siblings with prototypical examples and applications.
 Highlevel Survey:
 Invited Paper at IJCAR'16' [38] gives a brief manifesto for multidynamical systems.
 Comprehensive Reading:
 Textbook'18 [44] provides exceedingly readable and thorough material and videos. Comprehensive logical background on the sequent calculus of dL is in in the Book'10.
 Technical Development:
 Differential dynamic logic in JAR'17 [39] provides a rigorous development of modern differential dynamic logic and its parsimonious proof calculus.
 Differential Equation Invariants:
 differential equations axiomatization in LICS'18 and JACM'20 [46,51] provide complete differential equation invariant principles.
 Model Safety Transfer:
 ModelPlex verified runtime validation for verified CPS models [36] relates models to reality in provably correct ways establishing the fundamental link between models and reality/code/AI etc.
 Verified Compilation:
 VeriPhy verified controller executables from verified CPS models [45] to x64 or ARM.
 Hybrid Games:
 differential game logic [35] [41] for (differential) hybrid games, including constructive hybrid games [52].
 Distributed Hybrid Systems:
 quantified differential dynamic logic [23].
 Theory:
 complete proof theory of hybrid systems establishing how all true hybrid systems properties are provable from their atoms [5,21,39,46,51].
 Modeling Tutorial:
 KeYmaera modeling tutorial [31] and KeYmaera X Tutorial.
 Safe AI for CPS:
 Combines reinforcement learning optimality with differential dynamic logic safety for Safe AI for CPS [48,49].
Out of necessity, this quick list is hopelessly incomplete. Papers with additional background and papers on further topics are pointed to on the remainder of this page. For example, it can also be very effective to start reading up about an interesting case study.
Important Foundations
A highlevel overview of the principles behind the logical foundations of cyberphysical systems are in an IJCAR'16 invited paper [38]. A technical survey of many important aspects can be found in an LICS'12 invited tutorial [22]. A more recent survey based on examples is in the Science of Computer Programming 2025 [58]. The most important foundational landmark papers include the following:
 The logic, compositional proof calculus, and the first relative completeness result for hybrid systems in 2008 [5].
 The first logic and the first relatively complete compositional proof calculus for hybrid games [35], including an expressiveness characterization and with extensions to differential hybrid games [41].
 The first known complete proof calculus for propositional game logic, based on a complete propositional game logic extension with sabotage that is equiexpressive with the modal μcalculus [57].
 A study of the complete proof theory of hybrid systems [21], including a complete axiomatization of hybrid systems relative to discrete dynamics as well as a complete axiomatization relative to continuous dynamics.
These results prooftheoretically equate
discrete = continuous = hybrid systems by a constructive prooftheoretical approach.  An axiomatic form of differentialform differential dynamic logic with a uniform substitution calculus [33,39] gives a highly modular verification approach for hybrid systems enabling a lean implementation in KeYmaera X [34].
 A complete axiomatization of differential equation invariants [46,51] exploiting the flexibility of differentialform dL [39], differential invariants, differential cuts [9], and differential ghosts [20] to prove all true semianalytic invariants (and disprove all false ones).
 The article introducing differential invariants, differential variants, differential cuts, and a verification logic for more general hybrid systems and differentialalgebraic hybrid systems with differential inequalities and differentialalgebraic equations [6,9]. Including the subsequent extension to a procedure for computing differential invariants with differential cuts [7,10]
 A study of the structure of differential invariants and differential cut elimination, introducing differential auxiliaries (alias differential ghosts), and studying their proof theory [20], which were instrumental for JACM'20'.
 The first logic and the first relatively complete compositional proof calculus for distributed hybrid systems [15]
 ModelPlex, which is a systematic, proofbased way of ensuring that verified properties of CPS models apply to CPS implementations in a verifiably correct way [30,36].
 The first compositional verification approach and logic for stochastic hybrid systems [19], including proofs of measurability and welldefinedness.
Also see publications by area.
Important Applications
The most important applications and case studies that we have verified are NextGeneration Airborne Collision Avoidance System
ACAS X [40] and its game extension [55]  Obstacle avoidance navigation for robotic ground vehicles [43]
 Medical robotic surgery system for skullbase surgery [26]
 Distributed adaptive cruise control for cars [17]
 Roundabout air traffic conflict resolution [11] with the first formal verification results for fully curved flight.
 Safe controller for the Federal Railroad Administration kinematics model [54]
based on European train control system protocol
ETCS [12] and train control with air brake pressure propagation [42]
Differential Dynamic Logics
The family of differential dynamic logics consists of a number of intimately related logics for different classes of multidynamic systems.
The most important foundational logics are:
Logic  Logic for Dynamical System  References 

dL  Differential dynamic logic
for hybrid systems  [5,21,39] 
dGL  Differential game logic
for (differential) hybrid games  [35,41,52] 
QdL  Quantified differential dynamic logic
for distributed hybrid systems  [15,23] 
Further differential dynamic logics and extensions include:  
dRL  Differential refinement logic
for hybrid systems with system relations  [37,56] 
dL_{CHP}  Dynamic logic
for communicating hybrid programs with parallelism  [53] 
dHL  Hybridnominal differential dynamic logic
for hybrid systems whose nominals handle hyper properties  [2,47] 
DAL  Differentialalgebraic dynamic logic
for hybrid systems with differentialalgebraic programs, differentialalgebraic constraints, differential inequalities, disturbances etc.  [6,13] 
dTL  Differential temporal dynamic logic
for hybrid systems with temporal and throughout modalities  [13,29,50] 
SdL  Stochastic differential dynamic logic
for stochastic hybrid systems  [19] 
Publication Reading Guide
The primary paper on differential dynamic logic for hybrid systems verification appeared in the Journal of Automated Reasoning [5]. A broadly accessible invited tutorial on differential dynamic logic appeared at LICS [22]. A very intuitive but still rigorous development is in the textbook on logical foundations of cyberphysical systems [44]
For a first understanding the logical approach to hybrid systems verification, I also recommend the first conference paper [4], which introduces the first logic for hybrid systems that can be used to verify actual hybrid systems. This paper does not contain all details, but is a shorter read to start with. The major paper giving a detailed exploration of logic for hybrid systems verification and the theory behind KeYmaera, is the longer journal article [5]. This article also explains several aspects that are important for automation, including real generalizations of free variables and Skolem functions. This article is a breakthrough, because it presents and proves the first sound and complete axiomatization of hybrid systems relative to differential equations. This shows that hybrid systems verification can be reduced by recursive decomposition to elementary properties of differential equations. A followup breakthrough gave a sound and complete axiomatization of hybrid systems relative to discrete dynamics [21], thereby equating hybrid dynamics, continuous dynamics, and discrete dynamics, prooftheoretically. A corollary proves that numerical discretization and numerical differential equation solving can be used for hybrid systems verification without losing soundness.
An axiomatic form of differentialform differential dynamic logic with a uniform substitution calculus [33,39] leads to a very simple implementation [34].
A brief overview about the tool KeYmaera itself was reported later in a tool paper [8]. But this paper does not describe all capabilities of KeYmaera. It describes a very outdated version of KeYmaera and it only gives an overview of the features and refers to other articles for the actual verification techniques [5,6,13]. A more uptodate description on how to model and prove properties with KeYmaera can be found in a tutorial [31]. A more comprehensive survey on using logic for hybrid systems and the KeYmaera tool can be found in the CAV tutorial [18]. A more comprehensive survey on differential dynamic logic can be found in the LICS tutorial [22]. The new theorem prover KeYmaera X is described in a tool paper [34].
Another major step is the handling of more complex differential equations by an approach called differential invariants, which were first introduced in 2008 [6] and studied and extended subsequently [7,20,25]. This article also presents an advanced verification logic for hybrid systems that can even have disturbances and differential inequalities in the dynamics [6]. It has been the basis for subsequent automatic verification techniques to compute differential invariants [7,10]. Applications of these verification techniques have been described for air traffic control [11] and train control [12]. A comprehensive treatment of logic for hybrid systems, its theory, practice, and applications, can be found in a book [13] and a subsequent textbook [44].
Another interesting breakthrough [15] presents the first verification approach for distributed hybrid systems and a logic for distributed hybrid systems. This paper furthermore presents verification technique for reconfigurable distributed hybrid systems. Extensions to distributed hybrid systems with complicated continuous dynamics can be found in [16]
Numerical techniques and the image computation problem for hybrid systems are discussed in a paper at HSCC'07 [3]. This paper discusses the numerical decidability frontier for hybrid systems image computation. It further discusses computable versions of Weierstrass approximation theorems and their limits. The paper also shows that a stochastic view of hybrid systems, as later pursued in statistical model checking [14], is possible at all. A more comprehensive verification approach and logic for stochastic hybrid systems can be found in [19].
Select Publications

André Platzer.
Hybrid dynamical systems logic and its refinements.
Sci. Comput. Program. 239, pp. 103179, 2025. © The authors
[bib  ✂  doi  mypdf  abstract]

Noah Abou El Wafa and André Platzer.
Complete game logic with sabotage.
In Pawel Sobocinski, Ugo Dal Lago and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'24, pp. 1:11:15, ACM, 2024. © The authors
[bib  ✂  pdf  doi  slides  arXiv  abstract]

Enguerrand Prebet and André Platzer.
Uniform substitution for differential refinement logic.
In Christoph Benzmüller, Marijn J. Heule and Renate A. Schmidt, editors, Automated Reasoning, 12th International Joint Conference, IJCAR 2024, Proceedings, volume 14740 of LNCS. pp. 196215, Springer 2024. © The authors
[bib  ✂  pdf  doi  arXiv  abstract]

Rachel Cleveland, Stefan Mitsch and André Platzer.
Formally verified nextgeneration airborne collision avoidance games in ACAS X.
ACM Trans. Embed. Comput. Syst. 22(1), pp. 10:110:30, 2023. © The authors
[bib  ✂  pdf  doi  mypdf  kyx  arXiv  abstract]

Aditi Kabra, Stefan Mitsch and André Platzer.
Verified train controllers for the Federal Railroad Administration train kinematics model: Balancing competing brake and track forces.
IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 41(11), pp. 44094420, 2022. Special issue for EMSOFT 2022. © IEEE
Best paper finalist
[bib  ✂  pdf  doi  slides  video  kyx  extra  abstract]

Marvin Brieger, Stefan Mitsch and André Platzer.
Uniform substitution for dynamic logic with communicating hybrid programs.
In Brigitte Pientka and Cesare Tinelli, editors, International Conference on Automated Deduction, CADE29, Rome, Italy, Proceedings, volume 14132 of LNCS, pp. 96115. Springer, 2023. © The Authors
[bib  ✂  pdf  doi  slides  arXiv  abstract]

Brandon Bohrer and André Platzer.
Constructive hybrid games.
In Nicolas Peltier and Viorica SofronieStokkermans, editors, Automated Reasoning, 10th International Joint Conference, IJCAR 2020, Paris, France, Proceedings, Part I, volume 12166 of LNCS, pp. 454473. Springer 2020. © The authors
[bib  ✂  pdf  doi  mypdf  slides  arXiv  abstract]

André Platzer and Yong Kiam Tan.
Differential equation invariance axiomatization.
J. ACM 67(1), 6:16:66, 2020. © The authors
[bib  ✂  pdf  doi  mypdf  slides  video  arXiv  LICS'18  abstract]

Katherine Cordwell and André Platzer.
Towards physical hybrid systems.
In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE27, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 216232. Springer, 2019. © Springer
[bib  ✂  pdf  doi  slides  arXiv  abstract]

Nathan Fulton and André Platzer.
Verifiably safe offmodel reinforcement learning.
In Tomas Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2019, Proceedings, Part I, volume 11427 of LNCS, pp. 413430. Springer, 2019. © The authors
[bib  ✂  pdf  doi  arXiv  abstract]

Nathan Fulton and André Platzer.
Safe reinforcement learning via formal methods:
Toward safe control through proof and learning.
In Sheila A. McIlraith and Kilian Q. Weinberger, editors, AAAI Conference on Artificial Intelligence, pp. 64856492. AAAI 2018. © AAAI Press
[bib  ✂  pdf  eprint  slides  abstract]

Brandon Bohrer and André Platzer.
A hybrid, dynamic logic for hybriddynamic information flow.
In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, pp. 115124. ACM 2018. © The authors. Publication rights licensed to ACM
[bib  ✂  pdf  doi  slides  TR  abstract]

André Platzer and Yong Kiam Tan.
Differential equation axiomatization:
The impressive power of differential ghosts.
In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, pp. 819828. ACM 2018. © The authors
[bib  ✂  pdf  doi  mypdf  slides  video  arXiv  JACM'20  abstract]

Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen and André Platzer.
VeriPhy: Verified controller executables from verified cyberphysical system models.
In Dan Grossmann, editor, Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pp. 617630. ACM 2018. © The authors
[bib  ✂  pdf  doi  mypdf  slides  video  abstract]

André Platzer.
Logical Foundations of CyberPhysical Systems.
Springer, Cham, 2018. 659 pages. ISBN 9783319635873.
[bib  ✂  doi  slides  video  book  web  errata  abstract]

Stefan Mitsch, Khalil Ghorbal, David Vogelbacher, and André Platzer.
Formal verification of obstacle avoidance and navigation of ground robots.
International Journal of Robotics Research 36(12), pp. 13121340, 2017. © The authors
[bib  ✂  pdf  doi  kyx  arXiv  abstract]

Stefan Mitsch, Marco Gario, Christof J. Budnik, Michael Golm and André Platzer.
Formal verification of train control with air pressure brakes.
In Alessandro Fantechi, Thierry Lecomte and Alexander Romanovsky, editors, RSSRail 2017: Reliability, Safety, and Security of Railway Systems, volume 10598 of LNCS, pp. 173191. Springer, 2017. © Springer
[bib  ✂  pdf  doi  slides  abstract]

André Platzer.
Differential hybrid games.
ACM Trans. Comput. Log. 18(3), pp. 19:119:44, 2017. © The author
[bib  ✂  pdf  doi  mypdf  arXiv  abstract]

JeanBaptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Aurora Schmidt, Ryan Gardner, Stefan Mitsch, and André Platzer.
A formally verified hybrid system for safe advisories in the nextgeneration airborne collision avoidance system.
STTT 19(6), pp. 717741, 2017.
Special issue for selected papers from TACAS'15. © Springer
[bib  ✂  pdf  doi  kyx  study  TACAS'15  abstract]

André Platzer.
A complete uniform substitution calculus for differential dynamic logic.
Journal of Automated Reasoning 59(2), pp. 219265, 2017. © The author
[bib  ✂  pdf  doi  mypdf  arXiv  abstract]

André Platzer.
Logic & proofs for cyberphysical systems.
In Nicola Olivetti and Ashish Tiwari, editors, Automated Reasoning, 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, Proceedings, volume 9706 of LNCS, pp. 1521. Springer, 2016. © Springer
Invited paper.
[bib  ✂  pdf  doi  slides  abstract]

Sarah M. Loos and André Platzer.
Differential refinement logic.
ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, July 5–8, 2016, New York, NY, USA, pp. 505514. ACM, 2016. © The authors
[bib  ✂  pdf  doi  mypdf  slides  abstract]

Stefan Mitsch and André Platzer.
ModelPlex: Verified runtime validation of verified cyberphysical system models.
Formal Methods in System Design 49(1), pp. 3374. 2016.
Special issue for selected papers from RV'14. © The authors
[bib  ✂  pdf  doi  mypdf  RV'14  abstract]

André Platzer.
Differential game logic.
ACM Trans. Comput. Log. 17(1), pp. 1:11:52, 2015. © The author
[bib  ✂  pdf  doi  mypdf  arXiv  errata  abstract]

Nathan Fulton, Stefan Mitsch, JanDavid Quesel, Marcus Völp and André Platzer.
KeYmaera X: An aXiomatic tactical theorem prover for hybrid systems.
In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE25, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 527538. Springer, 2015. © Springer
[bib  ✂  pdf  doi  slides  poster  tool  tooldoi  abstract]

André Platzer.
A uniform substitution calculus for differential dynamic logic.
In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE25, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 467481. Springer, 2015. © Springer
[bib  ✂  pdf  doi  slides  arXiv  JAR'17  abstract]

JeanBaptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki, and André Platzer.
A formally verified hybrid system for the nextgeneration airborne collision avoidance system.
In Christel Baier and Cesare Tinelli, editors, Tools and Algorithms for the Construction and Analysis of Systems  21st International Conference, TACAS 2015, London, UK, April 1118, 2015, Proceedings, volume 9035 of LNCS, pp. 2136. Springer, 2015. © Springer
[bib  ✂  pdf  doi  study  TR  STTT'17  abstract]

JanDavid Quesel, Stefan Mitsch, Sarah Loos, Nikos Aréchiga, and André Platzer.
How to model and prove hybrid systems with KeYmaera: A tutorial on safety.
STTT 18(1), pp. 6791, 2016. © The authors
[bib  ✂  pdf  doi  mypdf  abstract]

Stefan Mitsch and André Platzer.
ModelPlex: Verified runtime validation of verified cyberphysical system models.
In Borzoo Bonakdarpour and Scott A. Smolka, editors, Runtime Verification  5th International Conference, RV 2014, Toronto, ON, Canada, September 2225, 2014. Proceedings, volume 8734 of LNCS, pp. 199214. Springer, 2014. © Springer
Best paper finalist
[bib  ✂  pdf  doi  slides  study  TR  FMSD'16  abstract]

JeanBaptiste Jeannin and André Platzer.
dTL^{2}: Differential temporal dynamic logic with nested temporalities for hybrid systems.
In Stéphane Demri, Deepak Kapur and Christoph Weidenbach, editors, Automated Reasoning, 7th International Joint Conference, IJCAR 2014, Vienna, Austria, July 1922, 2014, Proceedings, volume 8562 of LNCS, pp. 292306. Springer, 2014. © Springer
[bib  ✂  pdf  doi  slides  abstract]

Khalil Ghorbal and André Platzer.
Characterizing algebraic invariants by differential radical invariants.
In Erika Ábrahám and Klaus Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014, Proceedings, volume 8413 of LNCS, pp. 279294. Springer, 2014. © Springer
[bib  ✂  pdf  doi  slides  study  TR  abstract]

Stefan Mitsch, Khalil Ghorbal and André Platzer.
On provably safe obstacle avoidance for autonomous robotic ground vehicles.
In Paul Newman, Dieter Fox, and David Hsu, editors, Robotics: Science and Systems, RSS 2013. © The author
[bib  ✂  pdf  eprint  slides  video  study  IJRR'17  abstract]

Yanni Kouskoulas, David W. Renshaw, André Platzer and Peter Kazanzides.
Certifying the safe design of a virtual fixture control algorithm for a surgical robot.
In Calin Belta and Franjo Ivancic, editors, Hybrid Systems: Computation and Control (part of CPS Week 2013), HSCC'13, Philadelphia, PA, USA, April 813, 2013, pp. 263272. ACM, 2013. © ACM
[bib  ✂  pdf  doi  slides  study  abstract]

André Platzer.
A differential operator approach to equational differential invariants.
In Lennart Beringer and Amy Felty, editors, Interactive Theorem Proving, International Conference, ITP 2012, August 1315, Princeton, USA, Proceedings, volume 7406 of LNCS, pp. 2848. Springer, 2012. © Springer
Invited paper.
[bib  ✂  pdf  doi  slides  abstract]

André Platzer.
Dynamic logics of dynamical systems.
arXiv:1205.4788, May 2012. Long version of LICS'12 invited tutorial.
[bib  ✂  pdf  arXiv  LICS'12  abstract]

André Platzer.
A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems.
Logical Methods in Computer Science 8(4), pp. 144, 2012.
Special issue for selected papers from CSL'10. © The author
[bib  ✂  pdf  doi  arXiv  CSL'10  abstract]

André Platzer.
Logics of dynamical systems.
ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pp. 1324. IEEE 2012. © IEEE
Invited paper.
[bib  ✂  pdf  doi  slides  abstract]

André Platzer.
The complete proof theory of hybrid systems.
ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pp. 541550. IEEE 2012. © IEEE
[bib  ✂  pdf  doi  slides  TR  abstract]

André Platzer.
The structure of differential invariants and differential cut elimination.
Logical Methods in Computer Science 8(4), pp. 138, 2012. © The author
[bib  ✂  pdf  doi  mypdf  arXiv  abstract]

André Platzer.
Stochastic differential dynamic logic for stochastic hybrid programs.
In Nikolaj Bjørner and Viorica SofronieStokkermans, editors, International Conference on Automated Deduction, CADE23, Wroclaw, Poland, Proceedings, volume 6803 of LNCS, pp. 446460. Springer, 2011. © Springer
[bib  ✂  pdf  doi  slides  TR  abstract]

André Platzer.
Logic and compositional verification of hybrid systems.
In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification, CAV 2011, Snowbird, UT, USA, Proceedings, volume 6806 of LNCS, pp. 2843. Springer, 2011. © Springer
Invited tutorial.
[bib  ✂  pdf  doi  slides  abstract]

Sarah M. Loos, André Platzer and Ligia Nistor.
Adaptive cruise control:
Hybrid, distributed, and now formally verified.
In Michael Butler and Wolfram Schulte, editors, 17th International Symposium on Formal Methods, FM, Limerick, Ireland, Proceedings, volume 6664 of LNCS, pp. 4256. Springer, 2011. © Springer
[bib  ✂  pdf  doi  slides  study  TR  abstract]

André Platzer.
Quantified differential invariants.
In Emilio Frazzoli and Radu Grosu, editors, Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, USA, April 1214, pp. 6372. ACM, 2011. © ACM
[bib  ✂  pdf  doi  slides  abstract]

André Platzer.
Quantified differential dynamic logic for distributed hybrid systems.
In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 19th EACSL Annual Conference, CSL 2010, Brno, Czech Republic, August 2327, 2010. Proceedings, volume 6247 of LNCS, pp. 469483. Springer, 2010. © Springer
[bib  ✂  pdf  doi  slides  TR  LMCS'12  abstract]

Paolo Zuliani, André Platzer and Edmund M. Clarke.
Bayesian statistical model checking with application to Simulink/Stateflow verification.
In Karl Henrik Johansson and Wang Yi, editors, Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, April 1215, pp. 243252. ACM, 2010. © ACM
[bib  ✂  pdf  doi  slides  TR  abstract]

André Platzer.
Logical Analysis of Hybrid Systems:
Proving Theorems for Complex Dynamics.
Springer, Heidelberg, 2010. 426 pages. ISBN 9783642145087.
[bib  ✂  doi  book  web  errata  abstract]

André Platzer and JanDavid Quesel.
European Train Control System: A case study in formal verification.
In Karin Breitman and Ana Cavalcanti, editors, 11th International Conference on Formal Engineering Methods, ICFEM'09, Rio de Janeiro, Brasil, Proceedings, volume 5885 of LNCS, pp. 246265. Springer, 2009. © Springer
[bib  ✂  pdf  doi  slides  kyx  TR  old  abstract]

André Platzer and Edmund M. Clarke.
Formal verification of curved flight collision avoidance maneuvers: A case study.
In Ana Cavalcanti and Dennis Dams, editors, 16th International Symposium on Formal Methods, FM, Eindhoven, Netherlands, Proceedings, volume 5850 of LNCS, pp. 547562. Springer, 2009. © Springer
FM Best Paper Award.
[bib  ✂  pdf  doi  slides  study  TR  abstract]

André Platzer and Edmund M. Clarke.
Computing differential invariants of hybrid systems as fixedpoints.
Formal Methods in System Design 35(1), pp. 98120, 2009.
Special issue for selected papers from CAV'08. © Springer
[bib  ✂  pdf  doi  study  CAV'08  abstract]

André Platzer.
Differential Dynamic Logics:
Automated Theorem Proving for Hybrid Systems.
PhD Thesis, Department of Computing Science, University of Oldenburg, 2008.
ACM Doctoral Dissertation Honorable Mention Award in 2009.
Extended version appeared as book Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics, Springer, 2010.
[bib  ✂  pdf  eprint  slides  book  ebook  abstract]

André Platzer and JanDavid Quesel.
KeYmaera: A hybrid theorem prover for hybrid systems.
In Alessandro Armando, Peter Baumgartner and Gilles Dowek, editors, Automated Reasoning, Fourth International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings, volume 5195 of LNCS, pp. 171178. Springer, 2008. © Springer
[bib  ✂  pdf  doi  slides  tool  abstract]

André Platzer and Edmund M. Clarke.
Computing differential invariants of hybrid systems as fixedpoints.
In Aarti Gupta and Sharad Malik, editors, Computer Aided Verification, CAV 2008, Princeton, USA, Proceedings, volume 5123 of LNCS, pp. 176189, Springer, 2008. © Springer
[bib  ✂  pdf  doi  slides  study  TR  FMSD'09  abstract]

André Platzer.
Differentialalgebraic dynamic logic for differentialalgebraic programs.
Journal of Logic and Computation 20(1), pp. 309352, 2010.
Special issue for selected papers from TABLEAUX'07. © The author
[bib  ✂  pdf  doi  eprint  study  errata  TABLEAUX'07  abstract]

André Platzer.
Differential dynamic logic for hybrid systems.
Journal of Automated Reasoning 41(2), pp. 143189, 2008. © The author
[bib  ✂  pdf  doi  mypdf  study  abstract]

André Platzer.
Differential dynamic logic for verifying parametric hybrid systems.
In Nicola Olivetti, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2007, Aix en Provence, France, July 36, 2007, Proceedings, volume 4548 of LNCS, pp. 216232. Springer, 2007. © Springer
TABLEAUX Best Paper Award.
[bib  ✂  pdf  doi  slides  study  TR  abstract]

André Platzer and Edmund M. Clarke.
The image computation problem in hybrid systems model checking.
In Alberto Bemporad, Antonio Bicchi and Giorgio Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pp. 473486. Springer, 2007, © Springer
[bib  ✂  pdf  doi  slides  tool  abstract]

André Platzer.
Towards a hybrid dynamic logic for hybrid dynamic systems.
In Patrick Blackburn, Thomas Bolander, Torben Braüner, Valeria de Paiva and Jørgen Villadsen, editors, Proc., International Workshop on Hybrid Logic, HyLo 2006, Seattle, USA, Electr. Notes Theor. Comput. Sci. 174(6):6377, 2007.
[bib  ✂  pdf  doi  slides  abstract]

Bernhard Beckert and André Platzer.
Dynamic logic with nonrigid functions:
A basis for objectoriented program verification.
In Uli Furbach and Natarajan Shankar, editors, Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 1720, 2006, Proceedings, volume 4130 of LNCS, pp. 266280. Springer, 2006. © Springer
[bib  ✂  pdf  doi  slides  abstract]