
DownloadKeYmaera
or KeYmaera X or Source 
Overview
Differential invariants [1,4,3,5,13,14,22] provide induction principles for differential equations. They can be understood as the differential analogue of induction techniques but for differential equations rather than for discrete systems [11]. Discrete induction is used to prove a property of a loop by proving that the invariant is true initially and then that it is preserved every time the loop body executes once. Similarly, a differential invariant to hold always after a differential equation by proving that it holds initially and by proving that it is preserved in the direction of the dynamics of the differential equation. Differential invariants can prove properties of differential equations without having to solve the equations, which makes them computationally attractive. They play an important role in verifying properties of advanced hybrid systems such as aircraft and robots.
Differential Invariants
Advanced verification technology for differential dynamic logics is further based on differential invariants [1,4] that have been subsequently refined to a procedure that computes differential invariants in a fixedpoint loop [3,5]. Differential invariants define an induction principle for differential equations [11,22]. They make it possible to prove properties of differential equations without having to solve the equations. Differential invariants are formulas that remain true along the dynamics of the hybrid system and its differential equations. The central property of differential invariants for verification purposes is that they replace infeasible or impossible reachability analysis with feasible symbolic computation. Differential invariants are computationally attractive concepts, because their inductive conditions are just polynomial constraints, which are formulas of firstorder real arithmetic, and are thus decidable by quantifier elimination in realclosed fields.
Several results about the theory of differential invariants can be found in the literature [1,13,14,11,19,21,7,22].
There also is an implementation of differential invariants in the KeYmaera theorem prover and its successor KeYmaera X.
Differential Variants
The dual verification technique of differential variants can be used to prove liveness and progress properties of differential equations without having to solve them. Differential variants [1] are implemented in KeYmaera as well.
Differential Radical Invariants
A generalization of differential invariants to higherorder derivatives, called differential radical invariants, gives a decision procedure for algebraic invariants of algebraic differential equations. Differential radical invariants decide equational invariants p=0 for polynomials p. Differential radical invariants have been introduced in 2014 [17] and are implemented in KeYmaera as well.
Differential Cuts
Differential cuts [1,4,13,22] allow the use of lemmas that have been proved for differential equations. Differential cuts work as follows. They first prove that a differential equation never leaves region C and then restricts the dynamics of the system to C. Restricting the dynamics of a system to a subregion C usually changes the behavior of the system around, except that the first prove showed a lemma that the system cannot leave region C anyhow, so that the restriction of the dynamics to C turns out to be a pseudorestriction.
It has been shown that there is no differential cut elimination theorem [13].
Differential Ghosts
Auxiliary variables or ghost variables are extra variables that remember intermediate states, which can be useful for proving properties of conventional discrete programs. Differential ghosts [13,22] are the differential counterpart. What differential ghosts do is they introduce extra variables into extra dimensions of the system, which can further evolve according to extra differential equations that are made up for the purposes of the proof.
Abstract
The biggest challenge in hybrid systems verification is the handling of differential equations. Because computable closedform solutions only exist for very simple differential equations, proof certificates have been proposed for more scalable verification. Search procedures for these proof certificates are still rather adhoc, though, because the problem structure is only understood poorly. We investigate differential invariants, which define an induction principle for differential equations and which can be checked for invariance along a differential equation just by using their differential structure, without having to solve them. We study the structural properties of differential invariants. To analyze tradeoffs for proof search complexity, we identify more than a dozen relations between several classes of differential invariants and compare their deductive power. As our main results, we analyze the deductive power of differential cuts and the deductive power of differential invariants with auxiliary differential variables. We refute the differential cut elimination hypothesis and show that, unlike standard cuts, differential cuts are fundamental proof principles that strictly increase the deductive power. We also prove that the deductive power increases further when adding auxiliary differential variables to the dynamics.
Keywords: proof theory, differential equations, differential invariants, differential cut elimination, differential dynamic logic, hybrid systems, logics of programs, real differential semialgebraic geometry
[13]Selected Publications
The canonical reference on differential invariants is the article in the Journal of Logic and Computation [1] that appeared in 2008. Differential invariants were later used for a fixpoint procedure that computes differential invariants and verifies some interesting hybrid systems automatically , which appeared at CAV'08 [3] and in a special issue of FMSD for selected CAV papers [5]. An elegant axiomatic formulation of differential invariants, differential cuts, and differential ghosts has been reported at CADE'15 [20] and JAR [22]. Also see publications on differential invariants and the publication reading guide.
André Platzer.
A complete uniform substitution calculus for differential dynamic logic.
Journal of Automated Reasoning, 2016. © The author
[bib  pdf  doi  arXiv  abstract]

Andrew Sogokon, Khalil Ghorbal, Paul B. Jackson and André Platzer.
A method for invariant generation for polynomial continuous systems.
In Barbara Jobstmann and K. Rustan M. Leino, editors, Verification, Model Checking, and Abstract Interpretation  17th International Conference, VMCAI 2016, St. Petersburg, Florida, USA, January 1719, 2016, Proceedings, volume 9583 of LNCS, pp. 268288. Springer, 2016. © SpringerVerlag
[bib  pdf  doi  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]

Khalil Ghorbal, Andrew Sogokon, and André Platzer.
A hierarchy of proof rules for checking differential invariance of algebraic sets.
In Deepak D'Souza, Akash Lal, and Kim Guldstrand Larsen, editors, Verification, Model Checking, and Abstract Interpretation  16th International Conference, VMCAI 2015, Mumbai, India, January 1214, 2015, Proceedings, volume 8931 of LNCS, pp. 431448. Springer, 2015. © SpringerVerlag
[bib  pdf  doi  slides  study  ComLan'16  abstract]

Khalil Ghorbal, Andrew Sogokon, and André Platzer.
Invariance of conjunctions of polynomial equalities for algebraic differential equations.
In Markus MüllerOlm and Helmut Seidl, editors, 21st International Static Analysis Symposium, volume 8723 of LNCS, pp. 151167. Springer, 2014. © SpringerVerlag
[bib  pdf  doi  study  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]

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.
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.
Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics.
Springer, 2010. 426 p. ISBN 9783642145087.
[bib  book  eBook  doi  web]

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 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]
For full details, please see my List of Publications.