Table of Contents 

Landmark Papers
A highlevel overview of the principles behind the logical foundations of cyberphysical systems are in an invited IJCAR paper [38]. A technical survey of many important aspects can be found in an invited LICS tutorial [22]. 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] based on [4,2]
 The first logic and the first relatively complete compositional proof calculus for hybrid games [35], including an expressiveness characterization.
 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].
 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]
 Differential radical invariants, which decide algebraic invariants of algebraic differential equations and give rise to an efficient procedure for generating algebraic invariants [28].
 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,37].
 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 [32,40].  Obstacle avoidance navigation for robotic ground vehicles [27]
 Medical robotic surgery system for skullbase surgery [26]
 Distributed adaptive cruise control for cars [17]
 Air traffic collision avoidance [11] with the first formal verification results for fully curved flight.
 European train control system protocol
ETCS [12]
Differential Dynamic Logics
The family of differential dynamic logics consists of a number of intimately related logics for different classes of multidynamic systems.Logic  Logic for Dynamical System  References 

dL  dLDifferential dynamic logic
for hybrid systems  [5,21,13,39] 
dGL  Differential game logic
for hybrid games  [35] 
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] 
QdL  Quantified differential dynamic logic
for distributed hybrid systems  [15,23] 
SdL  Stochastic differential dynamic logic
for stochastic hybrid systems  [19] 
dL_{h}  Hybridnominal differential dynamic logic
for hybrid systems  [2] 
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].
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 is presented at CADE [33,39], which 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].
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].
Publications (incomplete list)

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, 2016.
Special issue for selected papers from TACAS'15. © SpringerVerlag
[bib  pdf  doi  study  TACAS'15  abstract]

André Platzer.
A complete uniform substitution calculus for differential dynamic logic.
Journal of Automated Reasoning, 2016. © The author
[bib  pdf  doi  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. © SpringerVerlag
Invited paper.
[bib  pdf  doi  slides  abstract]

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

André Platzer.
Foundations of CyberPhysical Systems.
Lecture Notes, Computer Science Department, Carnegie Mellon University. 2016.
[bib  pdf  course  abstract]

André Platzer.
Differential game logic.
ACM Trans. Comput. Log. 17(1), pp. 1:11:52, 2015. © The author
[bib  pdf  doi  arXiv  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, CADE'15, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 527538. Springer, 2015. © SpringerVerlag
[bib  pdf  doi  slides  poster  tool  abstract]

André Platzer.
A uniform substitution calculus for differential dynamic logic.
In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE'15, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 467481. Springer, 2015. © SpringerVerlag
[bib  pdf  doi  slides  arXiv  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. © SpringerVerlag
[bib  pdf  doi  study  TR  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. © SpringerVerlag
[bib  pdf  doi  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. © SpringerVerlag
[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. © SpringerVerlag
[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. © SpringerVerlag
[bib  pdf  doi  slides  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, 2013. © The author
[bib  pdf  slides  study  eprint  talk  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  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. © SpringerVerlag
Invited paper.
[bib  pdf  doi  slides  abstract]

André Platzer.
Dynamic logics of dynamical systems.
arXiv:1205.4788, May 2012.
[bib  pdf  arXiv  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  eprint  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  eprint  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, CADE'11, Wroclaw, Poland, Proceedings, volume 6803 of LNCS, pp. 431445. Springer, 2011. © SpringerVerlag
[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. © SpringerVerlag
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. © SpringerVerlag
[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. © SpringerVerlag
[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  TR  abstract]

André Platzer.
Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics.
Springer, 2010. 426 p. ISBN 9783642145087.
[bib  book  eBook  doi  web]

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, Rio de Janeiro, Brasil, Proceedings, volume 5885 of LNCS, pp. 246265. Springer, 2009. © SpringerVerlag
[bib  pdf  doi  slides  study  TR  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. © SpringerVerlag
This paper was awarded the 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. © SpringerVerlag
[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  book  doi  web  abstract  slides]

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. © SpringerVerlag
[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. © SpringerVerlag
[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. © The author
Special issue for selected papers from TABLEAUX'07. Advance Access published on November 18, 2008 by Oxford University Press.
[bib  pdf  doi  study  abstract]

André Platzer.
Differential dynamic logic for hybrid systems.
Journal of Automated Reasoning, 41(2), pp. 143189, 2008. © SpringerVerlag
[bib  pdf  doi  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. © SpringerVerlag
This paper was awarded the 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, © SpringerVerlag
[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. © SpringerVerlag
[bib  pdf  doi  slides  abstract]