Reading Guide for Publications by André Platzer

Landmark Papers

Most important foundational landmark papers include the following:

More information on the hybrid systems aspects can be found in the book on logic and hybrid systems verification [17] and in the lecture notes Foundations of Cyber-Physical Systems [3]. A very readable survey can also be found in the invited LICS tutorial [9] and an extended version with more detail and examples that also covers distributed hybrid systems and stochastic hybrid systems [6]. There is also an earlier verification overview in the invited CAV tutorial [13].

Also see publications by area.

Important Applications

The most important applications and case studies that we have verified are

Differential Dynamic Logics

There are many logics in the family of differential dynamic logics.
Logic Logic for Dynamical System References
dL Differential dynamic logic
for hybrid systems
[38,10,17]
DAL Differential-algebraic dynamic logic
for hybrid systems with differential-algebraic programs, differential-algebraic constraints, differential inequalities, disturbances etc.
[37,17]
dTL Differential temporal dynamic logic
for hybrid systems with temporal and throughout modalities
[17,43]
QdL Quantified differential dynamic logic
for distributed hybrid systems
[16,8]
SdL Stochastic differential dynamic logic
for stochastic hybrid systems
[12]
dLh Hybrid-nominal differential dynamic logic
for hybrid systems
[48]
Surveys of differential dynamic logics can be found in [9,6].

Publication Reading Guide

The primary paper for logic for hybrid systems verification appeared in the Journal of Automated Reasoning [38]. For a first understanding the logical approach to hybrid systems verification, I also recommend an earlier conference paper [41], 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 [38]. 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. Yet another breakthrough shows a sound and complete axiomatization of hybrid systems relative to discrete dynamics [10], thereby equating hybrid dynamics, continuous dynamics, and discrete dynamics, proof-theoretically. A corollary proves that numerical discretization and numerical differential equation solving can be used for hybrid systems verification without losing soundness.

A brief overview about the tool KeYmaera itself was reported later in a tool paper [33]. 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 [38,37,17]. A more comprehensive survey on using logic for hybrid systems and the KeYmaera tool can be found in the CAV tutorial [13]. A more comprehensive survey on differential dynamic logic can be found in the LICS tutorial [9].

Another major step is the handling of more complex differential equations by an approach called differential invariants, which were first introduced in 2008 [37] and studied further in [34,11,7]. This article also presents an advanced verification logic for hybrid systems that can even have disturbances and differential inequalities in the dynamics [37]. It has been the basis for subsequent automatic verification techniques to compute differential invariants [34,30]. Applications of these verification techniques have been described for air traffic control [22] and train control [21]. A comprehensive treatment of logic for hybrid systems, its theory, practice, and applications, can be found in a book [17].

Another interesting breakthrough [16] 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 [15]

Numerical techniques and the image computation problem for hybrid systems are discussed in a paper at HSCC'07 [46]. This paper discusses the numerical decidability frontier for hybrid systems image computation. This paper 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 [19], is possible at all. A more comprehensive verification approach and logic for stochastic hybrid systems can be found in [12].

Publications (incomplete list)

  1. 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, pages 199-214. Springer, 2014. © Springer-Verlag
    [bib | pdf | doi | slides | study | TR | abstract]

  2. 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, pages 279-294. Springer, 2014. © Springer-Verlag
    [bib | pdf | doi | slides | TR | abstract]

  3. André Platzer.
    Foundations of Cyber-Physical Systems.
    Lecture Notes, Computer Science Department, Carnegie Mellon University. 2013.
    [bib | pdf | course | abstract]

  4. 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.
    [bib | pdf | slides | study | eprint | talk | abstract]

  5. 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, pages 263-272. ACM, 2013. © ACM
    [bib | pdf | doi | study | abstract]

  6. André Platzer.
    Dynamic logics of dynamical systems.
    arXiv 1205.4788, May 2012.
    [bib | pdf | arXiv | abstract]

  7. 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, pages 28-48. Springer, 2012. © Springer-Verlag
    Invited paper.
    [bib | pdf | doi | slides | abstract]

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

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

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

  11. André Platzer.
    The structure of differential invariants and differential cut elimination.
    Logical Methods in Computer Science, 8(4), pages 1-38, 2012.
    [bib | pdf | doi | eprint | arXiv | abstract]

  12. André Platzer.
    Stochastic differential dynamic logic for stochastic hybrid programs.
    In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, International Conference on Automated Deduction, CADE'11, Wroclaw, Poland, Proceedings, volume 6803 of LNCS, pages 431-445. Springer, 2011. © Springer-Verlag
    [bib | pdf | doi | slides | TR | abstract]

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

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

  15. 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, Pages 63-72. ACM, 2011. © ACM
    [bib | pdf | doi | slides | abstract]

  16. 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, pages 469-483. Springer, 2010. © Springer-Verlag
    [bib | pdf | doi | slides | TR | LMCS'12 | abstract]

  17. André Platzer.
    Logical Analysis of Hybrid Systems: Proving Theorems for Complex Dynamics.
    Springer, 2010. 426 p. ISBN 978-3-642-14508-7.
    [bib | book | eBook | doi | web]

  18. Paolo Zuliani, André Platzer and Edmund M. Clarke.
    Bayesian Statistical Model Checking with Application to Simulink/Stateflow Verification.
    School of Computer Science, Carnegie Mellon University, CMU-CS-10-100, 2010.
    [bib | pdf | HSCC'10]

  19. 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 12-15, pages 243-252. ACM, 2010. © ACM
    [bib | pdf | doi | TR | abstract]

  20. André Platzer and Jan-David Quesel.
    European Train Control System: A Case Study in Formal Verification.
    Reports of SFB/TR 14 AVACS 54, 2009. ISSN: 1860-9821, www.avacs.org.
    [bib | pdf | ICFEM'09]

  21. 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, Rio de Janeiro, Brasil, Proceedings, volume 5885 of LNCS, pages 246-265. Springer, 2009. © Springer-Verlag
    [bib | pdf | doi | slides | study | TR | abstract]

  22. 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, pages 547-562. Springer, 2009. © Springer-Verlag
    This paper was awarded the FM Best Paper Award.
    [bib | pdf | doi | slides | study | TR | abstract]

  23. André Platzer and Edmund M. Clarke.
    Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study.
    School of Computer Science, Carnegie Mellon University, CMU-CS-09-147, 2009.
    [bib | pdf | FM'09]

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

  25. Sumit Kumar Jha, Edmund Clarke, Christopher Langmead, Axel Legay, André Platzer and Paolo Zuliani.
    A Bayesian approach to model checking biological systems.
    In Pierpaolo Degano and Roberto Gorrieri, editors, Computational Methods in Systems Biology, 7th International Conference, CMSB 2009, Bologna, Italy, Proceedings, volume 5688 of LNCS, pages 218-234. Springer, 2009. © Springer-Verlag
    [bib | pdf | doi | TR | abstract]

  26. Sumit Kumar Jha, Edmund Clarke, Christopher Langmead, Axel Legay, André Platzer and Paolo Zuliani.
    A Bayesian Approach to Model Checking Biological Systems.
    School of Computer Science, Carnegie Mellon University, CMU-CS-09-110, 2009.
    [bib | pdf | CMSB'09]

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

  28. André Platzer, Jan-David Quesel and Philipp Rümmer.
    Real World Verification.
    Reports of SFB/TR 14 AVACS 52, 2009. ISSN: 1860-9821, www.avacs.org.
    [bib | pdf | CADE'09]

  29. André Platzer, Jan-David Quesel and Philipp Rümmer.
    Real world verification.
    In Renate A. Schmidt, editor, International Conference on Automated Deduction, CADE'09, Montreal, Canada, Proceedings, volume 5663 of LNCS, pages 485-501. Springer, 2009. © Springer-Verlag
    [bib | pdf | doi | slides | TR | smtlib | abstract]
    Introduces a decision procedure for universal nonlinear real arithmetic combining Gröbner bases and semidefinite programming for the Real Nullstellensatz. An extended set of real arithmetic benchmarks from KeYmaera is available in smtlib, including the examples from CADE'09 paper and from some other KeYmaera-related papers.

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

  31. Edmund M. Clarke, Bruce Krogh, André Platzer and Raj Rajkumar.
    Analysis and verification challenges for cyber-physical transportation systems.
    In NITRD National Workshop for Research on Transportation Cyber-Physical Systems: Automotive, Aviation, and Rail, 2008.
    Position paper.
    [bib | pdf | abstract]

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

  33. 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, pages 171-178. Springer, 2008. © Springer-Verlag
    [bib | pdf | doi | slides | tool | abstract]

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

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

  36. 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, pages 646-649. Springer, 2008. © Springer-Verlag
    [bib | pdf | doi | poster | abstract]

  37. André Platzer.
    Differential-algebraic dynamic logic for differential-algebraic programs.
    Journal of Logic and Computation, 20(1), pages 309-352, 2010. © The author Advance Access published on November 18, 2008 by Oxford University Press.
    [bib | pdf | doi | study | abstract]

  38. André Platzer.
    Differential dynamic logic for hybrid systems.
    Journal of Automated Reasoning, 41(2), pages 143-189, 2008. © Springer-Verlag
    [bib | pdf | doi | study | abstract]

  39. 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:164-178, 2007.
    [bib | pdf | slides | eprint | abstract]

  40. Werner Damm, Alfred Mikschl, Jens Oehlerking, Ernst-Rüdiger Olderog, Jun Pang, André Platzer, Marc Segelken and Boris Wirtz.
    Automating verification of cooperation, control, and design in traffic applications.
    In Cliff Jones, Zhiming Liu and Jim Woodcock, editors, Formal Methods and Hybrid Real-Time Systems, volume 4700 of LNCS, pages 115-169. Springer, 2007. © Springer-Verlag
    Invited paper.
    [bib | pdf | doi | abstract]

  41. 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, pages 216-232. Springer, 2007. © Springer-Verlag
    This paper was awarded the TABLEAUX Best Paper Award.
    [bib | pdf | doi | slides | study | TR | abstract]

  42. André Platzer.
    Differential Dynamic Logic for Verifying Parametric Hybrid Systems.
    Reports of SFB/TR 14 AVACS 15, May 2007. ISSN: 1860-9821, www.avacs.org.
    [bib | pdf | TABLEAUX'07]

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

  44. André Platzer.
    A Temporal Dynamic Logic for Verifying Hybrid System Invariants.
    Reports of SFB/TR 14 AVACS 12, February 2007. ISSN: 1860-9821, www.avacs.org.
    [bib | pdf | LFCS'07]

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

  46. 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, pages 473-486. Springer, 2007, © Springer-Verlag
    [bib | pdf | doi | slides | tool | abstract]

  47. Stephanie Kemper and André Platzer.
    SAT-based abstraction refinement for real-time systems.
    In Frank S. de Boer and Vladimir Mencl, editors, Formal Aspects of Component Software, Third International Workshop, FACS 2006, Prague, Czech Republic, Proceedings, Electr. Notes Theor. Comput. Sci., 182:107-122, 2007
    [bib | pdf | doi | slides | tool | abstract]

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

  49. Bernhard Beckert and André Platzer.
    Dynamic logic with non-rigid functions: A basis for object-oriented program verification.
    In Uli Furbach and Natarajan Shankar, editors, Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4130 of LNCS, pages 266-280. Springer, 2006. © Springer-Verlag
    [bib | doi | slides | abstract]

  50. André Platzer.
    An Object-oriented Dynamic Logic with Updates.
    Master's Thesis, University of Karlsruhe, Department of Computer Science. Institute for Logic, Complexity and Deduction Systems, September 2004.
    Short version appeared as Dynamic logic with non-rigid functions: A basis for object-oriented program verification at IJCAR 2006.
    [bib | pdf | slides | abstract]

  51. André Platzer.
    Using a Program Verification Calculus for Constructing Specifications from Implementations.
    Minor Thesis (Studienarbeit), University of Karlsruhe, Department of Computer Science. Institute for Logic, Complexity and Deduction Systems, February 2004.
    [bib | pdf | slides | abstract]