
DownloadKeYmaera
or KeYmaera X or Source 
Overview
Differential dynamic logic (dL) [5,7,26,44] is a logic for specifying and verifying hybrid systems.
The logic dL can be used to specify correctness properties for hybrid systems given operationally as
The basic idea for dL formulas is to have formulas of the form [α]φ to specify that the hybrid system α always remains within region φ, i.e., all states reachable by following the transitions of hybrid system α satisfy the formula φ. Dually, the dL formula <α>φ expresses that the hybrid system α is able to reach region φ, i.e., there is a state reachable by following the transitions of hybrid system α that statisfies the formula φ. In either case, the hybrid system α is given as a full operational model in terms of a hybrid program. Using other propositional connectives, one can state the following dL formula
In much the same way as finite automata can be represented as whileprograms, or timed automata have a notation as realtime programs, we use a hybrid program notation for hybrid automata. Essentially, hybrid programs are what you get when you add continuous evolutions as a primitive operation to conventional discrete programs or, in fact, your favorite programming language.
Note: LaTeX typesets dL as follows:
\text{\upshape\textsf{d{\kern0.05em}L}}
Syntax
Note that the syntax of the differential dynamic logic dL given here uses slightly simplified notation in comparison to the full syntax in KeYmaera verification tool. The notation in KeYmaera and KeYmaera X uses more escaping of mathematical characters. 
Operators
and Cheat Sheet 
Formulas of dL, with typical names φ and ψ, are defined by the following syntax  
φ ::=  \forall x φ  Universal quantifier: for all real values of x, formula φ holds 
\exists x φ  Existential quantifier: for some real value of x, formula φ holds  
[α] φ  After all runs of hybrid program α, formula φ holds (safety)  
<α> φ  There is at least one run of hybrid program α, after which formula φ holds (liveness)  
!φ  Negation (not)  
φ & ψ  Conjunction (and)  
φ  ψ  Disjunction (or)  
φ > ψ  Implication (implication)  
φ <> ψ  Biimplication (equivalence)  
pred  Real arithmetic predicate expression 
The behavior of the hybrid system α is specified as a hybrid program, which is, essentially, a program notation for hybrid systems.
Hybrid programs, with typical names α and β, are defined by the following syntax  
α ::=  α; β  Sequential composition following β after α has finished 
α ++ β  Nondeterministic choice following either α or β  
α^{*}  Nondeterministic repetition, repeating α arbitrarily often including 0 times  
x:=t  Discrete assignment/jump assigning the value of t to x  
{x'=t,y'=s, H}  Continuous evolution along differential equation system with terms t,s, optionally with evolution domain H. Systems of differential equations, differentialalgebraic equations, and differential equations with disturbances are possible as well.  
?H  State assertion testing whether formula H is true in current state (otherwise abort)  
where H is a formula of (possibly nonlinear) real arithmetic. 
Verification
Verifying correct functioning of hybrid systems amounts to proving validity of corresponding formulas in differential dynamic logic dL [5,7]. These dL formulas state the desired correctness properties of the hybrid systems under consideration, including safety, liveness, reactivity, and controllability properties. For showing that these systems operate as expected, André Platzer has devised a logical verification calculus [5,7]. 
Operators
and Rules 
Case studies for using differential dynamic logic to verify complex physical systems include studies for the European Train Control System (ETCS) [16] and verification of collision avoidance in aircraft collision avoidance maneuvers [15] as well as the nextgeneration Airborne Collision Avoidance System ACAS X [45]. Also see further case studies..
Differential Invariants, Variants, and Cuts
Advanced verification technology for differential dynamic logics is further based on differential invariants [8,11] that define an induction principle for differential equations [25,44]. Differential variants are a dual proof principle that can be used to prove liveness and progress properties of differential equations without having to solve them. They have been implemented in KeYmaera and KeYmaera X as well.
Details and Extensions
This page only shows the simplest version of a simple differential dynamic logic. For more details see this overview of logics for dynamical systems. Full extended syntax of differential dynamic logic dL, including additionally definable operations [18]
 KeYmaera theorem prover for hybrid systems, which implements the dL calculus
 There is an extension called quantified differential dynamic logic (QdL) [19], with which distributed hybrid systems can be verified. This is the first formal verification approach for (dynamic/reconfigurable) distributed hybrid systems, in which participants may appear and disappear during the system evolution.
 There is an extension called stochastic differential dynamic logic (SdL) [22], with which stochastic hybrid systems can be verified.
 Publications related to dL
 There is an extension called differentialalgebraic dynamic logic (DAL) for more general differentialalgebraic programs [8]
 Advanced verification technology for differential dynamic logic is based on differential invariants [8,10,13], which are formulas that remain true along the dynamics of the hybrid system and its differential equations.
 There is a temporal extension called differential temporal dynamic logic (dTL) [4]. Also see further details and extensions in my book [18].
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 realvalued 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 wellsuited for verifying realistic hybrid systems with parametric system dynamics.
Keywords: dynamic logic, differential equations, sequent calculus, axiomatisation, automated theorem proving, verification of hybrid systems
[7]Selected Publications
The canonical references on this approach are [7,8,25,18,44]. Also see publications on hybrid systems logic and the publication reading guide.
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]

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  RV'14  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]

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

André Platzer.
Analog and hybrid computation: Dynamical systems and programming languages.
Bulletin of the EATCS, 114, 2014. © author
Invited paper in The Logic in Computer Science Column by Yuri Gurevich.
[bib  pdf  eprint  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]

Stefan Mitsch, JanDavid Quesel and André Platzer.
Refactoring, refinement, and reasoning: A logical characterization for hybrid systems.
In Cliff B. Jones, Pekka Pihlajasaari and Jun Sun, editors, 19th International Symposium on Formal Methods, FM, Singapore, Proceedings, volume 8442 of LNCS, pp. 481496. 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]

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

Sarah M. Loos, David Witmer, Peter Steenkiste and André Platzer.
Efficiency analysis of formally verified adaptive cruise controllers.
In Andreas Hegyi and Bart De Schutter, editors, 16th International IEEE Conference on Intelligent Transportation Systems, ITSC'13, The Hague, Netherlands, Proceedings, 2013. © IEEE
[bib  pdf  doi  slides  study  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]

André Platzer.
Dynamic logics of dynamical systems.
arXiv:1205.4788, May 2012.
[bib  pdf  arXiv  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.
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.
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 Complete Proof Theory of Hybrid Systems.
School of Computer Science, Carnegie Mellon University, CMUCS11144, November 2011.
[bib  pdf  LICS'12]

André Platzer.
The Structure of Differential Invariants and Differential Cut Elimination.
School of Computer Science, Carnegie Mellon University, CMUCS11112, April 2011.
[bib  pdf  arXiv  LMCS'12]

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]

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]

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.
Differential dynamic logic: Automated theorem proving for hybrid systems.
Künstliche Intelligenz, 24(1), pp. 7577, 2010. © SpringerVerlag
Invited paper.
[bib  doi  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, 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.
Verification of cyberphysical transportation systems.
IEEE Intelligent Systems, 24(4), pp. 1013, Jul/Aug, 2009. © IEEE.
Invited paper.
[bib  doi  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 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.
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 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 and Edmund M. Clarke.
Computing Differential Invariants of Hybrid Systems as Fixedpoints.
School of Computer Science, Carnegie Mellon University, CMUCS08103, Feb, 2008.
[bib  pdf  CAV'08]

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.
Combining deduction and algebraic constraints for hybrid system analysis.
In Bernhard Beckert, editor, 4th International Verification Workshop, VERIFY'07, Workshop at Conference on Automated Deduction (CADE), Bremen, Germany, CEUR Workshop Proceedings, 259:164178, 2007.
[bib  pdf  slides  eprint  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.
A temporal dynamic logic for verifying hybrid system invariants.
In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, USA, Proceedings, volume 4514 of LNCS, pp. 457471. Springer, 2007. © SpringerVerlag
[bib  pdf  doi  slides  study  TR  abstract]

André Platzer.
Differential logic for reasoning about hybrid systems.
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. 746749. Springer, 2007. © SpringerVerlag
[bib  pdf  doi  poster  abstract]

André Platzer.
Differential logic for reasoning about hybrid systems.
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. 746749. Springer, 2007. © SpringerVerlag
[bib  pdf  doi  poster  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]
For full details, please see my List of Publications.
There also is a verification tool implementation of dL in a theorem prover, which is called KeYmaera [12].