KeYmaera: A Hybrid Theorem Prover for Hybrid Systems

  1. Home
    2. >>
  2. Tools
    3. >>
  3. KeYmaera
Table of Contents
  1. Outdated: Use Successor KeYmaera X Instead
  2. Overview
  3. Case Studies
  4. KeYmaera Tool Architecture
  5. Sphinx: Verification-Driven Engineering Toolkit
  6. Verification
  7. Documentation & Tutorials
  8. KeYmaera Usage
  9. Old KeYmaera vs. New KeYmaera X
  10. News
  11. Etymology: The Name KeYmaera
  12. Abstract
  13. Selected Publications
KeYmaera or
Source
Book: Logical Analysis of Hybrid Systems

Outdated: Use Successor KeYmaera X Instead

The successor, KeYmaera X, is an entirely new and overall better theorem prover for hybrid systems building on the experience with the successes of KeYmaera. The older KeYmaera prover is, of course, also still available, but we generally recommend KeYmaera X for most purposes. [comparison]

 

See Successor: KeYmaera X

 

Overview
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 (dL) [4,6,27], which is a first-order dynamic logic for hybrid programs [4,6,27], a program notation for hybrid systems. KeYmaera also supports hybrid systems with nonlinear discrete jumps, nonlinear differential equations, differential-algebraic equations, differential inequalities, and systems with nondeterministic discrete or continuous input. For automation, KeYmaera implements a free-variable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically. This compositional verification principle helps scaling up verification, because KeYmaera verifies a big system by verifying properties of subsystems. To overcome the complexity of real arithmetic, we integrate real quantifier elimination following an iterative background closure strategy [5,14]. The KeYmaera verification tool is particularly suitable for verifying parametric hybrid systems and has been used successfully for verifying case studies from train control [17,19], car control [22,24], and air traffic control [16,19,48]. .

The KeYmaera verification tool provides significant automation (up to 100% depending on the problem). It handles differential equations and integrates full first-order real arithmetic. KeYmaera also implements differential invariants [7]. KeYmaera implements procedures for automatically generating invariants and differential invariants [10,13,33], but allows you to specify invariants interactively or by @invariant annotations whenever your case study is too complex for KeYmaera's current automation. The graphical user interface of KeYmaera can be used to navigate and manipulate the proofs discovered by KeYmaera or find more efficient proofs.

Details about the KeYmaera verification approach can be found in the corresponding book [19] and several other publications. The tutorial on How to Model and Prove Hybrid Systems with KeYmaera [47] can be a helpful starting point on how to use KeYmaera.

Case Studies

The KeYmaera verification tool has been used successfully for verification in railway [17], automotive [22,24,29], and aviation transportation systems [16,36,48], as well as autonomous robotics [38,34], surgical robotics [37], and electric circuits [19].

KeYmaera has been used for automatic verification of collision freedom for the cooperation layer of the European Train Control System (ETCS) [17]. It has been used systematically to synthesize the required safety constraints on the design parameters of fully parametric ETCS [17]. KeYmaera has been used to verify collision freedom in roundabout aircraft collision avoidance maneuvers [7], including the flyable roundabout collision avoidance maneuver [16]. These verification results show that the controllers of the aircraft models successfully prevent collisions. Extensions for provable collision freedom in flyable disc maneuvers for an arbitrary number of aircraft have been verified in KeYmaeraD [36]. A whole range of automotive systems have been verified with KeYmaera, including collision freedom in adaptive cruise control for highway systems [22], safety of a CICAS-inspired intersection control system for cars [24], safe interactions of cars with traffic centers via variable speed limits, including moving incidents [29], and a model for CICAS-SLTA Signalized Left Turn Assist [32]. The dynamic window approach for autonomous robotic ground vehicles has been verified in KeYmaera [38]. A few academic standard examples from the hybrid systems world have been verified with KeYmaera as well, including a fully parametric version of the bouncing ball [12] and the standard, non-parametric water tank. KeYmaera has been used to verify the RLC electric circuit [19], a model of a distributed elevator controller, medical surgical robotics applications for skull base surgery [37], and a robotic factory automation case study [34]. KeYmaera has also been used for verification efforts of the Next-Generation Airborne Collision Avoidance System ACAS X [48].

 
 
 
 
 
 
 
 
 
 

For more details on case studies, also see the subpages on this web page and the projects listed in KeYmaera's project wizard (the menu item File->Load Project in KeYmaera).

A number of other case studies have been verified, for example in the CPS V&V Grand Prix 2014 and 2013. Tell us if you want to advertise your case study or KeYmaera verification example on this web page and in the KeYmaera project wizard.

KeYmaera Tool Architecture

The architecture of the KeYmaera verification tool has a plug-in system for solvers and proof rules [12] and allows to adjust the automatic proof strategies by several options.

Sphinx: Verification-Driven Engineering Toolkit

Sphinx is a modeling tool that works with KeYmaera and provides textual and graphical modeling capabilities as well as model transformation and collaborative verification tools for KeYmaera. Sphinx is an extensible verification-driven engineering toolkit based on the Eclipse platform. It provides textual and graphical modeling editors to describe the structure, the discrete dynamics, and the continuous dynamics of cyber-physical systems. Sphinx uses KeYmaera as hybrid verification tool.

Verification

In KeYmaera, verifying correct functioning of hybrid systems amounts to proving corresponding formulas in, what is called, differential dynamic logic dL [4,6]. These 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 [4,6].

Advanced verification technology for differential dynamic logics is further based on differential invariants [7,10,13], which are formulas that remain true along the dynamics of the hybrid system and its differential equations. Differential invariants and differential induction are essentially a generalization of discrete induction to differential equations. This verification technology for differential dynamic logic and differential-algebraic dynamic logic has been implemented in the KeYmaera theorem prover for hybrid systems.

KeYmaera implements the verification calculi for the logics described in [4,6,3,7,34] and also part of [20,31]. The verification algorithms implemented in KeYmaera are described in the papers [5,14,13,33] and, a little bit also in the KeYmaera tool paper [12].

Documentation & Tutorials

FMCAD tutorial or
LICS tutorial or
LICS slides or
Cheat Sheet or
User Guide or
YouTube or
Howto Guide or
Book or
Lecture Notes

KeYmaera Usage

KeYmaera on YouTube Channel by Sarah Loos

Old KeYmaera vs. New KeYmaera X

We strongly recommend the successor KeYmaera X, which is a complete clean-slate implementation of a theorem prover for hybrid systems, featuring a minimal core of just 1700 lines of code that isolates all soundness-critical reasoning.

In addition to providing numerous improvements like an easier user interface, tactical proof programming, more sophisticated continuous invariant generation, and significantly more advanced automation that many users have always dreamed of, the new KeYmaera X provides almost all functionality that its predecessor KeYmaera provides. What you will not yet find in KeYmaera X is:

Except possibly when you are relying on any of these particular aspects of KeYmaera, you will really enjoy the novel programming features of KeYmaera X. While the old KeYmaera provides a small number of built-in automatic proof strategies to choose from, the new KeYmaera X provides a way of easily defining custom proof automation tactics, lemmas, it visually retains the sequent proofs, and provides a web-based user interface that even records tactics for you. KeYmaera X can also run out of the box without the need to install additional tools.

Correctness arguments also benefit from the gigantic reduction in the soundness-critical core from the 65,989 lines of KeYmaera to the 1,700 lines of KeYmaera X, which is a significant reduction down to 2.5%.

News

While KeYmaera 3 still provides a few features that are unique to KeYmaera 3, its successor KeYmaera X has matured to a significantly more solid tool and is actively developed and maintained [comparison].

Etymology: The Name KeYmaera

The name KeYmaera is a homophone to Chimaera (Χíμαιρα), the hybrid animal from ancient Greek mythology, which is a hybrid mixture of multiple animals [Homer, Iliad 6. 179-182]. KeYmaera is a hybrid version of the KeY tool. KeYmaera also is a hybrid mixture of multiple proving technologies from logic or discrete and continuous mathematics and KeYmaera is intended for hybrid systems verification, which are systems evolving along mixed discrete and continuous transitions.

The development code name for KeYmaera was HyKeY, because HyKeY stands to reason as a canonical name in line with hybrid systems model checkers like HyTech or HySAT. We decided to go for a fancy name instead, paying homage to KeYmaera's roots in a hybrid extension of KeY, to its purpose for hybrid systems verification, and to the hybrid nature of its algorithmic design combining aspects of theorem proving, computer algebra, decision procedures, and model checking.

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 [4,6], 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.

Keywords: dynamic logic, sequent calculus, automated theorem proving, decision procedures, computer algebra, verification of parametric hybrid systems, quantifier elimination

Selected Publications

The canonical references on the KeYmaera approach are [6,7,27]. The proof theory is studied in detail in [27]. The most comprehensive description of the KeYmaera appraoch can be found in the book [19], with further details also in subsequent papers. Also see publications on hybrid systems logic and the publication reading guide.
  1. Stefan Mitsch and André Platzer.
    A retrospective on developing hybrid system provers in the KeYmaera family:
       A tale of three provers.
    In Wolfgang Ahrendt et al., editors, Deductive Software Verification: Future Perspectives, volume 12345 of LNCS, pp. 21-64. Springer, 2020. © Springer
    [bib | ✂ | pdf | doi | abstract]

  2. André Platzer.
    Logical Foundations of Cyber-Physical Systems.
    Springer, Cham, 2018. 659 pages. ISBN 978-3-319-63587-3.
    [bib | ✂ | doi | slides | video | book | web | errata | abstract]

  3. Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki, and André Platzer.
    A formally verified hybrid system for the next-generation 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 11-18, 2015, Proceedings, volume 9035 of LNCS, pp. 21-36. Springer, 2015. © Springer
    [bib | ✂ | pdf | doi | study | TR | STTT'17 | abstract]

  4. Jan-David 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. 67-91, 2016. © The authors
    [bib | ✂ | pdf | doi | mypdf | abstract]

  5. 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 12-14, 2015, Proceedings, volume 8931 of LNCS, pp. 431-448. Springer, 2015. © Springer
    [bib | ✂ | pdf | doi | slides | study | ComLan'17 | abstract]

  6. André Platzer.
    Analog and hybrid computation: Dynamical systems and programming languages.
    Bulletin of the EATCS 114, 2014. © The author
    Invited paper in The Logic in Computer Science Column by Yuri Gurevich.
    [bib | ✂ | pdf | eprint | abstract]

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

  8. Khalil Ghorbal, Andrew Sogokon, and André Platzer.
    Invariance of conjunctions of polynomial equalities for algebraic differential equations.
    In Markus Müller-Olm and Helmut Seidl, editors, 21st International Static Analysis Symposium, SAS 2014, volume 8723 of LNCS, pp. 151-167. Springer, 2014. © Springer
    [bib | ✂ | pdf | doi | slides | study | abstract]

  9. Stefan Mitsch, Jan-David 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'14, Singapore, Proceedings, volume 8442 of LNCS, pp. 481-496. Springer, 2014. © Springer
    [bib | ✂ | pdf | doi | slides | abstract]

  10. 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. 279-294. Springer, 2014. © Springer
    [bib | ✂ | pdf | doi | slides | study | TR | abstract]

  11. André Platzer.
    Foundations of Cyber-Physical Systems.
    Lecture Notes, Computer Science Department, Carnegie Mellon University. 2014.
    [bib | ✂ | pdf | textbook | course]

  12. 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]

  13. 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]

  14. 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 8-13, 2013, pp. 263-272. ACM, 2013. © ACM
    [bib | ✂ | pdf | doi | slides | study | abstract]

  15. Sarah M. Loos, David W. Renshaw and André Platzer.
    Formal verification of distributed aircraft controllers.
    In Calin Belta and Franjo Ivancic, editors, Hybrid Systems: Computation and Control (part of CPS Week 2013), HSCC'13, Philadelphia, PA, USA, April 8-13, 2013, pp. 125-130. ACM, 2013. © ACM
    [bib | ✂ | pdf | doi | slides | poster | study | TR | abstract]

  16. 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]

  17. Jan-David Quesel and André Platzer.
    Playing hybrid games with KeYmaera.
    In Bernhard Gramlich, Dale Miller and Ulrike Sattler, editors, Automated Reasoning, 6th International Joint Conference, IJCAR'12, Manchester, UK, Proceedings, volume 7364 of LNCS, pp. 439-453. Springer, 2012. © Springer
    [bib | ✂ | pdf | doi | slides | study | abstract]

  18. 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 13-15, Princeton, USA, Proceedings, volume 7406 of LNCS, pp. 28-48. Springer, 2012. © Springer
    Invited paper.
    [bib | ✂ | pdf | doi | slides | abstract]

  19. Nikos Aréchiga, Sarah M. Loos, André Platzer and Bruce H. Krogh.
    Using theorem provers to guarantee closed-loop system properties.
    In Dawn Tilbury, editor, American Control Conference, ACC'12, Montréal, Canada, June 27-29. pp. 3573-3580. 2012. © IEEE
    [bib | ✂ | pdf | doi | abstract]

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

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

  22. Stefan Mitsch, Sarah M. Loos and André Platzer.
    Towards formal verification of freeway traffic control.
    In Chenyang Lu, editor, ACM/IEEE Third International Conference on Cyber-Physical Systems ICCPS'12, Beijing, China, April 17-19. pp. 171-180, IEEE. 2012. © IEEE
    [bib | ✂ | pdf | doi | slides | study | abstract]

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

  24. 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. 541-550. IEEE 2012. © IEEE
    [bib | ✂ | pdf | doi | slides | TR | abstract]

  25. André Platzer.
    Differential Game Logic for Hybrid Games.
    School of Computer Science, Carnegie Mellon University, CMU-CS-12-105, March 2012.
    Also see new results.
    [bib | ✂ | pdf | TOCL'15 | abstract]

  26. André Platzer.
    The Complete Proof Theory of Hybrid Systems.
    School of Computer Science, Carnegie Mellon University, CMU-CS-11-144, November 2011.
    [bib | ✂ | pdf | LICS'12]

  27. Sarah M. Loos and André Platzer.
    Safe intersections: At the crossing of hybrid systems and verification.
    In Kyongsu Yi, editor, 14th International IEEE Conference on Intelligent Transportation Systems, ITSC'11, Washington, DC, USA, Proceedings, pp. 1181-1186. 2011. © IEEE
    [bib | ✂ | pdf | doi | slides | study | abstract]

  28. 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. 28-43. Springer, 2011. © Springer
    Invited tutorial.
    [bib | ✂ | pdf | doi | slides | abstract]

  29. 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. 42-56. Springer, 2011. © Springer
    [bib | ✂ | pdf | doi | slides | study | TR | abstract]

  30. 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 12-14, pp. 63-72. ACM, 2011. © ACM
    [bib | ✂ | pdf | doi | slides | abstract]

  31. 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 23-27, 2010. Proceedings, volume 6247 of LNCS, pp. 469-483. Springer, 2010. © Springer
    [bib | ✂ | pdf | doi | slides | TR | LMCS'12 | abstract]

  32. André Platzer.
    Logical Analysis of Hybrid Systems:
       Proving Theorems for Complex Dynamics.
    Springer, Heidelberg, 2010. 426 pages. ISBN 978-3-642-14508-7.
    [bib | ✂ | doi | book | web | errata | abstract]

  33. André Platzer.
    Differential dynamic logic:
       Automated theorem proving for hybrid systems.
    Künstliche Intelligenz 24(1), pp. 75-77, 2010. © Springer
    Invited paper.
    [bib | ✂ | doi | abstract]

  34. André Platzer and Jan-David 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. 246-265. Springer, 2009. © Springer
    [bib | ✂ | pdf | doi | slides | kyx | TR | old | abstract]

  35. 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. 547-562. Springer, 2009. © Springer
    FM Best Paper Award.
    [bib | ✂ | pdf | doi | slides | study | TR | abstract]

  36. André Platzer.
    Verification of cyberphysical transportation systems.
    IEEE Intelligent Systems 24(4), pp. 10-13, Jul/Aug, 2009. © IEEE
    Invited paper.
    [bib | ✂ | doi | abstract]

  37. André Platzer, Jan-David Quesel and Philipp Rümmer.
    Real world verification.
    In Renate A. Schmidt, editor, International Conference on Automated Deduction, CADE-22, Montreal, Canada, Proceedings, volume 5663 of LNCS, pp. 485-501. Springer, 2009. © Springer
    [bib | ✂ | pdf | doi | slides | study | TR | smtlib | abstract]
    Introduces a decision procedure for universal nonlinear real arithmetic combining Gröbner bases and semidefinite programming for the Real Nullstellensatz.

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

  39. André Platzer and Jan-David 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. 171-178. Springer, 2008. © Springer
    [bib | ✂ | pdf | doi | slides | tool | abstract]

  40. 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]

  41. 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. 176-189, Springer, 2008. © Springer
    [bib | ✂ | pdf | doi | slides | study | TR | FMSD'09 | abstract]

  42. André Platzer and Edmund M. Clarke.
    Computing Differential Invariants of Hybrid Systems as Fixedpoints.
    School of Computer Science, Carnegie Mellon University, CMU-CS-08-103, Feb, 2008.
    [bib | ✂ | pdf | CAV'08]

  43. André Platzer and Jan-David Quesel.
    Logical verification and systematic parametric analysis in train control.
    In Magnus Egerstedt and Bud Mishra, editors, Hybrid Systems: Computation and Control, 11th International Conference, HSCC 2008, St. Louis, USA, Proceedings, volume 4981 of LNCS, pp. 646-649. Springer, 2008. © Springer
    [bib | ✂ | pdf | doi | poster | abstract]

  44. André Platzer.
    Differential-algebraic dynamic logic for differential-algebraic programs.
    Journal of Logic and Computation 20(1), pp. 309-352, 2010.
    Special issue for selected papers from TABLEAUX'07. © The author
    [bib | ✂ | pdf | doi | eprint | study | errata | TABLEAUX'07 | abstract]

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

  46. André Platzer.
    Combining deduction and algebraic constraints for hybrid system analysis.
    In Bernhard Beckert, editor, 4th International Verification Workshop, VERIFY'07, Bremen, Germany, CEUR Workshop Proceedings, 259:164-178, 2007.
    [bib | ✂ | pdf | eprint | slides | abstract]

  47. 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 3-6, 2007, Proceedings, volume 4548 of LNCS, pp. 216-232. Springer, 2007. © Springer
    TABLEAUX Best Paper Award.
    [bib | ✂ | pdf | doi | slides | study | TR | abstract]

  48. 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. 457-471. Springer, 2007. © Springer
    [bib | ✂ | pdf | doi | slides | study | TR | abstract]

  49. 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. 746-749. Springer, 2007. © Springer
    [bib | ✂ | pdf | doi | poster | abstract]

  50. 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):63-77, 2007.
    [bib | ✂ | pdf | doi | slides | abstract]

Copyright of publications is with the publisher 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. All information and materials on this site are provided solely for informational purposes on an AS-IS basis, and any and all implied warranties are expressly disclaimed. More details on the differential dynamic logic (dL), on the hybrid program model for hybrid systems, and on the principles of logic for hybrid systems. For full details, please see more publications.

Any opinions, findings, and conclusions or recommendations expressed are those of the author(s) and do not necessarily reflect the views of any sponsoring institution.

Copyright © by André Platzer        Last modified: 2024-01-09

Publications | Research | Tools | Courses | A. Platzer