Reading Guide for Publications by André Platzer

Table of Contents Key Publications Quickly: What to Read When Important Foundations Important Applications Differential Dynamic Logics Publication Reading Guide Select Publications

Publications By Type or By Year or By Area or Guide

Key Publications

Reading guide for select publications by André Platzer. This page provides pointers to the most important publications, as well as a short description of what to read when.

1. 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]
   
   
This textbook is breaking with the myth that cyber-physical systems are too challenging to be taught at the undergraduate level. Teaching CPS-related topics is notoriously challenging, but also creates an opportunity to discover and explore other areas of science with the intrinsic motivation it takes to succeed. This is the only textbook teaching undergraduate students the core principles behind CPS analysis. It shows them how to develop models and controls; identify safety specifications and critical properties; reason rigorously about CPS models; leverage multi-dynamical systems compositionality to tame CPS complexity; verify CPS models of appropriate scale in logic; and develop an intuition for operational effects. The textbook covers logic for hybrid systems, for differential equations, and for hybrid games, as well as comprehensive CPS correctness arguments. It is supported with homework exercises, YouTube lecture videos, and slides.


2. 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]
   
   
Identifies a fundamental constructive proof-theoretical relationship equating discrete, continuous, and hybrid dynamical systems by provably equivalently reducing properties of hybrid systems in Differential Dynamic Logic to both continuous systems and also reducing them to discrete systems. This proves that Differential Dynamic Logic has a sound and complete axiomatization of hybrid systems relative to continuous systems as well as a sound and complete axiomatization of hybrid systems relative to discrete systems. This fundamental cornerstone sheds light on the nature of hybridness and enables flexible and provably perfect combinations of discrete reasoning with continuous reasoning that lift to all aspects of hybrid systems and their fragments. The result forms the underlying foundation for subsequent insights at JACM'20 exploiting completeness characterizations.


3. André Platzer.
   A complete uniform substitution calculus for differential dynamic logic.
   Journal of Automated Reasoning 59(2), pp. 219-265, 2017. © The author
   [bib | ⧉ | pdf | doi | mypdf | arXiv | abstract]
   
   
Introduces a relatively complete proof calculus for Differential Dynamic Logic (dL) based entirely on uniform substitution. Uniform substitutions instantiate predicate symbols by formulas (due to Church for first-order logic) and continue to shine for dL. They enable substantially simpler theorem provers (KeYmaera X) by reducing axiom/rule schemata to axioms. Introduces differentials, which are inspired by Élie Cartan's seminal differential forms, but depart in crucial ways to draw sound conclusions from syntactic manipulations mixing dynamic statements about differential equations and static statements about differentials. They enable axiomatic proofs for differential equations with modular reasoning about i) the effect of differential equations on the derivatives of state variables, ii) the effect of evolution domains on differential equations, iii) the temporal effect of differential equations, and iv) static equations of differential forms.


4. André Platzer and Yong Kiam Tan.
   Differential equation invariance axiomatization.
   J. ACM 67(1), 6:1-6:66, 2020. © The authors
   [bib | ⧉ | pdf | doi | slides | video | arXiv | LICS'18 | abstract]
   
   
Fundamental result proving completeness of the Differential Dynamic Logic axiomatization for differential equation invariants, i.e., all true real arithmetic invariants of polynomial differential equation systems are provable and all false ones are disprovable, giving a logical decision procedure. First, all true algebraic properties of polynomial differential equation systems are shown to be provable by exploiting differential ghosts, which introduce additional variables that can be chosen to evolve freely along new differential equations. Completeness for real arithmetic invariants then reduces to local progress properties using algebraic completeness. Thanks to the parsimonious axiomatization of Differential Dynamic Logic, soundness and completeness extend to Noetherian functions.


5. Stefan Mitsch, Khalil Ghorbal, David Vogelbacher, and André Platzer.
   Formal verification of obstacle avoidance and navigation of ground robots.
   International Journal of Robotics Research 36(12), pp. 1312-1340, 2017. © The authors
   [bib | ⧉ | pdf | doi | kyx | arXiv | abstract]
   
   
Applies Differential Dynamic Logic and KeYmaera X to answer fundamental safety questions for ground robot navigation by identifying under which circumstances which control decision makes a ground robot provably safely avoid both static and dynamic obstacles. Proves correctness of the resulting controllers for static safety, passive safety, passive friendly safety, and passive orientation safety. The paper proves safety despite limited sensor uncertainty and actuator disturbance and also proves liveness results for robot controllers. These safe controllers for mobile ground robots also form an important basis for safe autonomous driving or more generally making autonomous CPS on the ground safe.

Quickly: What to Read When

This page gives suggestions of what papers to read for what purposes. In a nutshell:

Technical Survey:

Invited Tutorial at LICS'12 [22] surveys many important aspects, easily readable.

Exemplaric Survey:

SCP [58] surveys some important aspects of differential dynamic logic and its siblings with prototypical examples and applications.

High-level Survey:

Invited Paper at IJCAR'16' [38] gives a brief manifesto for multi-dynamical systems.

Comprehensive Reading:

Textbook'18 [44] provides exceedingly readable and thorough material and videos. Comprehensive logical background on the sequent calculus of dL is in in the Book'10.

Technical Development:

Differential dynamic logic in JAR'17 [39] provides a rigorous development of modern differential dynamic logic and its parsimonious proof calculus.

Differential Equation Invariants:

differential equations axiomatization in LICS'18 and JACM'20 [46,51] provide complete differential equation invariant principles.

Model Safety Transfer:

ModelPlex verified runtime validation for verified CPS models [36] relates models to reality in provably correct ways establishing the fundamental link between models and reality/code/AI etc.

Verified Compilation:

VeriPhy verified controller executables from verified CPS models [45] to x64 or ARM.

Hybrid Games:

differential game logic [35] [41] for (differential) hybrid games, including constructive hybrid games [52].

Distributed Hybrid Systems:

quantified differential dynamic logic [23].

Theory:

complete proof theory of hybrid systems establishing how all true hybrid systems properties are provable from their atoms [5,21,39,46,51].

Modeling Tutorial:

KeYmaera modeling tutorial [31] and KeYmaera X Tutorial.

Safe AI for CPS:

Combines reinforcement learning optimality with differential dynamic logic safety for Safe AI for CPS [48,49].

Out of necessity, this quick list is hopelessly incomplete. Papers with additional background and papers on further topics are pointed to on the remainder of this page. For example, it can also be very effective to start reading up about an interesting case study.

Important Foundations

A high-level overview of the principles behind the logical foundations of cyber-physical systems are in an IJCAR'16 invited paper [38]. A technical survey of many important aspects can be found in an LICS'12 invited tutorial [22]. A more recent survey based on examples is in the Science of Computer Programming 2025 [58]. 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].
• The first logic and the first relatively complete compositional proof calculus for hybrid games [35], including an expressiveness characterization and with extensions to differential hybrid games [41].
• The first known complete proof calculus for propositional game logic, based on a complete propositional game logic extension with sabotage that is equiexpressive with the modal μ-calculus [57].
• 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 proof-theoretically equate discrete = continuous = hybrid systems by a constructive proof-theoretical approach.
• An axiomatic form of differential-form 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].
• A complete axiomatization of differential equation invariants [46,51] exploiting the flexibility of differential-form dL [39], differential invariants, differential cuts [9], and differential ghosts [20] to prove all true semianalytic invariants (and disprove all false ones).
• The article introducing differential invariants, differential variants, differential cuts, and a verification logic for more general hybrid systems and differential-algebraic hybrid systems with differential inequalities and differential-algebraic 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], which were instrumental for JACM'20'.
• The first logic and the first relatively complete compositional proof calculus for distributed hybrid systems [15]
• ModelPlex, which is a systematic, proof-based way of ensuring that verified properties of CPS models apply to CPS implementations in a verifiably correct way [30,36].
• The first compositional verification approach and logic for stochastic hybrid systems [19], including proofs of measurability and well-definedness.

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

Also see publications by area.

Important Applications

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

• Next-Generation Airborne Collision Avoidance System ACAS X [40] and its game extension [55]
• Obstacle avoidance navigation for robotic ground vehicles [43]
• Medical robotic surgery system for skull-base surgery [26]
• Distributed adaptive cruise control for cars [17]
• Roundabout air traffic conflict resolution [11] with the first formal verification results for fully curved flight.
• Safe controller for the Federal Railroad Administration kinematics model [54] based on European train control system protocol ETCS [12] and train control with air brake pressure propagation [42]

Differential Dynamic Logics

The family of differential dynamic logics consists of a number of intimately related logics for different classes of multi-dynamic systems.

The most important foundational logics are:

Logic	Logic for Dynamical System	References
dL	Differential dynamic logic for hybrid systems	[5,21,39]
dGL	Differential game logic for (differential) hybrid games	[35,41,52]
QdL	Quantified differential dynamic logic for distributed hybrid systems	[15,23]
Further differential dynamic logics and extensions include:
dRL	Differential refinement logic for hybrid systems with system relations	[37,56]
dLCHP	Dynamic logic for communicating hybrid programs with parallelism	[53]
dHL	Hybrid-nominal differential dynamic logic for hybrid systems whose nominals handle hyper properties	[2,47]
DAL	Differential-algebraic dynamic logic for hybrid systems with differential-algebraic programs, differential-algebraic constraints, differential inequalities, disturbances etc.	[6,13]
dTL	Differential temporal dynamic logic for hybrid systems with temporal and throughout modalities	[13,29,50]
SdL	Stochastic differential dynamic logic for stochastic hybrid systems	[19]

Surveys of several but not all members of the family of differential dynamic logics can be found in an extended version of a LICS'12 tutorial [22,24].

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]. A very intuitive but still rigorous development is in the textbook on logical foundations of cyber-physical systems [44]

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 follow-up breakthrough gave a sound and complete axiomatization of hybrid systems relative to discrete dynamics [21], 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.

An axiomatic form of differential-form differential dynamic logic with a uniform substitution calculus [33,39] 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 up-to-date 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] and a subsequent textbook [44].

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

Select Publications

1. André Platzer.
   Hybrid dynamical systems logic and its refinements.
   Sci. Comput. Program. 239, pp. 103179, 2025. © The authors
   [bib | ⧉ | doi | mypdf | abstract]
   
   
2. Noah Abou El Wafa and André Platzer.
   Complete game logic with sabotage.
   In Pawel Sobocinski, Ugo Dal Lago and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'24, pp. 1:1-1:15, ACM, 2024. © The authors
   [bib | ⧉ | pdf | doi | slides | arXiv | abstract]
   
   
3. Enguerrand Prebet and André Platzer.
   Uniform substitution for differential refinement logic.
   In Christoph Benzmüller, Marijn J. Heule and Renate A. Schmidt, editors, Automated Reasoning, 12th International Joint Conference, IJCAR 2024, Proceedings, volume 14740 of LNCS. pp. 196-215, Springer 2024. © The authors
   [bib | ⧉ | pdf | doi | arXiv | abstract]
   
   
4. Rachel Cleveland, Stefan Mitsch and André Platzer.
   Formally verified next-generation airborne collision avoidance games in ACAS X.
   ACM Trans. Embed. Comput. Syst. 22(1), pp. 10:1-10:30, 2023. © The authors
   [bib | ⧉ | pdf | doi | kyx | arXiv | abstract]
   
   
5. Aditi Kabra, Stefan Mitsch and André Platzer.
   Verified train controllers for the Federal Railroad Administration train kinematics model: Balancing competing brake and track forces.
   IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 41(11), pp. 4409-4420, 2022. Special issue for EMSOFT 2022. © IEEE
   Best paper finalist
   [bib | ⧉ | pdf | doi | slides | video | kyx | extra | abstract]
   
   
6. Marvin Brieger, Stefan Mitsch and André Platzer.
   Uniform substitution for dynamic logic with communicating hybrid programs.
   In Brigitte Pientka and Cesare Tinelli, editors, International Conference on Automated Deduction, CADE-29, Rome, Italy, Proceedings, volume 14132 of LNCS, pp. 96-115. Springer, 2023. © The Authors
   [bib | ⧉ | pdf | doi | slides | arXiv | abstract]
   
   
7. Brandon Bohrer and André Platzer.
   Constructive hybrid games.
   In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning, 10th International Joint Conference, IJCAR 2020, Paris, France, Proceedings, Part I, volume 12166 of LNCS, pp. 454-473. Springer 2020. © The authors
   [bib | ⧉ | pdf | doi | mypdf | slides | arXiv | abstract]
   
   
8. André Platzer and Yong Kiam Tan.
   Differential equation invariance axiomatization.
   J. ACM 67(1), 6:1-6:66, 2020. © The authors
   [bib | ⧉ | pdf | doi | slides | video | arXiv | LICS'18 | abstract]
   
   
9. Katherine Cordwell and André Platzer.
   Towards physical hybrid systems.
   In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE-27, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 216-232. Springer, 2019. © Springer
   [bib | ⧉ | pdf | doi | slides | arXiv | abstract]
   
   
10. Nathan Fulton and André Platzer.
    Verifiably safe off-model reinforcement learning.
    In Tomas Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2019, Proceedings, Part I, volume 11427 of LNCS, pp. 413-430. Springer, 2019. © The authors
    [bib | ⧉ | pdf | doi | arXiv | abstract]
    
    
11. Nathan Fulton and André Platzer.
    Safe reinforcement learning via formal methods:
       Toward safe control through proof and learning.
    In Sheila A. McIlraith and Kilian Q. Weinberger, editors, AAAI Conference on Artificial Intelligence, pp. 6485-6492. AAAI 2018. © AAAI Press
    [bib | ⧉ | pdf | doi | eprint | slides | abstract]
    
    
12. Brandon Bohrer and André Platzer.
    A hybrid, dynamic logic for hybrid-dynamic information flow.
    In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, pp. 115-124. ACM 2018. © The authors. Publication rights licensed to ACM
    [bib | ⧉ | pdf | doi | slides | TR | abstract]
    
    
13. André Platzer and Yong Kiam Tan.
    Differential equation axiomatization:
       The impressive power of differential ghosts.
    In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, pp. 819-828. ACM 2018. © The authors
    [bib | ⧉ | pdf | doi | slides | video | arXiv | JACM'20 | abstract]
    
    
14. Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen and André Platzer.
    VeriPhy: Verified controller executables from verified cyber-physical system models.
    In Dan Grossmann, editor, Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pp. 617-630. ACM 2018. © The authors
    [bib | ⧉ | pdf | doi | slides | video | abstract]
    
    
15. 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]
    
    
16. Stefan Mitsch, Khalil Ghorbal, David Vogelbacher, and André Platzer.
    Formal verification of obstacle avoidance and navigation of ground robots.
    International Journal of Robotics Research 36(12), pp. 1312-1340, 2017. © The authors
    [bib | ⧉ | pdf | doi | kyx | arXiv | abstract]
    
    
17. Stefan Mitsch, Marco Gario, Christof J. Budnik, Michael Golm and André Platzer.
    Formal verification of train control with air pressure brakes.
    In Alessandro Fantechi, Thierry Lecomte and Alexander Romanovsky, editors, RSSRail 2017: Reliability, Safety, and Security of Railway Systems, volume 10598 of LNCS, pp. 173-191. Springer, 2017. © Springer
    [bib | ⧉ | pdf | doi | slides | abstract]
    
    
18. André Platzer.
    Differential hybrid games.
    ACM Trans. Comput. Log. 18(3), pp. 19:1-19:44, 2017. © The author
    [bib | ⧉ | pdf | doi | arXiv | abstract]
    
    
19. Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Aurora Schmidt, Ryan Gardner, Stefan Mitsch, and André Platzer.
    A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system.
    STTT 19(6), pp. 717-741, 2017.
    Special issue for selected papers from TACAS'15. © Springer
    [bib | ⧉ | pdf | doi | kyx | study | TACAS'15 | abstract]
    
    
20. André Platzer.
    A complete uniform substitution calculus for differential dynamic logic.
    Journal of Automated Reasoning 59(2), pp. 219-265, 2017. © The author
    [bib | ⧉ | pdf | doi | mypdf | arXiv | abstract]
    
    
21. André Platzer.
    Logic & proofs for cyber-physical systems.
    In Nicola Olivetti and Ashish Tiwari, editors, Automated Reasoning, 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, Proceedings, volume 9706 of LNCS, pp. 15-21. Springer, 2016. © Springer
    Invited paper.
    [bib | ⧉ | pdf | doi | slides | abstract]
    
    
22. Sarah M. Loos and André Platzer.
    Differential refinement logic.
    ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, July 5–8, 2016, New York, NY, USA, pp. 505-514. ACM, 2016. © The authors
    [bib | ⧉ | pdf | doi | slides | abstract]
    
    
23. Stefan Mitsch and André Platzer.
    ModelPlex: Verified runtime validation of verified cyber-physical system models.
    Formal Methods in System Design 49(1), pp. 33-74. 2016.
    Special issue for selected papers from RV'14. © The authors
    [bib | ⧉ | pdf | doi | mypdf | RV'14 | abstract]
    
    
24. André Platzer.
    Differential game logic.
    ACM Trans. Comput. Log. 17(1), pp. 1:1-1:52, 2015. © The author
    [bib | ⧉ | pdf | doi | arXiv | errata | abstract]
    
    
25. Nathan Fulton, Stefan Mitsch, Jan-David 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-25, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 527-538. Springer, 2015. © Springer
    [bib | ⧉ | pdf | doi | slides | poster | tool | tooldoi | abstract]
    
    
26. André Platzer.
    A uniform substitution calculus for differential dynamic logic.
    In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE-25, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 467-481. Springer, 2015. © Springer
    [bib | ⧉ | pdf | doi | slides | arXiv | JAR'17 | abstract]
    
    
27. 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]
    
    
28. 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]
    
    
29. 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]
    
    
30. Jean-Baptiste Jeannin and André Platzer.
    dTL²: 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 19-22, 2014, Proceedings, volume 8562 of LNCS, pp. 292-306. Springer, 2014. © Springer
    [bib | ⧉ | pdf | doi | slides | abstract]
    
    
31. 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]
    
    
32. 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]
    
    
33. 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]
    
    
34. 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]
    
    
35. 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]
    
    
36. 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]
    
    
37. 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]
    
    
38. 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]
    
    
39. 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]
    
    
40. 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-23, Wroclaw, Poland, Proceedings, volume 6803 of LNCS, pp. 446-460. Springer, 2011. © Springer
    [bib | ⧉ | pdf | doi | slides | TR | abstract]
    
    
41. 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]
    
    
42. 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]
    
    
43. 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]
    
    
44. 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]
    
    
45. 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, pp. 243-252. ACM, 2010. © ACM
    [bib | ⧉ | pdf | doi | slides | TR | abstract]
    
    
46. 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]
    
    
47. 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]
    
    
48. 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]
    
    
49. 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]
    
    
50. 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]
    
    
51. 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]
    
    
52. 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]
    
    
53. 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]
    
    
54. 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]
    
    
55. 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]
    
    
56. 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. 473-486. Springer, 2007, © Springer
    [bib | ⧉ | pdf | doi | slides | tool | abstract]
    
    
57. 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]
    
    
58. 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, pp. 266-280. Springer, 2006. © Springer
    [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.