Table of Contents 

List of Publications
[ORCID  DBLP  Google Scholar  by year  by area  abstracts  guide]Textbooks

Books

Book Chapters

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. 2164. Springer, 2020. © Springer
[bib  ✂  pdf  doi]This chapter provides a retrospective on the developments of three theorem provers for hybrid systems. While all three theorem provers implement closely related logics of the family of differential dynamic logic, they pursue fundamentally different styles of theorem prover implementations. Since the three provers KeYmaera, KeYmaeraD, and KeYmaera X share a common core logic, yet no line of code, and differ vastly in prover implementation technology, their logical proximity yet technical distance enables us to draw conclusions about the various advantages and disadvantages of different prover implementation styles for different purposes, which we hope are of generalizable interest.
Keywords: History of formal methods • Theorem provers • Differential dynamic logic • Hybrid systems

André Platzer.
Overview of logical foundations of cyberphysical systems.
In Helmut Seidl, editor, Postproceedings of the Summer School Marktoberdorf: Safety and Security of Software Systems  Logics, Proofs, Applications, TUM University Press, 2020. © The author
[bib  ✂  pdf  eprint  arXiv]Cyberphysical systems (CPSs) are important whenever computer technology interfaces with the physical world as it does in selfdriving cars or aircraft control support systems. Due to their many subtleties, controllers for cyberphysical systems deserve to be held to the highest correctness standards. Their correct functioning is crucial, which explains the broad interest in safety analysis technology for their mathematical models, which are called hybrid systems because they combine discrete dynamics with continuous dynamics. Differential dynamic logic (dL) provides logical specification and rigorous reasoning techniques for hybrid systems. The logic dL is implemented in the theorem prover KeYmaera X, which has been instrumental in verifying ground robot controllers, railway systems, and the nextgeneration airborne collision avoidance system ACAS X. This chapter provides an informal overview of this logical approach to CPS safety that is detailed in a recent textbook on Logical Foundations of CyberPhysical Systems. It also explains how safety guarantees obtained in the land of verified models reach the level of CPS execution unharmed.
Keywords: Cyberphysical systems • Differential dynamic logic • Hybrid systems • Theorem proving • Formal verification

Laurent Doyen, Goran Frehse, George J. Pappas, and André Platzer.
Verification of hybrid systems.
In Edmund M. Clarke and Thomas A. Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pp. 10471110. Springer, 2018. © Springer
[bib  ✂  pdf  doi  book]Hybrid systems are models with joint discrete and continuous behavior. They occur frequently in safetycritical applications in various domains such as health care, transportation, and robotics, as a result of interactions between a digital controller and a physical environment. They also have relevance in other areas such as systems biology, in which the discrete dynamics arises as an abstraction of fast continuous processes. One of the prominent models is that of hybrid automata, where differential equations are associated with each node, and jump constraints such as guards and resets are associated with each edge.
In this chapter, we focus on the problem of model checking of hybrid automata against reachability and invariance properties, enabling the techniques for the verification of general temporal logic specifications. We review the main decidability results for hybrid automata, and since modelchecking is in general undecidable, we present three complementary analysis approaches based on symbolic representations, abstraction, and logic. In particular, we illustrate polyhedronbased reachability analysis, finite quotients, abstraction refinement techniques, and logicbased verification. We survey important tools and application domains of successful hybrid system verification in this vibrant area of research.
Journal Publications

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. Special issue for EMSOFT 2022. To appear. © IEEE
[bib  ✂  doi  kyx]Automated train control improves railroad operation by safeguarding the motion of trains while increasing efficiency by enabling motion within a safe envelope. Train controllers decide when to slow trains down to avoid collisions with other trains on the track, stay inside movement authorities, and navigate slopes, curves and tunnels safely. These systems must base their decisions on detailed motion models to guarantee the absence of overshoot of the movement authority (safety) and limit undershoot (efficiency). This paper is the first to formally verify the safety of the Federal Railroad Administration freight train kinematics model with all its relevant forces and parameters, including track slope and curvature, air brake propagation, and resistive forces as computed by the Davis equation. Due to the significant competing influence of these parameters on train stopping distances, even designing train controllers is a nontrivial control challenge, which we solve using formal verification. For increased generality at reduced verification effort, we verify symbolic mathematical generalizations of the train control models and subsequently apply efficient uniform substitutions to obtain verification results for physical train control models.
Keywords: Train control • Formal verification • Hybrid systems • Differential dynamic logic

Rachel Cleveland, Stefan Mitsch and André Platzer.
Formally verified nextgeneration airborne collision avoidance games in ACAS X.
ACM Trans. Embed. Comput. Syst. To appear. © The authors
[bib  ✂  pdf  doi  kyx  arXiv]The design of aircraft collision avoidance algorithms is a subtle but important challenge that merits the need for provable safety guarantees. Obtaining such guarantees is nontrivial given the unpredictability of the interplay of the intruder aircraft decisions, the ownship pilot reactions, and the subtlety of the continuous motion dynamics of aircraft. Existing collision avoidance systems, such as TCAS and the NextGeneration Airborne Collision Avoidance System ACAS X, have been analyzed assuming severe restrictions on the intruder's flight maneuvers, limiting their safety guarantees in realworld scenarios where the intruder may change its course.
This work takes a conceptually significant and practically relevant departure from existing ACAS X models by generalizing them to hybrid games with firstclass representations of the ownship and intruder decisions coming from two independent players, enabling significantly advanced predictive power. By proving the existence of winning strategies for the resulting Adversarial ACAS X in differential game logic, collisionfreedom is established for the rich encounters of ownship and intruder aircraft with independent decisions along differential equations for flight paths with evolving vertical/horizontal velocities. We present three classes of models of increasing complexity: singleadvisory infinitetime models, bounded time models, and infinite time, multiadvisory models. Within each class of models, we identify symbolic conditions and prove that there then always is a possible ownship maneuver that will prevent a collision between the two aircraft.
Keywords: Airborne collision avoidance • ACAS X • Theorem proving • Hybrid games • Differential game logic

Qin Lin, Stefan Mitsch, André Platzer and John M. Dolan.
Safe and resilient practical waypointfollowing for autonomous vehicles.
IEEE Control Syst. Lett. 6, pp. 15741579, 2022. © IEEE
[bib  ✂  doi]We combine theorem proving and reachability analysis for cyberphysical systems verification to arrive at a practical approach to safe waypointfollowing for an autonomous mobile vehicle controlled by a learningenabled controller. We propose a robust monitor verifying shortterm and longterm safety simultaneously at runtime, thereby combining the benefits of both theorem proving and reachability analysis. The proposed novel monitor architecture allows temporary violation of longterm safety while maintaining shortterm safety to recover to a state with longterm safety. The recovery is based on a fallback model predictive controller. The experiments conducted in a highfidelity racing car simulator demonstrate that our framework is safe and resilient in path tracking scenarios, in which avoiding collision with the race track boundary and obstacles is required.
Keywords: Reachability analysis • Theorem proving • Safety verification • Safe control • Learningenabled control

Brandon Bohrer and André Platzer.
Structured proofs for adversarial cyberphysical systems.
ACM Trans. Embed. Comput. Syst. 20(5s), pp. 93:193:26, 2021.
Special issue on EMSOFT 2021. © The authors
[bib  ✂  pdf  doi  mypdf  arXiv]Many cyberphysical systems (CPS) are safetycritical, so it is important to formally verify them, e.g. in formal logics that show a model's correctness specification always holds. Constructive Differential Game Logic (CdGL) is such a logic for (constructive) hybrid games, including hybrid systems. To overcome undecidability, the user first writes a proof, for which we present a proofchecking tool.
We introduce Kaisar, the first language and tool for CdGL proofs, which until now could only be written by hand with a lowlevel proof calculus. Kaisar's structured proofs simplify challenging CPS proof tasks, especially by using programming language principles and highlevel stateful reasoning. Kaisar exploits CdGL's constructivity and refinement relations to build proofs around models of game strategies. The evaluation reproduces and extends existing case studies on 1D and 2D driving. Proof metrics are compared and reported experiences are discussed for the original studies and their reproductions.
Keywords: Cyberphysical systems • Hybrid games • Formal proof • Structured proofs

Yong Kiam Tan and André Platzer.
An axiomatic approach to existence and liveness for differential equations.
Formal Aspects of Computing 33(4), pp. 461518, 2021.
Special issue for selected papers from FM'19. © The authors
[bib  ✂  pdf  doi  arXiv  FM'19]This article presents an axiomatic approach for deductive verification of existence and liveness for ordinary differential equations (ODEs) with differential dynamic logic (dL). The approach yields proofs that the solution of a given ODE exists long enough to reach a given target region without leaving a given evolution domain. Numerous subtleties complicate the generalization of discrete liveness verification techniques, such as loop variants, to the continuous setting. For example, ODE solutions may blow up in finite time or their progress towards the goal may converge to zero. These subtleties are handled in dL by successively refining ODE liveness properties using ODE invariance properties which have a complete axiomatization. This approach is widely applicable: several liveness arguments from the literature are surveyed and derived as special instances of axiomatic refinement in dL. These derivations also correct several soundness errors in the surveyed literature, which further highlights the subtlety of ODE liveness reasoning and the utility of an axiomatic approach. An important special case of this approach deduces (global) existence properties of ODEs, which are a fundamental part of every ODE liveness argument. Thus, all generalizations of existence properties and their proofs immediately lead to corresponding generalizations of ODE liveness arguments. Overall, the resulting library of common refinement steps enables both the sound development and justification of new ODE existence and of liveness proof rules from dL axioms. These insights are put into practice through an implementation of ODE liveness proofs in the KeYmaera X theorem prover for hybrid systems.
Keywords: Differential equations • Liveness • Global existence • Differential dynamic logic

Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell and André Platzer.
Pegasus: Sound continuous invariant generation.
Formal Methods in System Design 58(1), pp. 541, 2022.
Special issue for selected papers from FM'19. © The authors
[bib  ✂  pdf  doi  tool  arXiv  FM'19]Continuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without unrolling their loops forever, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges to the automation of formal proofs of safety for hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.
Keywords: Invariant generation • Continuous invariants • Ordinary differential equations • Theorem proving

André Platzer and Yong Kiam Tan.
Differential equation invariance axiomatization.
J. ACM 67(1), 6:16:66, 2020. © The authors
[bib  ✂  pdf  doi  mypdf  slides  video  arXiv]This article proves the completeness of an axiomatization for differential equation invariants described by Noetherian functions. First, the differential equation axioms of differential dynamic logic are shown to be complete for reasoning about analytic invariants. Completeness crucially exploits differential ghosts, which introduce additional variables that can be chosen to evolve freely along new differential equations. Cleverly chosen differential ghosts are the prooftheoretical counterpart of dark matter. They create new hypothetical state, whose relationship to the original state variables satisfies invariants that did not exist before. The reflection of these new invariants in the original system then enables its analysis.
An extended axiomatization with existence and uniqueness axioms is complete for all local progress properties, and, with a real induction axiom, is complete for all semianalytic invariants. This parsimonious axiomatization serves as the logical foundation for reasoning about invariants of differential equations. Indeed, it is precisely this logical treatment that enables the generalization of completeness to the Noetherian case.
Keywords: Differential equation axiomatization • Invariants • Differential dynamic logic • Differential ghosts • Noetherian functions

Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Andrew Sogokon and André Platzer.
A formal safety net for waypoint following in ground robots.
IEEE Robotics and Automation Letters 4(3), pp. 29102917, 2019. © IEEE
[bib  ✂  pdf  doi  kyx  study  arXiv]We present a reusable formally verified safety net that provides endtoend safety and liveness guarantees for 2D waypointfollowing of Dubinstype ground robots with tolerances and acceleration. We: i) Model a robot in differential dynamic logic (dL), and specify assumptions on the controller and robot kinematics, ii) Prove formal safety and liveness properties for waypointfollowing with speed limits, iii) Synthesize a monitor, which is automatically proven to enforce model compliance at runtime, and iv) Our use of the VeriPhy toolchain makes these guarantees carry over down to the level of machine code with untrusted controllers, environments, and plans. The guarantees for the safety net apply to any robot as long as the waypoints are chosen safely and the physical assumptions in its model hold. Experiments show these assumptions hold in practice, with an inherent tradeoff between compliance and performance.
Keywords: Theorem proving • Safety verification • Liveness verification • Waypoint navigation • Robot motion control • Hybrid systems

Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger and André Platzer.
Tactical contract composition for hybrid system component verification.
STTT 20(6), pp. 615643, 2018.
Special issue for selected papers from FASE'17. © The authors
[bib  ✂  pdf  doi  mypdf  study  FASE'17]We present an approach for hybrid systems that combines the advantages of componentbased modeling (e.g., reduced model complexity) with the advantages of formal verification (e.g., guaranteed contract compliance). Componentbased modeling can be used to split large models into multiple component models with local responsibilities to reduce modeling complexity. Yet, this only helps the analysis if verification proceeds one component at a time. In order to benefit from the decomposition of a system into components for both modeling and verification purposes, we prove that the safety of compatible components implies safety of the composed system. We implement our composition theorem as a tactic in the KeYmaera X theorem prover, allowing automatic generation of a KeYmaera X proof for the composite system from proofs for the components without soundnesscritical changes to KeYmaera X.
Our approach supports component contracts (i.e., input assumptions and output guarantees for each component) that characterize the magnitude and rate of change of values exchanged between components. These contracts can take into account what has changed between two components in a given amount of time since the last exchange of information.
Keywords: Componentbased development • Hybrid systems • Componentbased verification

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. 13121340, 2017. © The authors
[bib  ✂  pdf  doi  kyx  arXiv]This article answers fundamental safety questions for ground robot navigation: Under which circumstances does which control decision make a ground robot safely avoid obstacles? Unsurprisingly, the answer depends on the exact formulation of the safety objective as well as the physical capabilities and limitations of the robot and the obstacles. Because uncertainties about the exact future behavior of a robot's environment make this a challenging problem, we formally verify corresponding controllers and provide rigorous safety proofs justifying why they can never collide with the obstacle in the respective physical model. To account for ground robots in which different physical phenomena are important, we analyze a series of increasingly strong properties of controllers for increasingly rich dynamics and identify the impact that the additional model parameters have on the required safety margins.
We analyze and formally verify: (i) static safety, which ensures that no collisions can happen with stationary obstacles, (ii) passive safety, which ensures that no collisions can happen with stationary or moving obstacles while the robot moves, (iii) the stronger passive friendly safety in which the robot further maintains sufficient maneuvering distance for obstacles to avoid collision as well, and (iv) passive orientation safety, which allows for imperfect sensor coverage of the robot, i.e., the robot is aware that not everything in its environment will be visible. We formally prove that safety can be guaranteed despite sensor uncertainty and actuator perturbation. We complement these provably correct safety properties with liveness properties: we prove that provably safe motion is flexible enough to let the robot navigate waypoints and pass intersections. In order to account for the mixed influence of discrete control decisions and the continuous physical motion of the ground robot, we develop corresponding hybrid system models and use differential dynamic logic theorem proving techniques to formally verify their correctness. Since these models identify a broad range of conditions under which control decisions are provably safe, our results apply to any control algorithm for ground robots with the same dynamics. As a demonstration, we, thus, also synthesize provably correct runtime monitor conditions that check the compliance of any control algorithm with the verified control decisions.
Keywords: Provable correctness • Obstacle avoidance • Ground robot • Navigation • Hybrid systems • Theorem proving

JeanBaptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Aurora Schmidt, Ryan Gardner, Stefan Mitsch, and André Platzer.
A formally verified hybrid system for safe advisories in the nextgeneration airborne collision avoidance system.
STTT 19(6), pp. 717741, 2017.
Special issue for selected papers from TACAS'15. © Springer
[bib  ✂  pdf  doi  kyx  study  TACAS'15]The NextGeneration Airborne Collision Avoidance System (ACAS X) is intended to be installed on all large aircraft to give advice to pilots and prevent midair collisions with other aircraft. It is currently being developed by the Federal Aviation Administration (FAA). In this paper we determine the geometric configurations under which the advice given by ACAS X is safe under a precise set of assumptions and formally verify these configurations using hybrid systems theorem proving techniques. We consider subsequent advisories and show how to adapt our formal verification to take them into account. We examine the current version of the real ACAS X system and discuss some cases where our safety theorem conflicts with the actual advisory given by that version, demonstrating how formal hybrid systems proving approaches are helping to ensure the safety of ACAS X. Our approach is general and could also be used to identify unsafe advice issued by other collision avoidance systems or confirm their safety.
Keywords: Airborne Collision Avoidance • ACAS X • Hybrid systems • Theorem proving • Federal Aviation Administration • Aircraft • Markov decision processes • Cyberphysical systems

André Platzer.
Differential hybrid games.
ACM Trans. Comput. Log. 18(3), pp. 19:119:44, 2017. © The author
[bib  ✂  pdf  doi  mypdf  arXiv]This paper introduces differential hybrid games, which combine differential games with hybrid games. In both kinds of games, two players interact with continuous dynamics. The difference is that hybrid games also provide all the features of hybrid systems and discrete games, but only deterministic differential equations. Differential games, instead, provide differential equations with input by both players, but not the luxury of hybrid games, such as mode switches and discrete or alternating interaction. This paper augments differential game logic with modalities for the combined dynamics of differential hybrid games. It shows how hybrid games subsume differential games and introduces differential game invariants and differential game variants for proving properties of differential games inductively.
Keywords: differential games • hybrid games • differential game game logic • differential game invariants • partial differential equations • viscosity solutions • real algebraic geometry

Khalil Ghorbal, Andrew Sogokon, and André Platzer.
A hierarchy of proof rules for checking positive invariance of algebraic and semialgebraic sets.
Computer Languages, Systems & Structures 47(1), pp. 1943, 2017.
Special issue for selected papers from VMCAI'15. © Elsevier
[bib  ✂  pdf  doi  study  VMCAI'15]This paper studies sound proof rules for checking positive invariance of algebraic and semialgebraic sets, that is, sets satisfying polynomial equalities and those satisfying finite boolean combinations of polynomial equalities and inequalities, under the flow of polynomial ordinary differential equations. Problems of this nature arise in formal verification of continuous and hybrid dynamical systems, where there is an increasing need for methods to expedite formal proofs. We study the tradeoff between proof rule generality and practical performance and evaluate our theoretical observations on a set of benchmarks. The relationship between increased deductive power and running time performance of the proof rules is far from obvious; we discuss and illustrate certain classes of problems where this relationship is interesting.
Keywords: Formal verification • Polynomial differential equations • Positive invariance • Deductive power • Dynamical systems

André Platzer.
A complete uniform substitution calculus for differential dynamic logic.
Journal of Automated Reasoning 59(2), pp. 219265, 2017. © The author
[bib  ✂  pdf  doi  mypdf  arXiv]This article introduces a relatively complete proof calculus for differential dynamic logic (dL) that is entirely based on uniform substitution, a proof rule that substitutes a formula for a predicate symbol everywhere. Uniform substitutions make it possible to use axioms instead of axiom schemata, thereby substantially simplifying implementations. Instead of subtle schema variables and soundnesscritical side conditions on the occurrence patterns of logical variables to restrict infinitely many axiom schema instances to sound ones, the resulting calculus adopts only a finite number of ordinary dL formulas as axioms, which uniform substitutions instantiate soundly. The static semantics of differential dynamic logic and the soundnesscritical restrictions it imposes on proof steps is captured exclusively in uniform substitutions and variable renamings as opposed to being spread in delicate ways across the prover implementation. In addition to sound uniform substitutions, this article introduces differential forms for differential dynamic logic that make it possible to internalize differential invariants, differential substitutions, and derivatives as firstclass axioms to reason about differential equations axiomatically. The resulting axiomatization of differential dynamic logic is proved to be sound and relatively complete.
Keywords: differential dynamic logic • uniform substitution • axioms • differentials • static semantics • axiomatization

Stefan Mitsch and André Platzer.
ModelPlex: Verified runtime validation of verified cyberphysical system models.
Formal Methods in System Design 49(1), pp. 3374. 2016.
Special issue for selected papers from RV'14. © The authors
[bib  ✂  pdf  doi  mypdf  RV'14]Formal verification and validation play a crucial role in making cyberphysical systems (CPS) safe. Formal methods make strong guarantees about the system behavior if accurate models of the system can be obtained, including models of the controller and of the physical dynamics. In CPS, models are essential; but any model we could possibly build necessarily deviates from the real world. If the real system fits to the model, its behavior is guaranteed to satisfy the correctness properties verified with respect to the model. Otherwise, all bets are off.
This article introduces ModelPlex, a method ensuring that verification results about models apply to CPS implementations. ModelPlex provides correctness guarantees for CPS executions at runtime: it combines offline verification of CPS models with runtime validation of system executions for compliance with the model. ModelPlex ensures in a provably correct way that the verification results obtained for the model apply to the actual system runs by monitoring the behavior of the world for compliance with the model. If, at some point, the observed behavior no longer complies with the model so that offline verification results no longer apply, ModelPlex initiates provably safe fallback actions, assuming the system dynamics deviation is bounded. This article, furthermore, develops a systematic technique to synthesize provably correct monitors automatically from CPS proofs in differential dynamic logic by a correctbyconstruction approach, leading to verifiably correct runtime model validation. Overall, ModelPlex generates provably correct monitor conditions that, if checked to hold at runtime, are provably guaranteed to imply that the offline safety verification results about the CPS model apply to the present run of the actual CPS implementation.
Keywords: Runtime verification • Static verification • Cyberphysical systems • Hybrid systems • Differential dynamic logic

JanDavid Quesel, Stefan Mitsch, Sarah Loos, Nikos Aréchiga, and André Platzer.
How to model and prove hybrid systems with KeYmaera: A tutorial on safety.
STTT 18(1), pp. 6791, 2016. © The authors
[bib  ✂  pdf  doi  mypdf]This paper is a tutorial on how to model hybrid systems as hybrid programs in differential dynamic logic and how to prove complex properties about these complex hybrid systems in KeYmaera, an automatic and interactive formal verification tool for hybrid systems. Hybrid systems can model highly nontrivial controllers of physical plants, whose behaviors are often safety critical such as trains, cars, airplanes, or medical devices. Formal methods can help design systems that work correctly. This paper illustrates how KeYmaera can be used to systematically model, validate, and verify hybrid systems. We develop tutorial examples that illustrate challenges arising in many realworld systems. In the context of this tutorial, we identify the impact that modeling decisions have on the suitability of the model for verification purposes. We show how the interactive features of KeYmaera can help users understand their system designs better and prove complex properties for which the automatic prover of KeYmaera still takes an impractical amount of time. We hope this paper is a helpful resource for designers of embedded and cyberphysical systems and that it illustrates how to master common practical challenges in hybrid systems verification.
Keywords: KeYmaera tutorial • Formal verification of hybrid systems • Differential dynamic logic • Automated theorem proving • Introduction to hybrid system modeling and verification

André Platzer.
Differential game logic.
ACM Trans. Comput. Log. 17(1), pp. 1:11:52, 2015. © The author
[bib  ✂  pdf  doi  mypdf  arXiv  errata]Differential game logic (dGL) is a logic for specifying and verifying properties of hybrid games, i.e. games that combine discrete, continuous, and adversarial dynamics. Unlike hybrid systems, hybrid games allow choices in the system dynamics to be resolved adversarially by different players with different objectives. The logic dGL can be used to study the existence of winning strategies for such hybrid games, i.e. ways of resolving the player's choices in some way so that he wins by achieving his objective for all choices of the opponent. Hybrid games are determined, i.e. from each state, one player has a winning strategy, yet computing their winning regions may take transfinitely many steps. The logic dGL, nevertheless, has a sound and complete axiomatization relative to any expressive logic. Separating axioms are identified that distinguish hybrid games from hybrid systems. Finally, dGL is proved to be strictly more expressive than the corresponding logic of hybrid systems by characterizing the expressiveness of both.
Keywords: Game logic • hybrid games • axiomatization • expressiveness

Stefan Mitsch, André Platzer, Werner Retschitzegger and Wieland Schwinger.
Logicbased modeling approaches for qualitative and hybrid reasoning in dynamic spatial systems.
ACM Computing Surveys 48(1), 2015. © ACM
[bib  ✂  pdf  doi]Autonomous agents that operate as components of dynamic spatial systems are becoming increasingly popular and mainstream. Applications can be found in consumer robotics, in road, rail, and air transportation, manufacturing, and military operations. Unfortunately, the approaches to modeling and analyzing the behavior of dynamic spatial systems are just as diverse as these application domains. In this paper, we discuss reasoning approaches for the mediumterm control of autonomous agents in dynamic spatial systems, which requires a sufficiently detailed description of the agent's behavior and environment, but may still be conducted in a qualitative manner. We survey logicbased qualitative and hybrid modeling and commonsense reasoning approaches w.r.t. their features for describing and analyzing dynamic spatial systems in general, and the actions of autonomous agents operating therein in particular. We introduce a conceptual reference model, which summarizes the current understanding of the characteristics of dynamic spatial systems based on a catalog of evaluation criteria derived from the model. We assess the modeling features provided by logicbased qualitative commonsense and hybrid approaches for projection, planning, simulation, and verification of dynamic spatial systems. We provide a comparative summary of the modeling features, discuss lessons learned, and introduce a research roadmap for integrating different approaches of dynamic spatial system analysis to achieve coverage of all required features.
Keywords: Autonomous agents • logicbased reasoning • commonsense reasoning • dynamic reasoning • dynamic spatial systems • knowledge representation • hybrid systems

Khalil Ghorbal, JeanBaptiste Jeannin, Erik P. Zawadzki, André Platzer, Geoffrey J. Gordon, and Peter Capell.
Hybrid theorem proving of aerospace systems: Applications and challenges.
Journal of Aerospace Information Systems 11(10), pp. 702713. 2014.
Special issue on Software Challenges in Aerospace. © The authors
[bib  ✂  pdf  doi]Complex software systems are becoming increasingly prevalent in aerospace applications, in particular to accomplish critical tasks. Ensuring the safety of these systems is crucial, while they can have subtly different behavior under slight variations in operating conditions. In this paper we advocate the use of formal verification techniques and in particular theorem proving for hybrid softwareintensive systems as a wellfounded complementary approach to the classical aerospace verification and validation techniques such as testing or simulation. As an illustration of these techniques, we study a novel lateral midair collision avoidance maneuver in an ideal setting, without accounting for the uncertainties of the physical reality. We then detail the challenges that naturally arise when applying such technology to industrialscale applications and our proposals on how to address these issues.

Akshay Rajhans, Ajinkya Bhave, Ivan Ruchkin, Bruce H. Krogh, David Garlan, André Platzer and Bradley Schmerl.
Supporting heterogeneity in cyberphysical systems architectures.
IEEE Transactions on Automatic Control 59(12), pp. 31783193, 2014.
Special issue on Control of CyberPhysical Systems. © IEEE
[bib  ✂  pdf  doi]Cyberphysical systems (CPS) are heterogeneous, because they tightly couple computation, communication and control along with physical dynamics, which are traditionally considered separately. Without a comprehensive modeling formalism, modelbased development of CPS involves using a multitude of models in a variety of formalisms that capture various aspects of the system design, such as software design, networking design, physical models, and protocol design. Without a rigorous unifying framework, system integration and integration of the analysis results for various models remains ad hoc. In this paper, we propose a multiview architecture framework that treats models as views of the underlying system structure and uses structural and semantic mappings to ensure consistency and enable systemlevel verification in a hierarchical and compositional manner. Throughout the paper, the theoretical concepts are illustrated using two examples, a quadrotor and an automotive intersection collision avoidance system.

Stefan Mitsch, Grant Olney Passmore and André Platzer.
Collaborative verificationdriven engineering of hybrid systems.
Mathematics in Computer Science 8(1), pp. 7197, 2014.
Special issue on Enabling Domain Experts to use Formalized Reasoning. © Springer
[bib  ✂  pdf  doi  arXiv]Hybrid systems with both discrete and continuous dynamics are an important model for realworld cyberphysical systems. The key challenge is to ensure their correct functioning w.r.t. safety requirements. Promising techniques to ensure safety seem to be modeldriven engineering to develop hybrid systems in a welldefined and traceable manner, and formal verification to prove their correctness. Their combination forms the vision of verificationdriven engineering. Often, hybrid systems are rather complex in that they require expertise from many domains (e. g., robotics, control systems, computer science, software engineering, and mechanical engineering). Moreover, despite the remarkable progress in automating formal verification of hybrid systems, the construction of proofs of complex systems often requires nontrivial human guidance, since hybrid systems verification tools solve undecidable problems. It is, thus, not uncommon for development and verification teams to consist of many players with diverse expertise. This paper introduces a verificationdriven engineering toolset that extends our previous work on hybrid and arithmetic verification with tools for (1) graphical (UML) and textual modeling of hybrid systems, (2) exchanging and comparing models and proofs, and (3) managing verification tasks. This toolset makes it easier to tackle largescale verification tasks.
Keywords: Formal verification • Hybrid system • Cyberphysical system • Modeldriven engineering

Paolo Zuliani, André Platzer and Edmund M. Clarke.
Bayesian statistical model checking with application to Simulink/Stateflow verification.
Formal Methods in System Design 43(2), pp. 338367, 2013.
Special issue on Probabilistic Model Checking. © Springer
[bib  ✂  pdf  doi]We address the problem of model checking stochastic systems, i.e., checking whether a stochastic system satisfies a certain temporal property with a probability greater (or smaller) than a fixed threshold. In particular, we present a Statistical Model Checking (SMC) approach based on Bayesian statistics. We show that our approach is feasible for a certain class of hybrid systems with stochastic transitions, a generalization of Simulink/Stateflow models. Standard approaches to stochastic discrete systems require numerical solutions for large optimization problems and quickly become infeasible with larger state spaces. Generalizations of these techniques to hybrid systems with stochastic effects are even more challenging. The SMC approach was pioneered by Younes and Simmons in the discrete and nonBayesian case. It solves the verification problem by combining randomized sampling of system traces (which is very efficient for Simulink/Stateflow) with hypothesis testing (i.e., testing against a probability threshold) or estimation (i.e., computing with high probability a value close to the true probability). We believe SMC is essential for scaling up to large Stateflow/Simulink models. While the answer to the verification problem is not guaranteed to be correct, we prove that Bayesian SMC can make the probability of giving a wrong answer arbitrarily small. The advantage is that answers can usually be obtained much faster than with standard, exhaustive model checking techniques. We apply our Bayesian SMC approach to a representative example of stochastic discretetime hybrid system models in Stateflow/Simulink: a fuel control system featuring hybrid behavior and fault tolerance. We show that our technique enables faster verification than stateoftheart statistical techniques. We emphasize that Bayesian SMC is by no means restricted to Stateflow/Simulink models. It is in principle applicable to a variety of stochastic models from other domains, e.g., systems biology.
Keywords: Probabilistic verification • Hybrid systems • Stochastic systems • Statistical model checking • Hypothesis testing • Estimation

André Platzer.
A complete axiomatization of quantified differential dynamic logic for distributed hybrid systems.
Logical Methods in Computer Science 8(4), pp. 144, 2012.
Special issue for selected papers from CSL'10. © The author
[bib  ✂  pdf  doi  arXiv  CSL'10]We address a fundamental mismatch between the combinations of dynamics that occur in cyberphysical systems and the limited kinds of dynamics supported in analysis. Modern applications combine communication, computation, and control. They may even form dynamic distributed networks, where neither structure nor dimension stay the same while the system follows hybrid dynamics, i.e., mixed discrete and continuous dynamics.
We provide the logical foundations for closing this analytic gap. We develop a formal model for distributed hybrid systems. It combines quantified differential equations with quantified assignments and dynamic dimensionalitychanges. We introduce a dynamic logic for verifying distributed hybrid systems and present a proof calculus for this logic. This is the first formal verification approach for distributed hybrid systems. We prove that our calculus is a sound and complete axiomatization of the behavior of distributed hybrid systems relative to quantified differential equations. In our calculus we have proven collision freedom in distributed car control even when an unbounded number of new cars may appear dynamically on the road.
Keywords: Differential dynamic logic • Distributed hybrid systems • Axiomatization • Theorem proving • Quantified differential equations • Proof theory

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  mypdf  arXiv]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

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. © Springer
[bib  ✂  pdf  doi  study  CAV'08]We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations whose righthand sides are polynomials in the state variables. In order to verify nontrivial systems without solving their differential equations and without numerical errors, we use a continuous generalization of induction, for which our algorithm computes the required differential invariants. As a means for combining local differential invariants into global system invariants in a sound way, our fixedpoint algorithm works with a compositional verification logic for hybrid systems. With this compositional approach we exploit locality in system designs. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively with differential invariants until safety becomes provable. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification procedure. We verify roundabout maneuvers in air traffic management and collision avoidance in train control and car control.
Keywords: verification of hybrid systems • differential invariants • verification logic • fixedpoint engine

André Platzer.
Differentialalgebraic dynamic logic for differentialalgebraic programs.
Journal of Logic and Computation 20(1), pp. 309352, 2010.
Special issue for selected papers from TABLEAUX'07. © The author
[bib  ✂  pdf  doi  eprint  study  errata  TABLEAUX'07]We generalise dynamic logic to a logic for differentialalgebraic programs, i.e., discrete programs augmented with firstorder differentialalgebraic formulas as continuous evolution constraints in addition to firstorder discrete jump formulas. These programs characterise interacting discrete and continuous dynamics of hybrid systems elegantly and uniformly. For our logic, we introduce a calculus over real arithmetic with discrete induction and a new
differential induction with which differentialalgebraic programs can be verified by exploiting their differential constraints algebraically without having to solve them. We develop the theory of differential induction and differential refinement and analyse their deductive power. As a case study, we present parametric tangential roundabout maneuvers in air traffic control and prove collision avoidance in our calculus.Keywords: dynamic logic • differential constraints • sequent calculus • verification of hybrid systems • differential induction • theorem proving

André Platzer.
Differential dynamic logic for hybrid systems.
Journal of Automated Reasoning 41(2), pp. 143189, 2008. © The author
[bib  ✂  pdf  doi  mypdf  study]Hybrid systems are models for complex physical systems and are defined as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. With the goal of developing a theoretical and practical foundation for deductive verification of hybrid systems, we introduce a dynamic logic for hybrid programs, which is a program notation for hybrid systems. As a verification technique that is suitable for automation, we introduce a free variable proof calculus with a novel combination of realvalued free variables and Skolemisation for lifting quantifier elimination for real arithmetic to dynamic logic. The calculus is compositional, i.e., it reduces properties of hybrid programs to properties of their parts. Our main result proves that this calculus axiomatises the transition behaviour of hybrid systems completely relative to differential equations. In a case study with cooperating traffic agents of the European Train Control System, we further show that our calculus is wellsuited for verifying realistic hybrid systems with parametric system dynamics.
Keywords: dynamic logic • differential equations • sequent calculus • axiomatisation • automated theorem proving • verification of hybrid systems
Conference Publications

Jonathan Laurent and André Platzer.
Learning to find proofs and theorems by learning to refine search strategies.
In Alekh Agarwal, Danielle Belgrave, Kyunghyun Cho and Alice Oh, editors, Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022.
[bib  ✂  pdf  arXiv]We propose a new approach to automated theorem proving and deductive program synthesis where an AlphaZerostyle agent is selftraining to refine a highlevel expert strategy expressed as a nondeterministic program. An analogous teacher agent is selftraining to generate tasks of suitable relevance and difficulty for the learner. This allows leveraging minimal amounts of domain knowledge to tackle problems for which training data is unavailable or hard to synthesize. We illustrate our approach on the problem of loop invariant synthesis for imperative programs and using neural networks to refine both the teacher and solver strategies.
Keywords: Theorem proving • Program synthesis • AlphaZero • Reinforcement learning

Yong Kiam Tan, Stefan Mitsch and André Platzer.
Verifying switched system stability with logic.
In Ezio Bartocci and Sylvie Putot, editors, Hybrid Systems: Computation and Control (part of CPS Week 2022), HSCC'22. Article No. 2, pp. 111. ACM, 2022.
This paper was awarded the HSCC Best Paper Award and HSCC Best Repeatability Evaluation Award. © The authors
[bib  ✂  pdf  doi  slides  video  kyx  arXiv  artifact]Switched systems are known to exhibit subtle (in)stability behaviors requiring system designers to carefully analyze the stability of closedloop systems that arise from their proposed switching control laws. This paper presents a formal approach for verifying switched system stability that blends classical ideas from the controls and verification literature using differential dynamic logic (dL), a logic for deductive verification of hybrid systems. From controls, we use standard stability notions for various classes of switching mechanisms and their corresponding Lyapunov functionbased analysis techniques. From verification, we use dL's ability to verify quantified properties of hybrid systems and dL models of switched systems as looping hybrid programs whose stability can be formally specified and proven by finding appropriate loop invariants, i.e., properties that are preserved across each loop iteration. This blend of ideas enables a trustworthy implementation of switched system stability verification in the KeYmaera X prover based on dL. For standard classes of switching mechanisms, the implementation provides fully automated stability proofs, including searching for suitable Lyapunov functions. Moreover, the generality of the deductive approach also enables verification of switching control laws that require nonstandard stability arguments through the design of loop invariants that suitably express specific intuitions behind those control laws. This flexibility is demonstrated on three case studies: a model for longitudinal flight control by Branicky, an automatic cruise controller, and Brockett's nonholonomic integrator.
Keywords: Switched system stability • Loop invariants • Differential dynamic logic

Matias Scharager, Katherine Cordwell, Stefan Mitsch and André Platzer.
Verified quadratic virtual substitution for real arithmetic.
In Marieke Huisman, Corina Pasareanu, and Naijun Zhan, editors, FM 2021: Formal Methods, volume 13047 of LNCS, pp. 200217. Springer, 2021. © Springer
[bib  ✂  pdf  doi  Isabelle  arXiv]This paper presents a formally verified quantifier elimination (QE) algorithm for firstorder real arithmetic by linear and quadratic virtual substitution (VS) in Isabelle/HOL. The TarskiSeidenberg theorem established that the firstorder logic of real arithmetic is decidable by QE. However, in practice, QE algorithms are highly complicated and often combine multiple methods for performance. VS is a practically successful method for QE that targets formulas with lowdegree polynomials. To our knowledge, this is the first work to formalize VS for quadratic real arithmetic including inequalities. The proofs necessitate various contributions to the existing multivariate polynomial libraries in Isabelle/HOL. Our framework is modularized and easily expandable (to facilitate integrating future optimizations), and could serve as a basis for developing practical generalpurpose QE algorithms. Further, as our formalization is designed with practicality in mind, we export our development to SML and test the resulting code on 378 benchmarks from the literature, comparing to Redlog, Z3, Wolfram Engine, and SMTRAT. This identified inconsistencies in some tools, underscoring the significance of a verified approach for the intricacies of real arithmetic.
Keywords: Virtual substitution • Quantifier elimination • Realclosed fields • Theorem proving

Katherine Cordwell, Yong Kiam Tan and André Platzer.
A verified decision procedure for univariate real arithmetic with the BKR algorithm.
In Liron Cohen and Cezary Kaliszyk, editors, 12th International Conference on Interactive Theorem Proving, ITP 2021, June 29July 1, 2021, Rome, Italy, volume 193 of LIPIcs, pp. 14:114:20. Schloss Dagstuhl  LeibnizZentrum für Informatik 2021. © The authors
[bib  ✂  pdf  doi  Isabelle  arXiv]We formalize the univariate fragment of BenOr, Kozen, and Reif's (BKR) decision procedure for firstorder real arithmetic in Isabelle/HOL. BKR's algorithm has good potential for parallelism and was designed to be used in practice. Its key insight is a clever recursive procedure that computes the set of all consistent sign assignments for an input set of univariate polynomials while carefully managing intermediate steps to avoid exponential blowup from naively enumerating all possible sign assignments (this insight is fundamental for both the univariate case and the general case). Our proof combines ideas from BKR and a followup work by Renegar that are wellsuited for formalization. The resulting proof outline allows us to build substantially on Isabelle/HOL's libraries for algebra, analysis, and matrices. Our main extensions to existing libraries are also detailed.
Keywords: Quantifier elimination • Matrix • Theorem proving • Real arithmetic

Yong Kiam Tan and André Platzer.
Switched systems as hybrid programs.
In Raphaël M. Jungers, Necmiye Ozay and Alessandro Abate, editors, 7th IFAC Conference on Analysis and Design of Hybrid Systems ADHS 2021, volume 54(5) of IFACPapersOnline, pp. 247252. 2021. © The authors
[bib  ✂  pdf  doi  kyx  arXiv]Real world systems of interest often feature interactions between discrete and continuous dynamics. Various hybrid system formalisms have been used to model and analyse this combination of dynamics, ranging from mathematical descriptions, e.g., using impulsive differential equations and switching, to automatatheoretic and languagebased approaches. This paper bridges two such formalisms by showing how various classes of switched systems can be modeled using the language of hybrid programs from differenttial dynamic logic (dL). The resulting models enable the formal specification and verification of switched systems using dL and its existing deductive verification tools such as KeYmaera X. Switched systems also provide a natural avenue for the generalization of dL's deductive proof theory for differential equations. The completeness results for switched system invariants proved in this paper enable effective safety verification of those systems in dL.
Keywords: Hybrid and switched systems modeling • Reachability analysis • Verification and abstraction of hybrid systems • Hybrid programs • Differential dynamic logic

Yong Kiam Tan and André Platzer.
Deductive stability proofs for ordinary differential equations.
In Jan Friso Groote and Kim G. Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021, Proceedings, Part II, volume 12652 of LNCS, pp. 181–199. Springer, 2021. © The authors
[bib  ✂  pdf  doi  mypdf  slides  video  kyx  arXiv]Stability is required for real world controlled systems as it ensures that they can tolerate small, real world perturbations around their desired operating states. This paper shows how stability for continuous systems modeled by ordinary differential equations (ODEs) can be formally verified in differential dynamic logic (dL). The key insight is to specify ODE stability by suitably nesting the dynamic modalities of dL with firstorder logic quantifiers. Elucidating the logical structure of stability properties in this way has three key benefits: i) it provides a flexible means of formally specifying various stability properties of interest, ii) it yields rigorous proofs of those stability properties from dL's axioms with dL's ODE safety and liveness proof principles, and iii) it enables formal analysis of the relationships between various stability properties which, in turn, inform proofs of those properties. These benefits are put into practice through an implementation of stability proofs for several examples in KeYmaera X, a hybrid systems theorem prover based on dL.
Keywords: Differential equations • Stability • Differential dynamic logic

Brandon Bohrer and André Platzer.
Refining constructive hybrid games.
In Zena M. Ariola, editor, 5th International Conference on Formal Structures for Computation and Deduction, FSCD 2020, June 29  July 5, Paris, France, Proceedings, volume 167 of LIPIcs, pp. 14:114:19. Schloss Dagstuhl  LeibnizZentrum für Informatik 2020. © The authors
[bib  ✂  pdf  doi  mypdf  slides  arXiv]We extend the constructive differential game logic (CdGL) of hybrid games with a refinement connective that relates two hybrid games. In addition to CdGL's ability to prove the existence of winning strategies for specific postconditions of hybrid games, game refinements relate two games to one another. That makes it possible to prove that any winning strategy for any postcondition of one game carries over to a winning strategy for the other. Since CdGL is constructive, a computable winning strategy can be extracted from a proof that a player wins a game. A folk theorem says that any such winning strategy for a hybrid game gives rise to a corresponding hybrid system satisfying the same property. We make this precise using CdGL's game refinements and prove correct the construction of hybrid systems from winning strategies of hybrid games.
Keywords: Hybrid games • Constructive logic • Refinement • Game logic

Brandon Bohrer and André Platzer.
Constructive hybrid games.
In Nicolas Peltier and Viorica SofronieStokkermans, editors, Automated Reasoning, 10th International Joint Conference, IJCAR 2020, Paris, France, Proceedings, Part I, volume 12166 of LNCS, pp. 454473. Springer 2020. © The authors
[bib  ✂  pdf  doi  mypdf  slides  arXiv]Hybrid games combine discrete, continuous, and adversarial dynamics. Differential game logic (dGL) enables proving (classical) existence of winning strategies. We introduce constructive differential game logic (CdGL) for hybrid games, where proofs that a player can win the game correspond to computable winning strategies. This constitutes the logical foundation for synthesis of correct control and monitoring code for safetycritical cyberphysical systems. Our contributions include novel semantics as well as soundness and consistency.
Keywords: Game logic • Constructive logic • Hybrid games • Dependent types

Brandon Bohrer and André Platzer.
Constructive game logic.
In Peter Müller, editor, Programming Languages and Systems  29th European Symposium on Programming, ESOP 2020, volume 12075 of LNCS, pp. 84111. Springer, 2020. © The authors
[bib  ✂  pdf  doi  mypdf  slides  arXiv]Game Logic is an excellent setting to study proofsaboutprograms via the interpretation of those proofs as programs, because constructive proofs for games correspond to effective winning strategies to follow in response to the opponent’s actions. We thus develop Constructive Game Logic, which extends Parikh’s Game Logic (GL) with constructivity and with firstorder programs à la Pratt’s firstorder dynamic logic (DL). Our major contributions include: 1. a novel realizability semantics capturing the adversarial dynamics of games, 2. a natural deduction calculus and operational semantics describing the computational meaning of strategies via proofterms, and 3. theoretical results including soundness of the proof calculus w.r.t. realizability semantics, progress and preservation of the operational semantics of proofs, and Existential Properties on support of the extraction of computational artifacts from game proofs. Together, these results provide the most general account of a CurryHoward interpretation for any program logic to date, and the first at all for Game Logic.
Keywords: Game logic • Constructive logic • Natural deduction •Proof terms

João G. Martins, André Platzer, and João Leite.
Dynamic doxastic differential dynamic logic for beliefaware cyberphysical systems.
In Serenella Cerrito and Andrei Popescu, editors, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2019, London, September 35, 2019, Proceedings, volume 11714 of LNCS, pp. 428445. Springer, 2019. © Springer Nature Switzerland AG
[bib  ✂  pdf  doi  slides]Cyberphysical systems (CPS), such as airplanes, operate based on sensor and communication data, i.e. on potentially noisy or erroneous beliefs about the world. Realistic CPS models must therefore incorporate the notion of beliefs if they are to provide safety guarantees in practice as well as in theory. To fundamentally address this challenge, this paper introduces a firstprinciples framework for reasoning about CPS models where control decisions are explicitly driven by controller beliefs arrived at through observation and reasoning. We extend the differential dynamic logic dL for CPS dynamics with belief modalities, and a learning operator for belief change. This new dynamic doxastic differential dynamic logic d^{4}L does due justice to the challenges of CPS verification by having 1) real arithmetic for describing the world and beliefs about the world; 2) continuous and discrete world change; 3) discrete belief change by means of the learning operator. We develop a sound sequent calculus for d^{4}L, which enables us to illustrate the applicability of d^{4}L by proving the safety of a simplified belieftriggered controller for an airplane.
Keywords: Differential dynamic logic • Dynamic epistemic logic • Sequent calculus • Hybrid systems • Cyberphysical systems

Andrew Sogokon, Stefan Mitsch, Yong Kiam Tan, Katherine Cordwell and André Platzer.
Pegasus: A framework for sound continuous invariant generation.
In Maurice ter Beek, Annabelle McIver, and José N. Oliviera, editors, FM 2019: Formal Methods  The Next 30 Years, volume 11800 of LNCS, pp. 138157. Springer, 2019. © Springer
FM Best Tool Paper Award.
[bib  ✂  pdf  doi  slides  tool  FMSD]Continuous invariants are an important component in deductive verification of hybrid and continuous systems. Just like discrete invariants are used to reason about correctness in discrete systems without unrolling their loops forever, continuous invariants are used to reason about differential equations without having to solve them. Automatic generation of continuous invariants remains one of the biggest practical challenges to automation of formal proofs of safety in hybrid systems. There are at present many disparate methods available for generating continuous invariants; however, this wealth of diverse techniques presents a number of challenges, with different methods having different strengths and weaknesses. To address some of these challenges, we develop Pegasus: an automatic continuous invariant generator which allows for combinations of various methods, and integrate it with the KeYmaera X theorem prover for hybrid systems. We describe some of the architectural aspects of this integration, comment on its methods and challenges, and present an experimental evaluation on a suite of benchmarks.
Keywords: Invariant generation • Continuous invariants • Ordinary differential equations • Cyberphysical systems • Formal verification

Yong Kiam Tan and André Platzer.
An axiomatic approach to liveness for differential equations.
In Maurice ter Beek, Annabelle McIver, and José N. Oliviera, editors, FM 2019: Formal Methods  The Next 30 Years, volume 11800 of LNCS, pp. 371388. Springer, 2019. © Springer
[bib  ✂  pdf  doi  slides  arXiv  FAC'21]This paper presents an approach for deductive liveness verification for ordinary differential equations (ODEs) with differential dynamic logic. Numerous subtleties prevent the generalization of wellknown discrete liveness verification techniques, such as loop variants, to the continuous setting. For example, ODE solutions rarely exist in closedform, they may blow up in finite time, or their progress towards the goal may converge to zero. Our approach handles these subtleties by successively refining ODE liveness properties using ODE invariance properties which have a wellunderstood deductive proof theory. This approach is widely applicable: we survey several liveness arguments in the literature and derive them as special instances of our axiomatic refinement approach. We also correct several soundness errors in the surveyed arguments, which further highlights the subtlety of ODE liveness reasoning and the utility of our deductive approach. The library of common refinement steps identified through our approach enables both the sound development and justification of new ODE liveness proof rules from our axioms.
Keywords: Differential equations • Liveness • Differential dynamic logic

Brandon Bohrer, Manuel Fernández and André Platzer.
dL_{ɩ} Definite descriptions in differential dynamic logic.
In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE27, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 94110. Springer, 2019. © Springer
[bib  ✂  pdf  doi  slides  TR]We introduce dL_{ɩ}, which extends differential dynamic logic (dL) for hybrid systems with definite descriptions and tuples, thus enabling its theoretical foundations to catch up with its implementation in the theorem prover KeYmaera X. Definite descriptions enable partial, nondifferentiable, and discontinuous terms, which have many examples in applications, such as divisions, nth roots, and absolute values. Tuples enable systems of multiple differential equations, arising in almost every application. Together, definite description and tuples combine to support longdesired features such as vector arithmetic.
We overcome the unique challenges posed by extending dL with these features. Unlike in dL, definite descriptions enable nonlocallyLipschitz terms, so our differential equation (ODE) axioms now make their continuity requirements explicit. Tuples are simple when considered in isolation, but in the context of hybrid systems they demand that differentials are treated in full generality. The addition of definite descriptions also makes dL_{ɩ} a free logic; we investigate the interaction of free logic and the ODEs of dL, showing that this combination is sound, and characterize its expressivity. We give an example system that can be defined and verified using these extensions.
Keywords: Dynamic logic • Definite description • Hybrid systems • Theorem proving • Uniform substitution • Partial functions

Katherine Cordwell and André Platzer.
Towards physical hybrid systems.
In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE27, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 216232. Springer, 2019. © Springer
[bib  ✂  pdf  doi  slides  arXiv]Some hybrid systems models are unsafe for mathematically correct but physically unrealistic reasons. For example, mathematical models can classify a system as being unsafe on a set that is too small to have physical importance. In particular, differences in measure zero sets in models of cyberphysical systems (CPS) have significant mathematical impact on the mathematical safety of these models even though differences on measure zero sets have no tangible physical effect in a real system. We develop the concept of "physical hybrid systems" (PHS) to help reunite mathematical models with physical reality. We modify a hybrid systems logic (differential temporal dynamic logic) by adding a firstclass operator to elide distinctions on measure zero sets of time within CPS models. This approach facilitates modeling since it admits the verification of a wider class of models, including some physically realistic models that would otherwise be classified as mathematically unsafe. We also develop a proof calculus to help with the verification of PHS.
Keywords: Hybrid systems • Almost everywhere • Differential temporal dynamic logic • Proof calculus

André Platzer.
Uniform substitution at one fell swoop.
In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE27, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 425441. Springer, 2019. © The author
[bib  ✂  pdf  doi  mypdf  slides  Isabelle  arXiv]Uniform substitution of function, predicate, program or game symbols is the core operation in parsimonious provers for hybrid systems and hybrid games. By postponing soundnesscritical admissibility checks, this paper introduces a uniform substitution mechanism that proceeds in a linear pass homomorphically along the formula. Soundness is recovered using a simple variable condition at the replacements performed by the substitution. The setting in this paper is that of differential hybrid games, in which discrete, continuous, and adversarial dynamics interact in differential game logic dGL. This paper proves soundness and completeness of onepass uniform substitutions for dGL.
Keywords: Uniform substitution • Differential game logic • Hybrid games

Nathan Fulton and André Platzer.
Verifiably safe offmodel 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. 413430. Springer, 2019. © The authors
[bib  ✂  pdf  doi  arXiv]The desire to use reinforcement learning in safetycritical settings has inspired a recent interest in formal methods for learning algorithms. Existing formal methods for learning and optimization primarily consider the problem of constrained learning or constrained optimization. Given a single correct model and associated safety constraint, these approaches guarantee efficient learning while provably avoiding behaviors outside the safety constraint. Acting well given an accurate environmental model is an important prerequisite for safe learning, but is ultimately insufficient for systems that operate in complex heterogeneous environments. This paper introduces verificationpreserving model updates, the first approach toward obtaining formal safety guarantees for reinforcement learning in settings where multiple possible environmental models must be taken into account. Through a combination of inductive data and deductive proving with designtime model updates and runtime model falsification, we provide a first approach toward obtaining formal safety proofs for autonomous systems acting in heterogeneous environments.
Keywords: Safe AI • Cyberphysical systems • Reinforcement learning • Hybrid systems • Theorem proving

Luis Garcia, Stefan Mitsch and André Platzer.
HyPLC: Hybrid programmable logic controller program translation for verification.
In Linda Bushnell and Miroslav Pajic, editor, 10th ACM/IEEE International Conference on CyberPhysical Systems ICCPS, pp. 4756. 2019. © ACM
Best paper finalist
[bib  ✂  pdf  doi  tool  arXiv]Programmable Logic Controllers (PLCs) provide a prominent choice of implementation platform for safetycritical industrial control systems. Formal verification provides ways of establishing correctness guarantees, which can be quite important for such safetycritical applications. But since PLC code does not include an analytic model of the system plant, their verification is limited to discrete properties. In this paper, we, thus, start the other way around with hybrid programs that include continuous plant models in addition to discrete control algorithms. Correctness properties of hybrid programs can be formally verified in the theorem prover KeYmaera X that implements differential dynamic logic, dL, for hybrid programs. After verifying the hybrid program, we now present an approach for translating hybrid programs into PLC code. The new HyPLC tool implements this translation of discrete control code of verified hybrid program models to PLC controller code and, vice versa, the translation of existing PLC code into the discrete control actions for a hybrid program given an additional input of the continuous dynamics of the system to be verified. This approach allows for the generation of real controller code while preserving, by compilation, the correctness of a valid and verified hybrid program. PLCs are common cyberphysical interfaces for safetycritical industrial control applications, and HyPLC serves as a pragmatic tool for bridging formal verification of complex cyberphysical systems at the algorithmic level of hybrid programs with the execution layer of concrete PLC implementations.
Keywords: Industrial control • Programming languages • Formal verification • Semantics • Compilation

Brandon Bohrer, Adriel Luo, Xue An Chuang and André Platzer.
CoasterX: A case study in componentdriven hybrid systems proof automation.
In Maurice Heemels and Antoine Girard, editors, 6th IFAC Conference on Analysis and Design of Hybrid Systems ADHS 2018, volume 51(6) of IFACPapersOnline, pp. 5560, 2018. © IFAC
[bib  ✂  pdf  doi  slides]Componentdriven proof automation (CDPA) exploits component structure to automate deductive verification of largescale hybrid systems with nontrivial continuous dynamics. We use CDPA to implement a case study CoasterX, which is a toolchain for designing and verifying safety of 2dimensional roller coaster track designs. Specifically, we verify velocity and acceleration bounds. CoasterX starts with a graphical frontend for pointandclick design of tracks. The CoasterX backend then automatically specifies and verifies the track in differential dynamic logic (dL) with a custom procedure built in the KeYmaera X theorem prover. We show that the CDPA approach scales, testing real coasters of up to 56 components.
Keywords: Roller coasters • Hybrid programs • Componentdriven verification

Andrew Sogokon, Khalil Ghorbal, Yong Kiam Tan and André Platzer.
Vector barrier certificates and comparison systems.
In Klaus Havelund. Bill Roscoe and Jan Peleska, editors, FM 2018: Formal Methods  22nd International Symposium, Oxford, UK, July 1517, 2018, Proceedings, volume 10951 of LNCS, pp. 418437. Springer, 2018. © Springer
[bib  ✂  pdf  doi  slides]Vector Lyapunov functions are a multidimensional extension of the more familiar (scalar) Lyapunov functions, commonly used to prove stability properties in systems described by nonlinear ordinary differential equations (ODEs). This paper explores an analogous vector extension for socalled barrier certificates used in safety verification. As with vector Lyapunov functions, the approach hinges on constructing appropriate comparison systems, i.e., related differential equation systems from which properties of the original system may be inferred. The paper presents an accessible development of the approach, demonstrates that most previous notions of barrier certificate are special cases of comparison systems, and discusses the potential applications of vector barrier certificates in safety verification and invariant synthesis.
Keywords: Ordinary differential equations • Safety verification • Vector barrier certificates • Comparison systems

Brandon Bohrer and André Platzer.
A hybrid, dynamic logic for hybriddynamic 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. 115124. ACM 2018. © The authors. Publication rights licensed to ACM
[bib  ✂  pdf  doi  slides  TR]Informationflow security is important to the safety and privacy of cyberphysical systems (CPSs) across many domains: information leakage can both violate user privacy and provide information that supports further attacks. CPSs face the challenge that information can flow both in discrete cyber channels and in continuous realvalued physical channels ranging from time to physical flow of resources. We call these hybrid information flows and introduce dHL, the first logic for verifying these flows in hybriddynamical models of CPSs. We achieve verification of hybrid information flows by extending differential dynamic logic (dL) for hybriddynamical systems with hybridlogical features for explicit representation and relation of program states. By verifying hybrid information flows, we ensure security even under a strong attacker model wherein an attacker can observe time and physical values continuously. We present a Hilbertstyle proof calculus for dHL, prove it sound, and compare the expressive power of dHL with dL. We demonstrate dHL's abilities by developing a hybrid system model of the smart electrical grid FREEDM. We verify that the naive model has a previouslyunknown information flow vulnerability and verify that a revised model resolves the vulnerability. To the best of our knowledge, this is both the first information flow proof for hybrid information flows and the first for a hybriddynamical model. We discuss applications of hybrid information flow to a range of critical systems.
Keywords: Dynamic logic • Hybrid logic • Hybrid systems • Information flow • Cyberphysical systems • Formal verification • Smart grid

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. 819828. ACM 2018. © The authors
[bib  ✂  pdf  doi  mypdf  slides  video  arXiv  JACM'20]We prove the completeness of an axiomatization for differential equation invariants. First, we show that the differential equation axioms in differential dynamic logic are complete for all algebraic invariants. Our proof exploits differential ghosts, which introduce additional variables that can be chosen to evolve freely along new differential equations. Cleverly chosen differential ghosts are the prooftheoretical counterpart of dark matter. They create new hypothetical state, whose relationship to the original state variables satisfies invariants that did not exist before. The reflection of these new invariants in the original system enables its analysis.
We then show that extending the axiomatization with existence and uniqueness axioms makes it complete for all local progress properties, and further extension with a real induction axiom makes it complete for all real arithmetic invariants. This yields a parsimonious axiomatization, which serves as the logical foundation for reasoning about invariants of differential equations. Moreover, our results are purely axiomatic, and so the axiomatization is suitable for sound implementation in foundational theorem provers.
Keywords: Differential equation axiomatization • Differential dynamic logic • Differential ghosts

André Platzer.
Uniform substitution for differential game logic.
In Didier Galmiche, Stephan Schulz and Roberto Sebastiani, editors, Automated Reasoning, 9th International Joint Conference, IJCAR 2018, Oxford, UK, Proceedings, volume 10900 of LNCS, pp. 211227. Springer 2018. © Springer
[bib  ✂  pdf  doi  slides  arXiv]This paper presents a uniform substitution calculus for differential game logic (dGL). Church's uniform substitutions substitute a term or formula for a function or predicate symbol everywhere. After generalizing them to differential game logic and allowing for the substitution of hybrid games for game symbols, uniform substitutions make it possible to only use axioms instead of axiom schemata, thereby substantially simplifying implementations. Instead of subtle schema variables and soundnesscritical side conditions on the occurrence patterns of logical variables to restrict infinitely many axiom schema instances to sound ones, the resulting axiomatization adopts only a finite number of ordinary dGL formulas as axioms, which uniform substitutions instantiate soundly. This paper proves the soundness of uniform substitutions for the monotone modal logic dGL. The resulting axiomatization admits a straightforward modular implementation of dGL in theorem provers.
Keywords: Differential game logic • Uniform substitution • Axioms • Static semantics

Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen and André Platzer.
VeriPhy: Verified controller executables from verified cyberphysical system models.
In Dan Grossmann, editor, Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pp. 617630. ACM 2018. © The authors
[bib  ✂  pdf  doi  mypdf  slides  video  tool]We present VeriPhy, a verified pipeline which automatically transforms verified highlevel models of safetycritical cyberphysical systems (CPSs) in differential dynamic logic (dL) to verified controller executables. VeriPhy proves that all safety results are preserved endtoend as it bridges abstraction gaps, including: i) the gap between mathematical reals in physical models and machine arithmetic in the implementation ii) the gap between real physics and its differentialequation models iii) and the gap between nondeterministic controller models and machine code. VeriPhy reduces CPS safety to the faithfulness of the physical environment, which is checked at runtime by synthesized, verified monitors. We use three provers in this effort: KeYmaera X, HOL4, and Isabelle/HOL. To minimize the trusted base, we crossverify KeYmaera X in Isabelle/HOL. We evaluate the resulting controller and monitors on commodity robotics hardware.
Keywords: Cyberphysical systems • Hybrid systems • Formal verification • Verified compilation • Verified executables

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. 64856492. AAAI 2018. © AAAI Press
[bib  ✂  pdf  eprint  slides]Formal verification provides a high degree of confidence in safe system operation, but only if reality matches the verified model. Although a good model will be accurate most of the time, even the best models are incomplete. This is especially true in CyberPhysical Systems because highfidelity physical models of systems are expensive to develop and often intractable to verify. Conversely, reinforcement learningbased controllers are lauded for their flexibility in unmodeled environments, but do not provide guarantees of safe operation.
This paper presents an approach for provably safe learning that provides the best of both worlds: the exploration and optimization capabilities of learning along with the safety guarantees of formal verification. Our main insight is that formal verification combined with verified runtime monitoring can ensure the safety of a learning agent. Verification results are preserved whenever learning agents limit exploration within the confounds of verified control choices as long as observed reality comports with the model used for offline verification. When a model violation is detected, the agent abandons efficiency and instead attempts to learn a control strategy that guides the agent to a modeled portion of the state space.
We prove that our approach toward incorporating knowledge about safe control into learning systems preserves safety guarantees, and demonstrate that we retain the empirical performance benefits provided by reinforcement learning. We also explore various points in the design space for these justified speculative controllers in a simple model of adaptive cruise control model for autonomous cars.
Keywords: Formal methods • Software verification • Safe reinforcement learning • AI safety • Hybrid systems • Cyberphysical systems

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. 173191. Springer, 2017. © Springer
[bib  ✂  pdf  doi  slides]Train control technology enhances the safety and efficiency of railroad operation by safeguarding the motion of trains to prevent them from leaving designated areas of operation and colliding with other trains. It is crucial for safety that the trains engage their brakes early enough in order to make sure they never leave the safe part of the track. Efficiency considerations, however, also require that the train does not brake too soon, which would limit operational suitability. It is surprisingly subtle to reach the right tradeoffs and identify the right control conditions that guarantee safe motion without being overly conservative.
In pursuit of an answer, we develop a hybrid system model with discrete control decisions for acceleration, brakes, and with continuous differential equations for their physical effects on the motion of the train. The resulting hybrid system model is systematically derived from the Federal Railway Administration model for flat terrain by conservatively neglecting minor forces.
The main contribution of this paper is the identification of a controller with control constraints that we formally verify to always guarantee collision freedom in the FRA model. The safe braking behavior of a train is influenced not only by the train configuration (e.g., train length and mass), but also by physical characteristics (e.g., brake pressure propagation and reaction time). We formalize train control safety properties in differential dynamic logic and prove the correctness of the train control models in the theorem prover KeYmaera X.
Keywords: Train control safety • Braking model verification • Performance analysis • Hybrid systems • Differential dynamic logic

Nathan Fulton, Stefan Mitsch, Brandon Bohrer and André Platzer.
Bellerophon: Tactical theorem proving for hybrid systems.
In Mauricio AyalaRincón and César A. Muñoz, editors, Interactive Theorem Proving, International Conference, ITP 2017, volume 10499 of LNCS, pp. 207224. Springer, 2017. © Springer
[bib  ✂  pdf  doi  slides  kyx]Hybrid systems combine discrete and continuous dynamics, which makes them attractive as models for systems that combine computer control with physical motion. Verification is undecidable for hybrid systems and challenging for many models and properties of practical interest. Thus, human interaction and insight are essential for verification. Interactive theorem provers seek to increase user productivity by allowing them to focus on those insights. We present a tactics language and library for hybrid systems verification, named Bellerophon, that provides a way to convey insights by programming hybrid systems proofs.
We demonstrate that in focusing on the important domain of hybrid systems verification, Bellerophon emerges with unique automation that provides a productive proving experience for hybrid systems from a small foundational prover core in the KeYmaera X prover. Among the automation that emerges are tactics for decomposing hybrid systems, discovering and establishing invariants of nonlinear continuous systems, arithmetic simplifications to maximize the benefit of automated solvers and generalpurpose heuristic proof search. Our presentation begins with syntax and semantics for the Bellerophon tactic combinator language, culminating in an example verification effort exploiting Bellerophon's support for invariant and arithmetic reasoning for a nonsolvable system.
Keywords: Hybrid systems • Tactical theorem proving • Differential dynamic logic

Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger and André Platzer.
Change and delay contracts for hybrid system component verification.
In Marieke Huisman and Julia Rubin, editors, Fundamental Approaches to Software Engineering. FASE 2017, volume 10202 of LNCS, pp. 134151. Springer, 2017. © Springer
[bib  ✂  pdf  doi  slides  study  STTT'18]In this paper, we present reasoning techniques for a componentbased modeling and verification approach for hybrid systems comprising discrete dynamics as well as continuous dynamics, in which the components have local responsibilities. Our approach supports component contracts (i.e., input assumptions and output guarantees of interfaces) that are more general than previous componentbased hybrid systems verification techniques in the following ways: We introduce change contracts, which characterize how current values exchanged between components along ports relate to previous values. We also introduce delay contracts, which describe the change relative to the time that has passed since the last value was exchanged. Together, these contracts can take into account what has changed between two components in a given amount of time since the last exchange of information. Most crucially, we prove that the safety of compatible components implies safety of the composite. The proof steps of the theorem are also implemented as a tactic in KeYmaera X, allowing automatic generation of a KeYmaera X proof for the composite system from proofs of the concrete components.
Keywords: componentbased development • hybrid systems • formal verification

Brandon Bohrer, Vincent Rahli, Ivana Vukotic, Marcus Völp, and André Platzer.
Formally verified differential dynamic logic.
Certified Programs and Proofs  6th ACM SIGPLAN Conference, CPP 2017, Paris, France, January 1617, 2017, pp. 208221, ACM, 2017. © ACM
[bib  ✂  pdf  doi  slides  Isabelle  Coq]We formalize the soundness theorem for differential dynamic logic, a logic for verifying hybrid systems. To increase confidence in the formalization, we present two versions: one in Isabelle/HOL and one in Coq. We extend the metatheory to include features used in practice, such as systems of differential equations and functions of multiple arguments. We demonstrate the viability of constructing a verified kernel for the hybrid systems theorem prover KeYmaera X by embedding proof checkers for differential dynamic logic in Coq and Isabelle. We discuss how different provers and libraries influence the design of the formalization.
Keywords: differential dynamic logic • hybridsystem verification • KeYmaera X • formalization

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. 505514. ACM, 2016. © The authors
[bib  ✂  pdf  doi  mypdf  slides]We introduce differential refinement logic (dRL), a logic with firstclass support for refinement relations on hybrid systems, and a proof calculus for verifying such relations. dRL simultaneously solves several seemingly different challenges common in theorem proving for hybrid systems: 1. When hybrid systems are complicated, it is useful to prove properties about simpler and related subsystems before tackling the system as a whole. 2. Some models of hybrid systems can be implementationspecific. Verification can be aided by abstracting the system down to the core components necessary for safety, but only if the relations between the abstraction and the original system can be guaranteed. 3. One approach to taming the complexities of hybrid systems is to start with a simplified version of the system and iteratively expand it. However, this approach can be costly, since every iteration has to be proved safe from scratch, unless refinement relations can be leveraged in the proof. 4. When proofs become large, it is difficult to maintain a modular or comprehensible proof structure. By using a refinement relation to arrange proofs hierarchically according to the structure of natural subsystems, we can increase the readability and modularity of the resulting proof. dRL extends an existing specification and verification language for hybrid systems (differential dynamic logic, dL) by adding a refinement relation to directly compare hybrid systems. This paper gives a syntax, semantics, and proof calculus for dRL. We demonstrate its usefulness with examples where using refinement results in easier and betterstructured proofs.
Keywords: differential dynamic logic • hybrid systems •cyberphysical systems •theorem proving • refinement

Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger and André Platzer.
A componentbased approach to hybrid systems safety verification.
In Erika Abraham and Marieke Huisman, editors, Integrated Formal Methods  12th International Conference, iFM 2016, Reykjavik, Iceland, June 14, 2016, Proceedings, volume 9681 of LNCS, pp. 441456. Springer, 2016. © Springer
[bib  ✂  pdf  doi  slides  TR]We study a componentbased approach to simplify the challenges of verifying largescale hybrid systems. Componentbased modeling can be used to split large models into partial models to reduce modeling complexity. Yet, verification results also need to transfer from components to composites. In this paper, we propose a componentbased hybrid system verification approach that combines the advantages of componentbased modeling (e.g., reduced model complexity) with the advantages of formal verification (e.g., guaranteed contract compliance). Our strategy is to decompose the system into components, verify their local safety individually and compose them to form an overall system that provably satisfies a global contract, without proving the whole system. We introduce the necessary formalism to define the structure and behavior of components and a technique how to compose components such that safety properties provably emerge from component safety.
Keywords: Componentbased development • Hybrid systems • Formal verification

Nathan Fulton and André Platzer.
A logic of proofs for differential dynamic logic:
Toward independently checkable proof certificates for dynamic logics.
In Jeremy Avigad and Adam Chlipala, editors, Proceedings of the 2016 Conference on Certified Programs and Proofs, CPP 2016, St. Petersburg, FL, USA, January 1819, 2016, pp. 110121. ACM, 2016. © ACM
[bib  ✂  pdf  doi  slides]Differential dynamic logic is a logic for specifying and verifying safety, liveness, and other properties about models of cyberphysical systems. Theorem provers based on differential dynamic logic have been used to verify safety properties for models of selfdriving cars and collision avoidance protocols for aircraft. Unfortunately, these theorem provers do not have explicit proof terms, which makes the implementation of a number of important features unnecessarily complicated without soundnesscritical and extralogical extensions to the theorem prover. Examples include: an unambiguous separation between proof checking and proof search, the ability to extract program traces corresponding to counterexamples, and synthesis of surelylive deterministic programs from liveness proofs for nondeterministic programs.
This paper presents a differential dynamic logic with such an explicit representation of proofs. The resulting logic extends both the syntax and semantics of differential dynamic logic with proof terms  syntactic representations of logical deductions. To support axiomatic theorem proving, the logic allows equivalence rewriting deep within formulas and supports both uniform renaming and uniform substitutions.
Keywords: cyberphysical systems • differential dynamic logic • hybrid systems • proof terms

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. © Springer
[bib  ✂  pdf  doi  slides]This paper presents a method for generating semialgebraic invariants for systems governed by nonlinear polynomial ordinary differential equations under semialgebraic evolution constraints. Based on the notion of discrete abstraction, our method eliminates unsoundness and unnecessary coarseness found in existing approaches for computing abstractions for nonlinear continuous systems and is able to construct invariants with intricate boolean structure, in contrast to invariants typically generated using templatebased methods. In order to tackle the state explosion problem associated with discrete abstraction, we present invariant generation algorithms that exploit sound proof rules for safety verification, such as differential cut (DC), and a new proof rule that we call differential divideandconquer (DDC), which splits the verification problem into smaller subproblems. The resulting invariant generation method is observed to be much more scalable and efficient than the naïve approach, exhibiting orders of magnitude performance improvement on many of the problems.
Keywords: Continuous systems • Differential equations • Invariant generation • Formal safety verification • Hybrid systems

Andreas Müller and Stefan Mitsch and André Platzer.
Verified traffic networks: Componentbased verification of cyberphysical flow systems.
In Intelligent Transportation Systems (ITSC), 2015 IEEE 18th International Conference on, pp. 757764, 2015. © IEEE
[bib  ✂  pdf  doi  slides]We address the problem how highfidelity verification results about the hybrid systems dynamics of cyberphysical flow systems can be provided at the scale of large (traffic) networks without prohibitive analytic cost. We propose the use of contracts for traffic flow components concisely capturing the conditions for a safe operation in the context of a traffic network. This reduces the analysis of flows in the full traffic network to simple arithmetic checks of the local compatibility of the traffic component contracts, while retaining higherfidelity correctness guarantees of the global hybrid systems models that inherits from correct contracts of the hybrid system components. We evaluate our approach in a case study of a modular traffic network and a prototypical implementation in a modelbased analysis and design tool for traffic flow networks.
Keywords: Automobiles • Contracts • Load modeling •Mathematical model • Roads • Safety

Nikos Aréchiga, James Kapinski, Jyotirmoy V. Deshmukh, André Platzer, and Bruce Krogh.
Forward invariant cuts to simplify proofs of safety.
In Alain Girault and Nan Guan, editors, International Conference on Embedded Software, EMSOFT'15, Amsterdam, The Netherlands, Proceedings, pp. 227236. IEEE, 2015. © IEEE
[bib  ✂  pdf  doi  arXiv]The use of deductive techniques, such as theorem provers, has several advantages in safety verification of hybrid systems; however, stateoftheart theorem provers require manual intervention to handle complex systems. Furthermore, there is often a gap between the type of assistance that a theorem prover requires to make progress on a proof task and the assistance that a system designer is able to provide directly. This paper presents an extension to KeYmaera, a deductive verification tool for differential dynamic logic; the new technique allows local reasoning using system designer intuition about performance within particular modes as part of a proof task. Our approach allows the theorem prover to leverage forward invariants, discovered using numerical techniques, as part of a proof of safety. We introduce a new inference rule into the proof calculus of KeYmaera, the forward invariant cut rule, and we present a methodology to discover useful forward invariants, which are then used with the new cut rule to complete verification tasks. We demonstrate how our new approach can be used to complete verification tasks that lie out of the reach of existing automatic verification approaches using several examples, including one involving an automotive powertrain control system.

André Platzer.
A uniform substitution calculus for differential dynamic logic.
In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE25, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 467481. Springer, 2015. © Springer
[bib  ✂  pdf  doi  slides  arXiv  JAR'17]This paper introduces a new proof calculus for differential dynamic logic (dL) that is entirely based on uniform substitution, a proof rule that substitutes a formula for a predicate symbol everywhere. Uniform substitutions make it possible to rely on axioms rather than axiom schemata, substantially simplifying implementations. Instead of subtle schema variables and soundnesscritical side conditions on the occurrence patterns of variables, the resulting calculus adopts only a finite number of ordinary dL formulas as axioms. The static semantics of differential dynamic logic is captured exclusively in uniform substitutions and bound variable renamings as opposed to being spread in delicate ways across the prover implementation. In addition to sound uniform substitutions, this paper introduces a differential form of differential dynamic logic that makes it possible to internalize differential invariants, differential substitutions, and derivations as firstclass citizens in the logic.
Keywords: differential dynamic logic • uniform substitution • axioms • differentials • static semantics

JeanBaptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki, and André Platzer.
A formally verified hybrid system for the nextgeneration airborne collision avoidance system.
In Christel Baier and Cesare Tinelli, editors, Tools and Algorithms for the Construction and Analysis of Systems  21st International Conference, TACAS 2015, London, UK, April 1118, 2015, Proceedings, volume 9035 of LNCS, pp. 2136. Springer, 2015. © Springer
[bib  ✂  pdf  doi  study  TR  STTT'17]The nextgeneration Airborne Collision Avoidance System (ACAS X) is intended to be installed on all large aircraft to give advice to pilots and prevent midair collisions with other aircraft. It is currently being developed by the Federal Aviation Administration (FAA). In this paper we determine the geometric configurations under which the advice given by ACAS X is safe under a precise set of assumptions and formally verify these configurations using hybrid systems theorem proving techniques. We conduct an initial examination of the current version of the real ACAS X system and discuss some cases where our safety theorem conflicts with the actual advisory given by that version, demonstrating how formal, hybrid approaches are helping ensure the safety of ACAS X. Our approach is general and could also be used to identify unsafe advice issued by other collision avoidance systems or confirm their safety.
Keywords: Airborne Collision Avoidance • ACAS X • Hybrid systems • Theorem proving • Federal Aviation Administration • Aircraft • Markov decision processes • Cyberphysical systems

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. © Springer
[bib  ✂  pdf  doi  slides  study  ComLan'17]This paper presents a theoretical and experimental comparison of sound proof rules for proving invariance of algebraic sets, that is, sets satisfying polynomial equalities, under the flow of polynomial ordinary differential equations. Problems of this nature arise in formal verification of continuous and hybrid dynamical systems, where there is an increasing need for methods to expedite formal proofs. We study the tradeoff between proof rule generality and practical performance and evaluate our theoretical observations on a set of heterogeneous benchmarks. The relationship between increased deductive power and running time performance of the proof rules is far from obvious; we discuss and illustrate certain classes of problems where this relationship is interesting.
Keywords: Inductive invariants • Theorem proving • Deductive power of proof rules • Dynamical and hybrid systems

Stefan Mitsch and André Platzer.
ModelPlex: Verified runtime validation of verified cyberphysical system models.
In Borzoo Bonakdarpour and Scott A. Smolka, editors, Runtime Verification  5th International Conference, RV 2014, Toronto, ON, Canada, September 2225, 2014. Proceedings, volume 8734 of LNCS, pp. 199214. Springer, 2014. © Springer
Best paper finalist
[bib  ✂  pdf  doi  slides  study  TR  FMSD'16]Formal verification and validation play a crucial role in making cyberphysical systems (CPS) safe. Formal methods make strong guarantees about the system behavior if accurate models of the system can be obtained, including models of the controller and of the physical dynamics. In CPS, models are essential; but any model we could possibly build necessarily deviates from the real world. If the real system fits to the model, its behavior is guaranteed to satisfy the correctness properties verified w.r.t. the model. Otherwise, all bets are off. This paper introduces ModelPlex, a method ensuring that verification results about models apply to CPS implementations. ModelPlex provides correctness guarantees for CPS executions at runtime: it combines offline verification of CPS models with runtime validation of system executions for compliance with the model. ModelPlex ensures that the verification results obtained for the model apply to the actual system runs by monitoring the behavior of the world for compliance with the model, assuming the system dynamics deviation is bounded. If, at some point, the observed behavior no longer complies with the model so that offline verification results no longer apply, ModelPlex initiates provably safe fallback actions. This paper, furthermore, develops a systematic technique to synthesize provably correct monitors automatically from CPS proofs in differential dynamic logic.
Keywords: Runtime verification • Cyberphysical systems • Hybrid systems • Logic

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, SAS 2014, volume 8723 of LNCS, pp. 151167. Springer, 2014. © Springer
[bib  ✂  pdf  doi  slides  study]In this paper we seek to provide greater automation for formal deductive verification tools working with continuous and hybrid dynamical systems. We present an efficient procedure to check invariance of conjunctions of polynomial equalities under the flow of polynomial ordinary differential equations. The procedure is based on a necessary and sufficient condition that characterizes invariant conjunctions of polynomial equalities. We contrast this approach to an alternative one which combines fast and sufficient (but not necessary) conditions using differential cuts for soundly restricting the system evolution domain.
Keywords: Checking algebraic invariance • Algebraic differential equations • Theorem proving • Continuous systems • Hybrid systems verification

JeanBaptiste Jeannin and André Platzer.
dTL^{2}: Differential temporal dynamic logic with nested temporalities for hybrid systems.
In Stéphane Demri, Deepak Kapur and Christoph Weidenbach, editors, Automated Reasoning, 7th International Joint Conference, IJCAR 2014, Vienna, Austria, July 1922, 2014, Proceedings, volume 8562 of LNCS, pp. 292306. Springer, 2014. © Springer
[bib  ✂  pdf  doi  slides]The differential temporal dynamic logic dTL^{2} is a logic to specify temporal properties of hybrid systems. It combines differential dynamic logic with temporal logic to reason about the intermediate states reached by a hybrid system. The logic dTL^{2} supports some linear time temporal properties of LTL. It extends differential temporal dynamic logic dTL with nested temporalities. We provide a semantics and a proof system for the logic dTL^{2}, and show its usefulness for nontrivial temporal properties of hybrid systems. We take particular care to handle the case of alternating universal dynamic and existential temporal modalities and its dual, solving an open problem formulated in previous work.
Keywords: differential temporal dynamic logic • hybrid systems, dynamic logic • temporal logic

Stefan Mitsch, JanDavid Quesel and André Platzer.
Refactoring, refinement, and reasoning:
A logical characterization for hybrid systems.
In Cliff B. Jones, Pekka Pihlajasaari and Jun Sun, editors, 19th International Symposium on Formal Methods, FM, Singapore, Proceedings, volume 8442 of LNCS, pp. 481496. Springer, 2014. © Springer
[bib  ✂  pdf  doi  slides]Refactoring of code is a common device in classical programs. As cyberphysical systems (CPS) become ever more complex, similar engineering practices become more common in CPS development. Proper safe developments of CPS designs are accompanied by a proof of correctness. Since the inherent complexities of CPS practically mandate iterative development, frequent changes of models are standard practice, but require reverification of the resulting models after every change.
To overcome this issue, we develop proofaware refactorings for CPS. That is, we study model transformations on CPS and show how they correspond to relations on correctness proofs. As the main technical device, we show how the impact of model transformations on correctness can be characterized by different notions of refinement in differential dynamic logic. Furthermore, we demonstrate the application of refinements on a series of safetypreserving and liveness preserving refactorings. For some of these we can give strong results by proving on a metalevel that they are correct. Where this is impossible, we construct proof obligations for showing that the refactoring respects the refinement relation.
Keywords: formal verification • hybrid system • modeldriven engineering

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. © Springer
[bib  ✂  pdf  doi  slides  study  TR]We prove that any invariant algebraic set of a given polynomial vector field can be algebraically represented by one polynomial and a finite set of its successive Lie derivatives. This socalled differential radical characterization relies on a sound abstraction of the reachable set of solutions by the smallest variety that contains it. The characterization leads to a differential radical invariant proof rule that is sound and complete, which implies that invariance of algebraic equations over realclosed fields is decidable. Furthermore, the problem of generating invariant varieties is shown to be as hard as minimizing the rank of a symbolic matrix, and is therefore NPhard. We investigate symbolic linear algebra tools based on Gaussian elimination to efficiently automate the generation. The approach can, e.g., generate nontrivial algebraic invariant equations capturing the airplane behavior during takeoff or landing in longitudinal motion.
Keywords: Algebraic invariants • Differential ideals • Higherorder Lie derivation • Differential invariants • Differential equations • Invariant generation

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]We consider an adaptive cruise control system in which control decisions are made based on position and velocity information received from other vehicles via V2V wireless communication. If the vehicles follow each other at a close distance, they have better wireless reception but collisions may occur when a follower car does not receive notice about the decelerations of the leader car fast enough to react before it is too late. If the vehicles are farther apart, they would have a bigger safety margin, but the wireless communication drops out more often, so that the follower car no longer receives what the leader car is doing. In order to guarantee safety, such a system must return control to the driver if it does not receive an update from a nearby vehicle within some timeout period. The value of this timeout parameter encodes a tradeoff between the likelihood that an update is received and the maximum safe acceleration. Combining formal verification techniques for hybrid systems with a wireless communication model, we analyze how the expected efficiency of a provablysafe adaptive cruise control system is affected by the value of this timeout.
Keywords: Traffic theory for ITS • Network modeling • Driver assistance systems • V2V wireless communication • Hybrid systems • Formal verification

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]Nowadays, robots interact more frequently with a dynamic environment outside limited manufacturing sites and in close proximity with humans. Thus, safety of motion and obstacle avoidance are vital safety features of such robots. We formally study two safety properties of avoiding both stationary and moving obstacles: (i) passive safety, which ensures that no collisions can happen while the robot moves, and (ii) the stronger passive friendly safety in which the robot further maintains sufficient maneuvering distance for obstacles to avoid collision as well. We use hybrid system models and formal verification techniques that describe and formally verify the robot's discrete control decisions along with its continuous, physical motion. Moreover, we formally prove that safety can still be guaranteed despite location and actuator uncertainty.
Keywords: autonomous robotics obstacle avoidance • formal verification • hybrid systems • dynamic window approach

Erik P. Zawadzki, André Platzer and Geoffrey J. Gordon.
A generalization of SAT and #SAT for policy evaluation.
In Francesca Rossi, editor, IJCAI 2013, Proceedings of the 23nd International Joint Conference on Artificial Intelligence, Beijing, China, August 39, 2013, pp. 25832589, IJCAI/AAAI, 2013.
[bib  ✂  pdf  eprint  poster  TR]Both SAT and #SAT can represent difficult problems in seemingly dissimilar areas such as planning, verification, and probabilistic inference. Here, we examine an expressive new language, #ESAT, that generalizes both of these languages. #ESAT problems require counting the number of satisfiable formulas in a conciselydescribable set of existentiallyquantified, propositional formulas. We characterize the expressiveness and worstcase difficulty of #ESAT by proving that it is complete for the complexity class #P^{NP[1]}, and relating this class to more familiar complexity classes. We also experiment with three new generalpurpose #ESAT solvers on a battery of problem distributions including a simple logistics domain. Our experiments show that, despite the formidable worstcase complexity of #P^{NP[1]}, many of the instances can be solved efficiently by noticing and exploiting a particular type of frequent structure.
Keywords: exact probabilistic inference • satisfiability • solvers and tools • search in planning and scheduling

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 813, 2013, pp. 263272. ACM, 2013. © ACM
[bib  ✂  pdf  doi  slides  study]We applied quantified differentialdynamic logic (QdL) to analyze a control algorithm designed to provide directional force feedback for a surgical robot. We identified problems with the algorithm, proved that it was in general unsafe, and described exactly what could go wrong. We then applied QdL to guide the development of a new algorithm that provides safe operation along with directional force feedback. Using KeYmaeraD (a tool that mechanizes QdL), we created a machinechecked proof that guarantees the new algorithm is safe for all possible inputs.
Keywords: quantified differential dynamic logic • medical robotics • formal verification

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 813, 2013, pp. 125130. ACM, 2013. © ACM
[bib  ✂  pdf  doi  slides  poster  study  TR]As airspace becomes ever more crowded, air traffic management must reduce both space and time between aircraft to increase throughput, making onboard collision avoidance systems ever more important. These safetycritical systems must be extremely reliable, and as such, many resources are invested into ensuring that the protocols they implement are accurate. Still, it is challenging to guarantee that such a controller works properly under every circumstance. In tough scenarios where a large number of aircraft must execute a collision avoidance maneuver, a human pilot under stress is not necessarily able to understand the complexity of the distributed system and may not take the right course, especially if actions must be taken quickly. We consider a class of distributed collision avoidance controllers designed to work even in environments with arbitrarily many aircraft or UAVs. We prove that the controllers never allow the aircraft to get too close to one another, even when new planes approach an inprogress avoidance maneuver that the new plane may not be aware of. Because these safety guarantees always hold, the aircraft are protected against unexpected emergent behavior which simulation and testing may miss. This is an important step in formally verified, flyable, and distributed air traffic control.
Keywords: formal verification • collision avoidance in aircraft • quantified differential dynamic logic • distributed hybrid systems • distributed aircraft controllers

David Henriques, João G. Martins, Paolo Zuliani, André Platzer and Edmund M. Clarke.
Statistical model checking for Markov decision processes.
In 9th International Conference on Quantitative Evaluation of Systems, QEST 2012, September 1720, London, UK, pp. 8493. IEEE Computer Society, 2012. © IEEE
[bib  ✂  pdf  doi  slides  study]Statistical Model Checking (SMC) is a computationally very efficient verification technique based on selective system sampling. One well identified shortcoming of SMC is that, unlike probabilistic model checking, it cannot be applied to systems featuring nondeterminism, such as Markov Decision Processes (MDP). We address this limitation by developing an algorithm that resolves nondeterminism probabilistically, and then uses multiple rounds of sampling and Reinforcement Learning to provably improve resolutions of nondeterminism with respect to satisfying a Bounded Linear Temporal Logic (BLTL) property. Our algorithm thus reduces an MDP to a fully probabilistic Markov chain on which SMC may be applied to give an approximate solution to the problem of checking the probabilistic BLTL property. We integrate our algorithm in a parallelised modification of the PRISM simulation framework. Extensive validation with both new and PRISM benchmarks demonstrates that the approach scales very well in scenarios where symbolic algorithms fail to do so.
Keywords: statistical model checking • Markov decision processes • reinforcement learning

JanDavid 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. 439453. Springer, 2012. © Springer
[bib  ✂  pdf  doi  slides  study]We propose a new logic, called differential dynamic game logic (dDGL), that adds several game constructs on top of differential dynamic logic (dL) so that it can be used for hybrid games. The logic dDGL is a conservative extension of dL, which we exploit for our implementation of dDGL in the theorem prover KeYmaera. We provide rules for extending the dL sequent proof calculus to handle the dDGL constructs by identifying analogs to operators of dL. We have implemented dDGL in an extension of KeYmaera and verified a case study in which a robot satisfies a joint safety and liveness objective in a factory automation scenario, in which the factory may perform interfering actions independently.
Keywords: differential dynamic logic • hybrid games • sequent calculus • theorem proving • logics for hybrid systems • factory automation

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]Hybrid systems are a fusion of continuous dynamical systems and discrete dynamical systems. They freely combine dynamical features from both worlds. For that reason, it has often been claimed that hybrid systems are more challenging than continuous dynamical systems and than discrete systems. We now show that, prooftheoretically, this is not the case. We present a complete prooftheoretical alignment that interreduces the discrete dynamics and the continuous dynamics of hybrid systems. We give a sound and complete axiomatization of hybrid systems relative to continuous dynamical systems and a sound and complete axiomatization of hybrid systems relative to discrete dynamical systems. Thanks to our axiomatization, proving properties of hybrid systems is exactly the same as proving properties of continuous dynamical systems and again, exactly the same as proving properties of discrete dynamical 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.
Keywords: proof theory • hybrid dynamical systems • differential dynamic logic • axiomatization • completeness

Nikos Aréchiga, Sarah M. Loos, André Platzer and Bruce H. Krogh.
Using theorem provers to guarantee closedloop system properties.
In Dawn Tilbury, editor, American Control Conference, ACC, Montréal, Canada, June 2729. pp. 35733580. 2012. © IEEE
[bib  ✂  pdf  doi]This paper presents a new approach for leveraging the power of theorem provers for formal verification to provide sufficient conditions that can be checked on embedded control designs. Theorem provers are often most efficient when using generic models that abstract away many of the controller details, but with these abstract models very general conditions can be verified under which desirable properties such as safety can be guaranteed for the closedloop system. We propose an approach in which these sufficient conditions are static conditions that can be checked for the specific controller design, without having to include the dynamics of the plant. We demonstrate this approach using the KeYmaera theorem prover for differential dynamic logic for two examples: an intelligent cruise controller and a cooperative intersection collision avoidance system (CICAS) for leftturn assist. In each case, safety of the closedloop system proved using KeYmaera provides static sufficient conditions that are checked for the controller design.

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 CyberPhysical Systems ICCPS, Beijing, China, April 1719. pp. 171180, IEEE. 2012. © IEEE
[bib  ✂  pdf  doi  slides  study]We study how CPS technology can help improve freeway traffic by combining local car GPS positioning, traffic center control decisions, and communication to achieve more tightly coupled feedback control in intelligent speed adaptation. We develop models for an intelligent speed adaptation that respects variable speed limit control and incident management. We identify safe ranges for crucial design parameters in these systems and, using the theorem prover KeYmaera, formally verify safety of the resulting CPS models. Finally, we show how those parameter ranges can be used to decide tradeoffs for practical system implementations even for design parameters that are not modeled formally.
Keywords: freeway traffic control • intelligent speed adaptation • hybrid system

Akshay Rajhans, Ajinkya Bhave, Sarah M. Loos, Bruce H. Krogh, André Platzer and David Garlan.
Using parameters in architectural views to support heterogeneous design and verification.
In 50th IEEE Conference on Decision and Control and European Control Conference CDC. pp. 27052710, IEEE. 2011. © IEEE
[bib  ✂  pdf  doi  TAC'14]Current methods for designing cyberphysical systems lack a unifying framework due to the heterogeneous nature of the constituent models and their respective analysis and verification tools. There is a need for a formal representation of the relationships between the different models. Our approach is to define these relationships at the architectural level, associating with each model a particular view of the overall system base architecture. This architectural framework captures critical structural and semantic information without including all the details of the various modeling formalisms. This paper introduces the use of logical constraints over parameters in the architectural views to represent the conditions under which the specifications verified for each model are true and imply the systemlevel specification. Interdependencies and connections between the constraints in the architectural views are managed in the base architecture using firstorder logic of real arithmetic to ensure consistency and correct reasoning. The approach is illustrated in the context of heterogeneous verification of a leaderfollower vehicle scenario.

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. 11811186. 2011. © IEEE
[bib  ✂  pdf  doi  slides  study]Intelligent vehicle systems have interesting prospects for solving inefficiencies and risks in ground transportation, e.g., by making cars aware of their environment and regulating speed intelligently. If the computer control technology reacts fast enough, intelligent control can be used to increase the density of cars on the streets. The technology may also help prevent crashes at intersections, which cost the US $97 Billion in the year 2000. The crucial prerequisite for intelligent vehicle control, however, is that it must be correct, for it may otherwise do more harm than good. Formal verification techniques provide the best reliability guarantees but have had difficulties in the past with scaling to such complex systems. We report our successes with a logical approach to hybrid systems verification, which can capture discrete control decisions and continuous driving dynamics. We present a model for the interaction of two cars and a traffic light at a two lane intersection and verify with a formal proof that our system always ensures collision freedom and that our controller always prevents cars from running red lights.

João G. Martins, André Platzer and João Leite.
Statistical model checking for distributed probabilistic control hybrid automata with smart grid applications.
In Shengchao Qin and Zongyan Qiu, editors, International Conference on Formal Engineering Methods, ICFEM'11, Durham, UK, Proceedings, volume 6991 of LNCS, pp. 131146. Springer, 2011. © Springer
[bib  ✂  pdf  doi  slides  study]The power industry is currently moving towards a more dynamical, intelligent power grid. This Smart Grid is still in its infancy and a formal evaluation of the expensive technologies and ideas on the table is necessary before committing to a full investment. In this paper, we argue that a good model for the Smart Grid must match its basic properties: it must be hybrid (both evolve over time, and perform control/computation), distributed (multiple concurrently executing entities), and allow for asynchronous communication and stochastic behaviour (to accurately model realworld power consumption). We propose Distributed ProbabilisticControl Hybrid Automata (DPCHA) as a model for this purpose, and extend Bounded LTL to Quantified Bounded LTL in order to adapt and apply existing statistical modelchecking techniques. We provide an implementation of a framework for developing and verifying DPCHAs. Finally, we conduct a case study for Smart Grid communications analysis.
Keywords: Bayesian statistical model checking • distributed hybrid systems • probabilistic hybrid automata • verification of smart grid

David W. Renshaw, Sarah M. Loos and André Platzer.
Distributed theorem proving for distributed hybrid systems.
In Shengchao Qin and Zongyan Qiu, editors, International Conference on Formal Engineering Methods, ICFEM'11, Durham, UK, Proceedings, volume 6991 of LNCS, pp. 356371. Springer, 2011. © Springer
[bib  ✂  pdf  doi  tool  study  errata]Distributed hybrid systems present extraordinarily challenging problems for verification. On top of the notorious difficulties associated with distributed systems, they also exhibit continuous dynamics described by quantified differential equations. All serious proofs rely on decision procedures for real arithmetic, which can be extremely expensive. Quantified Differential Dynamic Logic (QdL) has been identified as a promising approach for getting a handle in this domain. QdL has been proved to be complete relative to quantified differential equations. But important questions remain as to how best to translate this theoretical result into practice: how do we succinctly specify a proof search strategy, and how do we control the computational cost?
We address the problem of automated theorem proving for distributed hybrid systems. We identify a simple mode of use of QdL that cuts down on the enormous number of choices that it otherwise allows during proof search. We have designed a powerful strategy and tactics language for directing proof search. With these techniques, we have implemented a new automated theorem prover called KeYmaera D. To overcome the high computational complexity of distributed hybrid systems verification, KeYmaeraD uses a distributed proving backend. We have experimentally observed that calls to the real arithmetic decision procedure can effectively be made in parallel. In this paper, we demonstrate these findings through an extended case study where we prove absence of collisions in a distributed car control system with a varying number of arbitrarily many cars.
Keywords: Hybrid systems • theorem proving • formal verification • distributed systems

André Platzer.
Stochastic differential dynamic logic for stochastic hybrid programs.
In Nikolaj Bjørner and Viorica SofronieStokkermans, editors, International Conference on Automated Deduction, CADE23, Wroclaw, Poland, Proceedings, volume 6803 of LNCS, pp. 446460. Springer, 2011. © Springer
[bib  ✂  pdf  doi  slides  TR]Logic is a powerful tool for analyzing and verifying systems, including programs, discrete systems, realtime systems, hybrid systems, and distributed systems. Some applications also have a stochastic behavior, however, either because of fundamental properties of nature, uncertain environments, or simplifications to overcome complexity. Discrete probabilistic systems have been studied using logic. But logic has been chronically underdeveloped in the context of stochastic hybrid systems, i.e., systems with interacting discrete, continuous, and stochastic dynamics. We aim at overcoming this deficiency and introduce a dynamic logic for stochastic hybrid systems. Our results indicate that logic is a promising tool for understanding stochastic hybrid systems and can help taming some of their complexity. We introduce a compositional model for stochastic hybrid systems. We prove adaptivity, cadlag, and Markov time properties, and prove that the semantics of our logic is measurable. We present compositional proof rules, including rules for stochastic differential equations, and prove soundness.
Keywords: dynamic logic • proof calculus • stochastic differential equations • stochastic hybrid systems • stochastic processes

Sicun Gao, André Platzer and Edmund M. Clarke.
Quantifier elimination over finite fields with Gröbner bases.
In Franz Winkler, editor, Algebraic Informatics, Fourth International Conference, CAI 2011, Linz, Austria, June 2124, 2011, Proceedings, volume 6742 of LNCS, pp. 140157. Springer, 2011. © Springer
[bib  ✂  pdf  doi  arXiv]We give an algebraic quantifier elimination algorithm for the firstorder theory over any given finite field using Gröbner basis methods. The algorithm relies on the strong Nullstellensatz and properties of elimination ideals over finite fields. We analyze the theoretical complexity of the algorithm and show its application in the formal analysis of a biological controller model.
Keywords: Quantifier Elimination • Gröbner Bases • Finite Fields • Formal Verification

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. 4256. Springer, 2011. © Springer
[bib  ✂  pdf  doi  slides  study  TR]Car safety measures can be most effective when the cars on a street coordinate their control actions using distributed cooperative control. While each car optimizes its navigation planning locally to ensure the driver reaches his destination, all cars coordinate their actions in a distributed way in order to minimize the risk of safety hazards and collisions. These systems control the physical aspects of car movement using cyber technologies like local and remote sensor data and distributed V2V and V2I communication. They are thus cyberphysical systems. In this paper, we consider a distributed car control system that is inspired by the ambitions of the California PATH project, the CICAS system, SAFESPOT and PReVENT initiatives. We develop a formal model of a distributed car control system in which every car is controlled by adaptive cruise control. One of the major technical difficulties is that faithful models of distributed car control have both distributed systems and hybrid systems dynamics. They form distributed hybrid systems, which makes them very challenging for verification. In a formal proof system, we verify that the control model satisfies its main safety objective and guarantees collision freedom for arbitrarily many cars driving on a street, even if new cars enter the lane from onramps or multilane streets. The system we present is in many ways one of the most complicated cyberphysical systems that has ever been fully verified formally.
Keywords: distributed car control • multiagent systems • highway traffic safety • formal verification • distributed hybrid systems • adaptive cruise control

Erik P. Zawadzki, Geoffrey J. Gordon and André Platzer.
An InstantiationBased Theorem Prover for FirstOrder Programming.
In 14th International Conference on Artificial Intelligence and Statistics (AISTATS) 2011, Fort Lauderdale, FL, USA, Proceedings, volume 15 of JMLR W&CP, pp. 855863, 2011.
[bib  ✂  pdf  poster  proceedings]Firstorder programming (FOP) is a new representation language that combines the strengths of mixedinteger linear programming (MILP) and firstorder logic (FOL). In this paper we describe a novel feasibility proving system for FOP formulas that combines MILP solving with instancebased methods from theorem proving. This prover allows us to perform lifted inference by repeatedly refining a propositional MILP. We prove that this procedure is sound and refutationally complete: if a formula is infeasible our solver will demonstrate this fact in finite time. We conclude by demonstrating an implementation of our decision procedure on a simple firstorder planning problem.

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]We address the verification problem for distributed hybrid systems with nontrivial dynamics. Consider air traffic collision avoidance maneuvers, for example. Verifying dynamic appearance of aircraft during an ongoing collision avoidance maneuver is a longstanding and essentially unsolved problem. The resulting systems are not hybrid systems and their state space is not of the form R^n. They are distributed hybrid systems with nontrivial continuous and discrete dynamics in distributed state spaces whose dimension and topology changes dynamically over time. We present the first formal verification technique that can handle the complicated nonlinear dynamics of these systems. We introduce quantified differential invariants, which are properties that can be checked for invariance along the dynamics of the distributed hybrid system based on differentiation, quantified substitution, and quantifier elimination in realclosed fields. This gives a computationally attractive technique, because it works without having to solve the infinitedimensional differential equation systems underlying distributed hybrid systems. We formally verify a roundabout maneuver in which aircraft can appear dynamically.
Keywords: distributed hybrid systems • verification logic • quantified differential equations • quantified differential invariants

André Platzer.
Quantified differential dynamic logic for distributed hybrid systems.
In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 19th EACSL Annual Conference, CSL 2010, Brno, Czech Republic, August 2327, 2010. Proceedings, volume 6247 of LNCS, pp. 469483. Springer, 2010. © Springer
[bib  ✂  pdf  doi  slides  TR  LMCS'12]We address a fundamental mismatch between the combinations of dynamics that occur in complex physical systems and the limited kinds of dynamics supported in analysis. Modern applications combine communication, computation, and control. They may even form dynamic networks, where neither structure nor dimension stay the same while the system follows mixed discrete and continuous dynamics.
We provide the logical foundations for closing this analytic gap. We develop a system model for distributed hybrid systems that combines quantified differential equations with quantified assignments and dynamic dimensionalitychanges. We introduce a dynamic logic for verifying distributed hybrid systems and present a proof calculus for it. We prove that this calculus is a sound and complete axiomatization of the behavior of distributed hybrid systems relative to quantified differential equations. In our calculus we have proven collision freedom in distributed car control even when new cars may appear dynamically on the road.
Keywords: Dynamic logic • Distributed hybrid systems • Axiomatization • Theorem proving • Quantified differential equations

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 1215, pp. 243252. ACM, 2010. © ACM
[bib  ✂  pdf  doi  slides  TR]We address the problem of model checking stochastic systems, i.e. checking whether a stochastic system satisfies a certain temporal property with a probability greater (or smaller) than a fixed threshold. In particular, we present a novel Statistical Model Checking (SMC) approach based on Bayesian statistics. We show that our approach is feasible for hybrid systems with stochastic transitions, a generalization of Simulink/Stateflow models. Standard approaches to stochastic (discrete) systems require numerical solutions for large optimization problems and quickly become infeasible with larger state spaces. Generalizations of these techniques to hybrid systems with stochastic effects are even more challenging. The SMC approach was pioneered by Younes and Simmons in the discrete and nonBayesian case. It solves the verification problem by combining randomized sampling of system traces (which is very efficient for Simulink/Stateflow) with hypothesis testing or estimation. We believe SMC is essential for scaling up to large Stateflow/Simulink models. While the answer to the verification problem is not guaranteed to be correct, we prove that Bayesian SMC can make the probability of giving a wrong answer arbitrarily small. The advantage is that answers can usually be obtained much faster than with standard, exhaustive model checking techniques. We apply our Bayesian SMC approach to a representative example of stochastic discretetime hybrid system models in Stateflow/Simulink: a fuel control system featuring hybrid behavior and fault tolerance. We show that our technique enables faster verification than stateoftheart statistical techniques, while retaining the same error bounds. We emphasize that Bayesian SMC is by no means restricted to Stateflow/Simulink models: we have in fact successfully applied it to very large stochastic models from Systems Biology.

André Platzer and JanDavid Quesel.
European Train Control System: A case study in formal verification.
In Karin Breitman and Ana Cavalcanti, editors, 11th International Conference on Formal Engineering Methods, ICFEM, Rio de Janeiro, Brasil, Proceedings, volume 5885 of LNCS, pp. 246265. Springer, 2009. © Springer
[bib  ✂  pdf  doi  slides  kyx  TR  old]Complex physical systems have several degrees of freedom. They only work correctly when their control parameters obey corresponding constraints. Based on the informal specification of the European Train Control System (ETCS), we design a controller for its cooperation protocol. For its free parameters, we successively identify constraints that are required to ensure collision freedom. We formally prove the parameter constraints to be sharp by characterizing them equivalently in terms of reachability properties of the hybrid system dynamics. Using our deductive verification tool KeYmaera, we formally verify controllability, safety, liveness, and reactivity properties of the ETCS protocol that entail collision freedom. We prove that the ETCS protocol remains correct even in the presence of perturbation by disturbances in the dynamics. We verify that safety is preserved when a PI controlled speed supervision is used.
Keywords: formal verification of hybrid systems • train control • theorem proving • parameter constraint identification • disturbances

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. © Springer
This paper was awarded the FM Best Paper Award.
[bib  ✂  pdf  doi  slides  study  TR]Aircraft collision avoidance maneuvers are important and complex applications. Curved flight exhibits nontrivial continuous behavior. In combination with the control choices during air traffic maneuvers, this yields hybrid systems with challenging interactions of discrete and continuous dynamics. As a case study illustrating the use of a new proof assistant for a logic for nonlinear hybrid systems, we analyze collision freedom of roundabout maneuvers in air traffic control, where appropriate curved flight, good timing, and compatible maneuvering are crucial for guaranteeing safe spatial separation of aircraft throughout their flight. We show that formal verification of hybrid systems can scale to curved flight maneuvers required in aircraft control applications. We introduce a fully flyable variant of the roundabout collision avoidance maneuver and verify safety properties by compositional verification.
Keywords: formal verification of hybrid systems • deduction • air traffic control • logic for hybrid systems

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, pp. 218234. Springer, 2009. © Springer
[bib  ✂  pdf  doi  TR]Recently, there has been considerable interest in the use of Model Checking for Systems Biology. Unfortunately, the state space of stochastic biological models is often too large for classical Model Checking techniques. For these models, a statistical approach to Model Checking has been shown to be an effective alternative. Extending our earlier work, we present the first algorithm for performing statistical Model Checking using Bayesian Sequential Hypothesis Testing. We show that our Bayesian approach outperforms current statistical Model Checking techniques, which rely on tests from Classical (aka Frequentist) statistics, by requiring fewer system simulations. Another advantage of our approach is the ability to incorporate prior Biological knowledge about the model being verified. We demonstrate our algorithm on a variety of models from the Systems Biology literature and show that it enables faster verification than stateoftheart techniques, even when no prior knowledge is available.

André Platzer, JanDavid Quesel and Philipp Rümmer.
Real world verification.
In Renate A. Schmidt, editor, International Conference on Automated Deduction, CADE22, Montreal, Canada, Proceedings, volume 5663 of LNCS, pp. 485501. Springer, 2009. © Springer
[bib  ✂  pdf  doi  slides  TR  smtlib]
Introduces a decision procedure for universal nonlinear real arithmetic combining Gröbner bases and semidefinite programming for the Real Nullstellensatz.Scalable handling of real arithmetic is a crucial part of the verification of hybrid systems, mathematical algorithms, and mixed analog/digital circuits. Despite substantial advances in verification technology, complexity issues with classical decision procedures are still a major obstacle for formal verification of realworld applications, e.g., in automotive and avionic industries. To identify strengths and weaknesses, we examine state of the art symbolic techniques and implementations for the universal fragment of realclosed fields: approaches based on quantifier elimination, Gröbner Bases, and semidefinite programming for the Positivstellensatz. Within a uniform context of the verification tool KeYmaera, we compare these approaches qualitatively and quantitatively on verification benchmarks from hybrid systems, textbook algorithms, and on geometric problems. Finally, we introduce a new decision procedure combining Gröbner Bases and semidefinite programming for the real Nullstellensatz that outperforms the individual approaches on an interesting set of problems.
Keywords: realclosed fields • decision procedures • hybrid systems • software verification

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. © Springer
[bib  ✂  pdf  doi  slides  study  TR  FMSD'09]We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations whose righthand sides are polynomials in the state variables. In order to verify nontrivial systems without solving their differential equations and without numerical errors, we use a continuous generalization of induction, for which our algorithm computes the required differential invariants. As a means for combining local differential invariants into global system invariants in a sound way, our fixedpoint algorithm works with a compositional verification logic for hybrid systems. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively with differential invariants until safety becomes provable. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification procedure. We verify roundabout maneuvers in air traffic management and collision avoidance in train control.
Keywords: verification of hybrid systems • differential invariants • verification logic • fixedpoint engine

André Platzer.
Differential dynamic logic for verifying parametric hybrid systems.
In Nicola Olivetti, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2007, Aix en Provence, France, July 36, 2007, Proceedings, volume 4548 of LNCS, pp. 216232. Springer, 2007. © Springer
This paper was awarded the TABLEAUX Best Paper Award.
[bib  ✂  pdf  doi  slides  study  TR]We introduce a firstorder dynamic logic for reasoning about systems with discrete and continuous state transitions, and we present a sequent calculus for this logic. As a uniform model, our logic supports hybrid programs with discrete and differential actions. For handling real arithmetic during proofs, we lift quantifier elimination to dynamic logic. To obtain a modular combination, we use side deductions for verifying interacting dynamics. With this, our logic supports deductive verification of hybrid systems with symbolic parameters and firstorder definable flows. Using our calculus, we prove a parametric inductive safety constraint for speed supervision in a train control system.
Keywords: dynamic logic • sequent calculus • verification of parametric hybrid systems • quantifier elimination

André Platzer.
A temporal dynamic logic for verifying hybrid system invariants.
In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, USA, Proceedings, volume 4514 of LNCS, pp. 457471. Springer, 2007. © Springer
[bib  ✂  pdf  doi  slides  study  TR]We combine firstorder dynamic logic for reasoning about possible behaviour of hybrid systems with temporal logic for reasoning about the temporal behaviour during their operation. Our logic supports verification of hybrid programs with firstorder definable flows and provides a uniform treatment of discrete and continuous evolution. For our combined logic, we generalise the semantics of dynamic modalities to refer to hybrid traces instead of final states. Further, we prove that this gives a conservative extension of dynamic logic. On this basis, we provide a modular verification calculus that reduces correctness of temporal behaviour of hybrid systems to nontemporal reasoning. Using this calculus, we analyse safety invariants in a train control system and symbolically synthesise parametric safety constraints.
Keywords: dynamic logic • temporal logic • sequent calculus • logic for hybrid systems • deductive verification of embedded systems

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. 473486. Springer, 2007, © Springer
[bib  ✂  pdf  doi  slides  tool]In this paper, we analyze limits of approximation techniques for (nonlinear) continuous image computation in model checking hybrid systems. In particular, we show that even a single step of continuous image computation is not semidecidable numerically even for a very restricted class of functions. Moreover, we show that symbolic insight about derivative bounds provides sufficient additional information for approximation refinement model checking. Finally, we prove that purely numerical algorithms can perform continuous image computation with arbitrarily high probability. Using these results, we analyze the prerequisites for a safe operation of the roundabout maneuver in air traffic collision avoidance.
Keywords: model checking • hybrid systems • image computation

Bernhard Beckert and André Platzer.
Dynamic logic with nonrigid functions:
A basis for objectoriented program verification.
In Uli Furbach and Natarajan Shankar, editors, Automated Reasoning, Third International Joint Conference, IJCAR 2006, Seattle, WA, USA, August 1720, 2006, Proceedings, volume 4130 of LNCS, pp. 266280. Springer, 2006. © Springer
[bib  ✂  pdf  doi  slides]We introduce a dynamic logic that is enriched by nonrigid functions, i.e., functions that may change their value from state to state (during program execution), and we present a (relatively) complete sequent calculus for this logic. In conjunction with dynamically typed object enumerators, nonrigid functions allow to embed notions of objectorientation in dynamic logic, thereby forming a basis for verification of objectoriented programs. A semantical generalisation of substitutions, called state update, which we add to the logic, constitutes the central technical device for dealing with object aliasing during function modification. With these few extensions, our dynamic logic captures the essential aspects of the complex verification system KeY and, hence, constitutes a foundation for objectoriented verification with the principles of reasoning that underly the successful KeY case studies.
Keywords: dynamic logic • sequent calculus • program logic • software verification • logical foundations of programming languages • objectorientation
Short & Tool Publications

James Gallicchio, Yong Kiam Tan, Stefan Mitsch and André Platzer.
Implicit definitions with differential equations for KeYmaera X (System Description).
In Jasmin Blanchette, Laura Kovacs and Dirk Pattinson, editors, Automated Reasoning, International Joint Conference, IJCAR 2022, Haifa, Israel, August 712, 2022, Proceedings. volume 13385 of LNCS, pp. 723733. Springer, 2022. © The authors
[bib  ✂  pdf  doi  arXiv]Definition packages in theorem provers provide users with means of defining and organizing concepts of interest. This system description presents a new definition package for the hybrid systems theorem prover KeYmaera X based on differential dynamic logic (dL). The package adds KeYmaera X support for userdefined smooth functions whose graphs can be implicitly characterized by dL formulas. Notably, this makes it possible to implicitly characterize functions, such as the exponential and trigonometric functions, as solutions of differential equations and then prove properties of those functions using dL's differential equation reasoning principles. Trustworthiness of the package is achieved by minimally extending KeYmaera X's soundnesscritical kernel with a single axiom scheme that expands function occurrences with their implicit characterization. Users are provided with a highlevel interface for defining functions and nonsoundnesscritical tactics that automate lowlevel reasoning over implicit characterizations in hybrid system proofs.
Keywords: Definitions • Differential dynamic logic • Verification of hybrid systems • Theorem proving

Nathan Fulton, Stefan Mitsch, JanDavid Quesel, Marcus Völp and André Platzer.
KeYmaera X: An aXiomatic tactical theorem prover for hybrid systems.
In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE25, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 527538. Springer, 2015. © Springer
[bib  ✂  pdf  doi  slides  poster  tool]KeYmaera X is a theorem prover for differential dynamic logic (dL), a logic for specifying and verifying properties of hybrid systems. Reasoning about complicated hybrid systems models requires support for sophisticated proof techniques, efficient computation, and a user interface that crystallizes salient properties of the system. KeYmaera X allows users to specify custom proof search techniques as tactics, execute these tactics in parallel, and interface with partial proofs via an extensible user interface.
Advanced proof search featuresand userdefined tactics in particularare difficult to check for soundness. To admit extension and experimentation in proof search without reducing trust in the prover, KeYmaera X is built up from a small trusted kernel. The prover kernel contains a list of sound dL axioms that are instantiated using a uniform substitution proof rule. Isolating all soundnesscritical reasoning to this prover kernel obviates the intractable task of ensuring that each new proof search algorithm is implemented correctly. Preliminary experiments suggest that a single layer of tactics on top of the prover kernel provides a rich language for implementing novel and sophisticated proof search techniques.
Keywords: verification of hybrid systems • theorem proving • differential dynamic logic

André Platzer and JanDavid Quesel.
KeYmaera: A hybrid theorem prover for hybrid systems.
In Alessandro Armando, Peter Baumgartner and Gilles Dowek, editors, Automated Reasoning, Fourth International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings, volume 5195 of LNCS, pp. 171178. Springer, 2008. © Springer
[bib  ✂  pdf  doi  slides  tool]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, which is a realvalued firstorder dynamic logic for hybrid programs, a program notation for hybrid automata. For automating the verification process, KeYmaera implements a generalized freevariable 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 • automated theorem proving • decision procedures • computer algebra • verification of hybrid systems

André Platzer and JanDavid 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. 646649. Springer, 2008. © Springer
[bib  ✂  pdf  doi  poster]We formally verify hybrid safety properties of cooperation protocols in a fully parametric version of the European Train Control System (ETCS). We present a formal model using hybrid programs and verify correctness using our logicbased decomposition procedure. This procedure supports free parameters and parameter discovery, which is required to determine correct design choices for free parameters of ETCS.
Keywords: parametric verification • logic for hybrid systems • symbolic decomposition

André Platzer.
Differential logic for reasoning about hybrid systems.
In Alberto Bemporad, Antonio Bicchi and Giorgio Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pp. 746749. Springer, 2007. © Springer
[bib  ✂  pdf  doi  poster]We propose a firstorder dynamic logic for reasoning about hybrid systems. As a uniform model for discrete and continuous evolutions in hybrid systems, we introduce hybrid programs with differential actions. Our logic can be used to specify and verify correctness statements about hybrid programs, which are suitable for symbolic processing by calculus rules. Using firstorder variables, our logic supports systems with symbolic parameters. With dynamic modalities, it is prepared to handle multiple system components.
Keywords: dynamic logic • hybrid systems • parametric verification
Workshop Publications

Andreas Müller, Stefan Mitsch, Wieland Schwinger and André Platzer.
A componentbased hybrid systems verification and implementation tool in KeYmaera X.
In Roger Chamberlain, Walid Taha and Martin Törngren, editors, CyPhy 2018, WESE 2018: Cyber Physical Systems. ModelBased Design, revised selected papers, volume 11615 of LNCS, pp. 91110. Springer, 2019. © Springer
[bib  ✂  pdf  doi]Safetycritical cyberphysical systems (CPS) should be analyzed using formal verification techniques in order to gain insight into and obtain rigorous safety guarantees about their behavior. For practical purposes, methods are needed to split modeling and verification effort into manageable pieces and link formal artifacts and techniques with implementation. In this paper we present a tool chain that supports componentbased modeling and verification of CPS, generation of monitors, and systematic (but unverified) translation of models and monitors into executable code. A running example demonstrates how to model a system in a componentbased fashion in differential dynamic logic (dL), how to represent and structure these models in the syntax of the hybrid systems theorem prover KeYmaera X (which implements dL), and how to prove properties in KeYmaera X. The verified components are the source for translation into executable C code, which can be run on controlled components (e.g., a robot). Additionally, we demonstrate how to generate monitors that validate the behavior of uncontrolled components (e.g., validate the assumptions made about obstacles)
Keywords: Componentbased development • Hybrid systems • Formal verification

Stefan Mitsch and André Platzer.
The KeYmaera X proof IDE:
Concepts on usability in hybrid systems theorem proving.
In Catherine Dubois, Paolo Masci and Dominique Méry, editors, 3rd Workshop on Formal Integrated Development Environment FIDE 2016, volume 240 of EPTCS, pp. 6781, 2017. © The authors
[bib  ✂  pdf  doi  tool  arXiv]Hybrid systems verification is quite important for developing correct controllers for physical systems, but is also challenging. Verification engineers, thus, need to be empowered with ways of guiding hybrid systems verification while receiving as much help from automation as possible. Due to undecidability, verification tools need sufficient means for intervening during the verification and need to allow verification engineers to provide system design insights.
This paper presents the design ideas behind the user interface for the hybrid systems theorem prover KeYmaera X. We discuss how they make it easier to prove hybrid systems as well as help learn how to conduct proofs in the first place. Unsurprisingly, the most difficult user interface challenges come from the desire to integrate automation and human guidance. We also share thoughts how the success of such a user interface design could be evaluated and anecdotal observations about it.

Stefan Mitsch, JanDavid Quesel, and André Platzer.
From safety to guilty & from liveness to niceness.
In Calin Belta and Hadas KressGazit, editors, 5th Workshop on Formal Methods for Robotics and Automation, 2014. © The author
[bib  ✂  pdf]Robots are solving challenging tasks that we want them to be able to perform (liveness), but we also do not want them to endanger their surroundings (safety). Formal methods provide ways of proving such correctness properties, but have the habit of only saying "yes" when the answer is "yes" (soundness). More often than not, formal methods say "no": They find out that the system is neither safe nor live, because there are "unexpected" circumstances in which the robot just cannot do what we expect it to. Inspecting those unexpected circumstances is informative, and identifies constraints on reasonable behavior of the environment. This ultimately leads from safety to the question of who is guilty depending on whose action caused the safety violation. It also leads from liveness to the question of what behavior of the environment is nice enough so that the robot can finish its task.

Erik P. Zawadzki, Geoffrey J. Gordon and André Platzer .
A projection algorithm for strictly monotone linear complementarity problems.
In 6th NIPS Workshop on Optimization for Machine Learning, 2013.
[bib  ✂  pdf  eprint]Complementary problems play a central role in equilibrium finding, physical simulation, and optimization. As a consequence, we are interested in understanding how to solve these problems quickly, and this often involves approximation. In this paper we present a method for approximately solving strictly monotone linear complementarity problems with a Galerkin approximation. We also give bounds for the approximate error, and prove novel bounds on perturbation error. These perturbation bounds suggest that a Galerkin approximation may be much less sensitive to noise than the original LCP.

André Platzer.
Teaching CPS foundations with contracts.
First Workshop on CyberPhysical Systems Education (CPSEd 2013), pp. 710. 2013.
[bib  ✂  pdf  eprint  slides  poster  course]We describe the experience with courses that teach the Foundations of Cyberphysical Systems (CPS) and methods for ensuring the correctness of CPS designs. CPSs combine cyber effects (computation & communication) with physical effects (motion or other physical processes). CPS represent a paradigm shift that transcends the separation of computer science, which traditionally focuses on computation & communication isolated from the physical world, versus engineering and physics, which traditionally focus more on physical effects than on software intensive solutions. CPS are a unique challenge and unique opportunity for education. They challenge, because of their mathematical demand and interdisciplinary nature. CPS are an opportunity, because students learn important insights about the interface with other areas and develop a deeper understanding about the principles that make cyber and physical aspects work together. The course addresses the challenges of designing CPS that people can bet their lives on by emphasizing CPS contracts.
Keywords: cyberphysical systems • foundations • education • correctness • contracts

André Platzer.
Combining deduction and algebraic constraints for hybrid system analysis.
In Bernhard Beckert, editor, 4th International Verification Workshop, VERIFY'07, Workshop at Conference on Automated Deduction (CADE), Bremen, Germany, CEUR Workshop Proceedings, 259:164178, 2007.
[bib  ✂  pdf  eprint  slides]We show how theorem proving and methods for handling real algebraic constraints can be combined for hybrid system verification. In particular, we highlight the interaction of deductive and algebraic reasoning that is used for handling the joint discrete and continuous behaviour of hybrid systems. We illustrate proof tasks that occur when verifying scenarios with cooperative traffic agents. From the experience with these examples, we analyse proof strategies for dealing with the practical challenges for integrated algebraic and deductive verification of hybrid systems, and we propose an iterative background closure strategy.
Keywords: modular prover combination • analytic tableaux • verification of hybrid systems • dynamic logic

Stephanie Kemper and André Platzer.
SATbased abstraction refinement for realtime 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:107122, 2007
[bib  ✂  pdf  doi  slides  tool]In this paper, we present an abstraction refinement approach for model checking safety properties of realtime systems using SATsolving. We present a faithful embedding of bounded model checking for systems of timed automata into propositional logic with linear arithmetic and prove correctness. With this logical representation, we achieve a linearsize representation of parallel composition and introduce a quick abstraction technique that works uniformly for clocks, events, and states. When necessary, abstractions are refined by analysing spurious counterexamples using a promising extension of counterexampleguided abstraction refinement with syntactic information about Craig interpolants. To support generalisations, our overall approach identifies the algebraic and logical principles required for logicbased abstraction refinement.
Keywords: abstraction refinement • model checking • realtime systems • SAT • Craig interpolation

André Platzer.
Towards a hybrid dynamic logic for hybrid dynamic systems.
In Patrick Blackburn, Thomas Bolander, Torben Braüner, Valeria de Paiva and Jørgen Villadsen, editors, Proc., International Workshop on Hybrid Logic, HyLo 2006, Seattle, USA, Electr. Notes Theor. Comput. Sci. 174(6):6377, 2007.
[bib  ✂  pdf  doi  slides]We introduce a hybrid variant of a dynamic logic with continuous state transitions along differential equations, and we present a sequent calculus for this extended hybrid dynamic logic. With the addition of satisfaction operators, this hybrid logic provides improved system introspection by referring to properties of states during system evolution. In addition to this, our calculus introduces statebased reasoning as a paradigm for delaying expansion of transitions using nominals as symbolic state labels. With these extensions, our hybrid dynamic logic capabilities the capabilities for compositional reasoning about (semialgebraic) hybrid dynamic systems. Moreover, the constructive reasoning support for goaloriented analytic verification of hybrid dynamic systems carries over from the base calculus to our extended calculus.
Keywords: hybrid logic • dynamic logic • sequent calculus • compositional verification • realtime hybrid dynamic systems
Invited Papers

André Platzer.
The logical path to autonomous cyberphysical systems.
In David Parker and Verena Wolf, editors, International Conference on Quantitative Evaluation of SysTems, QEST 2019, Glasgow, UK, Proceedings, volume 11785 of LNCS, pp. 2533. Springer, 2019. © Springer
Invited paper.
[bib  ✂  pdf  doi  slides]Autonomous cyberphysical systems are systems that combine the physics of motion with advanced cyber algorithms to act on their own without close human supervision. The present consensus is that reasonable levels of autonomy, such as for selfdriving cars or autonomous drones, can only be reached with the help of artificial intelligence and machine learning algorithms that cope with the uncertainties of the real world. That makes safety assurance even more challenging than it already is in cyberphysical systems (CPSs) with classically programmed control, precisely because AI techniques are lauded for their flexibility in handling unpredictable situations, but are themselves harder to predict.
This paper identifies the logical path toward autonomous cyberphysical systems in multiple steps. First, differential dynamic logic (dL) provides a logical foundation for developing cyberphysical system models with the mathematical rigor that their safetycritical nature demands. Then, its ModelPlex technique provides a logically correct way to tame the subtle relationship of CPS models to CPS implementations. Finally, the resulting logical monitor conditions can then be exploited to safeguard the decisions of learning agents, guide the optimization of learning processes, and resolve the nondeterminism frequently found in verification models. Overall, logic leads the way in combining the best of both worlds: the strong predictions that formal verification techniques provide alongside the strong flexibility that the use of AI provides.
Keywords: Autonomous cyberphysical systems • Safe AI • Hybrid systems • Differential dynamic logic • Formal verification • Runtime verification

Nathan Fulton and André Platzer.
Safe AI for CPS.
In International Testing Conference ITC'18, IEEE, 2018. © IEEE
Invited paper.
[bib  ✂  pdf  doi  slides]Autonomous cyberphysical systems  such as selfdriving cars and autonomous drones  often leverage artificial intelligence and machine learning algorithms to act well in open environments. Although testing plays an important role in ensuring safety and robustness, modern autonomous systems have grown so complex that achieving safety via testing alone is intractable. Formal verification reduces this testing burden by ruling out large classes of errant behavior at design time. This paper reviews recent work toward developing formal methods for cyberphysical systems that use AI for planning and control by combining the rigor of formal proofs with the flexibility of reinforcement learning.
Keywords: AI safety • Cyberphysical systems • Formal methods • Safe reinforcement learning • Hybrid systems • Theorem proving

Franz Franchetti, Tze Meng Low, Stefan Mitsch, Juan Paolo Mendoza, Liangyan Gui, Amarin Phaosawasdi, David Padua, Soummya Kar, José M. F. Moura, Mike Franusich, Jeremy Johnson, André Platzer and Manuela Veloso.
Highassurance SPIRAL:
Endtoend guarantees for robot and car control.
IEEE Control Systems 37(2), pp. 82103. 2017. © IEEE
[bib  ✂  pdf  doi]

André Platzer.
Logic & proofs for cyberphysical systems.
In Nicola Olivetti and Ashish Tiwari, editors, Automated Reasoning, 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, Proceedings, volume 9706 of LNCS, pp. 1521. Springer, 2016. © Springer
Invited paper.
[bib  ✂  pdf  doi  slides]Cyberphysical systems (CPS) combine cyber aspects such as communication and computer control with physical aspects such as movement in space, which arise frequently in many safetycritical application domains, including aviation, automotive, railway, and robotics. But how can we ensure that these systems are guaranteed to meet their design goals, e.g., that an aircraft will not crash into another one?
This paper highlights some of the most fascinating aspects of cyberphysical systems and their dynamical systems models, such as hybrid systems that combine discrete transitions and continuous evolution along differential equations. Because of the impact that they can have on the real world, CPSs deserve proof as safety evidence.
Multidynamical systems understand complex systems as a combination of multiple elementary dynamical aspects, which makes them natural mathematical models for CPS, since they tame their complexity by compositionality. The family of differential dynamic logics achieves this compositionality by providing compositional logics, programming languages, and reasoning principles for CPS. Differential dynamic logics, as implemented in the theorem prover KeYmaera X, have been instrumental in verifying many applications, including the Airborne Collision Avoidance System ACAS X, the European Train Control System ETCS, automotive systems, mobile robot navigation, and a surgical robot system for skullbase surgery. This combination of strong theoretical foundations with practical theorem proving challenges and relevant applications makes Logic for CPS an ideal area for compelling and rewarding research.
Keywords: Logic • Cyberphysical systems • Multidynamical systems • Differential dynamic logic • KeYmaera X

André Platzer.
How to prove hybrid systems and why that matters.
International Conference on Complex Systems Engineering, ICCSE 2015 © IEEE
Invited paper
[bib  ✂  pdf  doi]This invited talk provides a brief exposition how hybrid systems proving works, why hybrid systems verification is an important device to ensure the safety of complex systems, and gives an idea where that technology is successful.

JeanBaptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki, and André Platzer.
Formal verification of ACAS X, an industrial airborne collision avoidance system.
In Alain Girault and Nan Guan, editors, International Conference on Embedded Software, EMSOFT'15, Amsterdam, The Netherlands, Proceedings, pp. 127136. IEEE Press, 2015. © IEEE
[bib  ✂  pdf  doi]Formal verification of industrial systems is very challenging, due to reasons ranging from scalability issues to communication difficulties with engineeringfocused teams. More importantly, industrial systems are rarely designed for verification, but rather for operational needs. In this paper we present an overview of our experience using hybrid systems theorem proving to formally verify ACAS X, an airborne collision avoidance system for airliners scheduled to be operational around 2020. The methods and proof techniques presented here are an overview of the work already presented, while the evaluation of ACAS X has been significantly expanded and updated to the most recent version of the system, run 13. The effort presented in this paper is an integral part of the ACAS X development and was performed in tight collaboration with the ACAS X development team.
Keywords: Airborne Collision Avoidance • ACAS X • Hybrid systems • Theorem proving • Federal Aviation Administration • Aircraft • Markov decision processes • Cyberphysical systems

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]The purpose of this article is to serve as a lightweight introduction into the mysteries of analog and hybrid computing models from a dynamical systems and programming languages perspective. Hybrid systems are the dynamical systems that combine both models of computation, i.e., have interacting discrete and continuous dynamics. They have found widespread application as models for embedded computing in embedded systems as well as in cyberphysical systems. The primary role hybrid systems have played so far is to allow us to model how a (discrete) computer controller interacts with the (continuous) physical world and to analyze by means of formal proofs or reachability analyzes whether this interaction is safe or not. Without any doubt, such analyzes are of tremendous importance for our society, because they determine whether we can bet our lives on those systems.
But this article argues that hybrid systems also have computational consequences that make them an interesting subject to study from a computability theory perspective. Hybrid systems are described by hybrid programs or hybrid automata, both hybrid generalizations of corresponding discrete computational models. The phenomenon of discrete and continuous interplay, which hybrid systems provide, is fundamental and raises interesting computability questions. For example: what is computable using the analogue computation capabilities of continuous dynamical systems? How do the discrete computation capabilities of discrete dynamical systems relate to classical models of computation à la ChurchTuring? What happens in hybrid computation, where discrete and continuous computation interact? Are the two facets of computation, discrete and continuous, of fundamentally different character or are they two sides of the same computational coin? This article answers some of these questions using the rich theory that a logical characterization of hybrid systems in differential dynamic logic of hybrid programs provides. But the article is meant primarily as a manifesto for the significance and inherent beauty that these questions possess in the first place.

André Platzer.
Logical analysis of hybrid systems:
A complete answer to a complexity challenge.
Journal of Automata, Languages and Combinatorics 17(24), pp. 265275. 2012.
Invited Paper
[bib  ✂  pdf  doi]Hybrid systems are systems with interacting discrete and continuous dynamics. They are models for understanding, e.g., computer systems interfacing with the physical environment. Hybrid systems have a complete axiomatization in differential dynamic logic relative to continuous systems. They also have a complete axiomatization relative to discrete systems. Moreover, there is a constructive reduction of properties of hybrid systems to corresponding properties of continuous systems or to corresponding properties of discrete systems. We briefly summarize and discuss some of the implications of these results.
Keywords: survey • differential dynamic logic • hybrid systems • completeness • complexity

André Platzer.
Logical analysis of hybrid systems:
A complete answer to a complexity challenge.
In Martin Kutrib, Nelma Moreira and Rogério Reis, editors, Descriptional Complexity of Formal Systems, DCFS'12, Braga, Portugal, Proceedings, volume 7386 of LNCS, pp. 4349. Springer, 2012. © Springer
Invited Paper
[bib  ✂  pdf  doi]Hybrid systems have a complete axiomatization in differential dynamic logic relative to continuous systems. They also have a complete axiomatization relative to discrete systems. Moreover, there is a constructive reduction of properties of hybrid systems to corresponding properties of continuous systems or to corresponding properties of discrete systems. We briefly summarize and discuss some of the implications of these results.
Keywords: differential dynamic logic • hybrid systems • complexity

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. © Springer
Invited paper.
[bib  ✂  pdf  doi  slides]Hybrid systems, i.e., dynamical systems combining discrete and continuous dynamics, have a complete axiomatization in differential dynamic logic relative to differential equations. Differential invariants are a natural induction principle for proving properties of the remaining differential equations. We study the equational case of differential invariants using a differential operator view. We relate differential invariants to Lie's seminal work and explain important structural properties resulting from this view. Finally, we study the connection of differential invariants with partial differential equations in the context of the inverse characteristic method for computing differential invariants.
Keywords: differential dynamic logic • differential invariants • differential equations • hybrid systems

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]We study the logic of dynamical systems, that is, logics and proof principles for properties of dynamical systems. Dynamical systems are mathematical models describing how the state of a system evolves over time. They are important in modeling and understanding many applications, including embedded systems and cyberphysical systems. In discrete dynamical systems, the state evolves in discrete steps, one step at a time, as described by a difference equation or discrete state transition relation. In continuous dynamical systems, the state evolves continuously along a function, typically described by a differential equation. Hybrid dynamical systems or hybrid systems combine both discrete and continuous dynamics.
This is a brief survey of differential dynamic logic for specifying and verifying properties of hybrid systems. We explain hybrid system models, differential dynamic logic, its semantics, and its axiomatization for proving logical formulas about hybrid systems. We study differential invariants, i.e., induction principles for differential equations. We briefly survey theoretical results, including soundness and completeness and deductive power. Differential dynamic logic has been implemented in automatic and interactive theorem provers and has been used successfully to verify safetycritical applications in automotive, aviation, railway, robotics, and analogue electrical circuits.
Keywords: logic of dynamical systems • dynamic logic • differential dynamic logic • hybrid systems • axiomatization • deduction

Nikos Aréchiga, Sarah M. Loos, André Platzer and Bruce H. Krogh.
Using theorem provers to guarantee closedloop system properties.
In Dawn Tilbury, editor, American Control Conference, ACC, Montréal, Canada, June 2729. pp. 35733580. 2012. © IEEE
[bib  ✂  pdf  doi]This paper presents a new approach for leveraging the power of theorem provers for formal verification to provide sufficient conditions that can be checked on embedded control designs. Theorem provers are often most efficient when using generic models that abstract away many of the controller details, but with these abstract models very general conditions can be verified under which desirable properties such as safety can be guaranteed for the closedloop system. We propose an approach in which these sufficient conditions are static conditions that can be checked for the specific controller design, without having to include the dynamics of the plant. We demonstrate this approach using the KeYmaera theorem prover for differential dynamic logic for two examples: an intelligent cruise controller and a cooperative intersection collision avoidance system (CICAS) for leftturn assist. In each case, safety of the closedloop system proved using KeYmaera provides static sufficient conditions that are checked for the controller design.

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. 11811186. 2011. © IEEE
[bib  ✂  pdf  doi  slides  study]Intelligent vehicle systems have interesting prospects for solving inefficiencies and risks in ground transportation, e.g., by making cars aware of their environment and regulating speed intelligently. If the computer control technology reacts fast enough, intelligent control can be used to increase the density of cars on the streets. The technology may also help prevent crashes at intersections, which cost the US $97 Billion in the year 2000. The crucial prerequisite for intelligent vehicle control, however, is that it must be correct, for it may otherwise do more harm than good. Formal verification techniques provide the best reliability guarantees but have had difficulties in the past with scaling to such complex systems. We report our successes with a logical approach to hybrid systems verification, which can capture discrete control decisions and continuous driving dynamics. We present a model for the interaction of two cars and a traffic light at a two lane intersection and verify with a formal proof that our system always ensures collision freedom and that our controller always prevents cars from running red lights.

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. © Springer
Invited tutorial.
[bib  ✂  pdf  doi  slides]Hybrid systems are models for complex physical systems and have become a widely used concept for understanding their behavior. Many applications are safetycritical, including car, railway, and air traffic control, robotics, physicalchemical process control, and biomedical devices. Hybrid systems analysis studies how we can build computerised controllers for physical systems which are guaranteed to meet their design goals. The continuous dynamics of hybrid systems can be modeled by differential equations, the discrete dynamics by a combination of discrete statetransitions and conditional execution. The discrete and continuous dynamics interact to form hybrid systems, which makes them quite challenging for verification.
In this tutorial, we survey stateoftheart verification techniques for hybrid systems. In particular, we focus on a coherent logical approach for systematic hybrid systems analysis. We survey theory, practice, and applications, and show how hybrid systems can be verified in the hybrid systems verification tool KeYmaera. KeYmaera has been used successfully to verify safety, reactivity, controllability, and liveness properties, including collision freedom in air traffic, car, and railway control systems. It has also been used to verify properties of electrical circuits.

André Platzer.
Differential dynamic logic:
Automated theorem proving for hybrid systems.
Künstliche Intelligenz 24(1), pp. 7577, 2010. © Springer
Invited paper.
[bib  ✂  doi]Designing and analyzing hybrid systems, which are models for complex physical systems, is expensive and errorprone. The dissertation presented in this article introduces a verification logic that is suitable for analyzing the behavior of hybrid systems. It presents a proof calculus and a new deductive verification tool for hybrid systems that has been used successfully to verify aircraft and train control.

André Platzer.
Verification of cyberphysical transportation systems.
IEEE Intelligent Systems 24(4), pp. 1013, Jul/Aug, 2009. © IEEE
Invited paper.
[bib  ✂  doi]Cyberphysical system technology has an important share in modern intelligent transportation systems, including next generation flight, rail, and car control. This control technology is intended to help improve performance objectives like throughput and improve overall system safety. To ensure that these transportation systems operate correctly, new analysis techniques are needed that consider physical movement combined with computational control to establish properties like collision freedom. Logicbased analysis can verify the correct functioning of these cyberphysical systems.
Keywords: cyberphysical transportation systems • train control • air traffic control • logicbased analysis • verification

Werner Damm, Alfred Mikschl, Jens Oehlerking, ErnstRü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 RealTime Systems, volume 4700 of LNCS, pp. 115169. Springer, 2007. © Springer
Invited paper.
[bib  ✂  pdf  doi]We present a verification methodology for cooperating traffic agents covering analysis of cooperation strategies, realization of strategies through control, and implementation of control. For each layer, we provide dedicated approaches to formal verification of safety and stability properties of the design. The range of employed verification techniques invoked to span this verification space includes application of preverified design patterns, automatic synthesis of Lyapunov functions, constraint generation for parameterized designs, modelchecking in rich theories, and abstraction refinement. We illustrate this approach with a variant of the European Train Control System (ETCS), employing layer specific verification techniques to layer specific views of an ETCS design.
Theses

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]Hybrid systems are models for complex physical systems and are defined as dynamical systems with interacting discrete transitions and continuous evolutions along differential equations. With the goal of developing a theoretical and practical foundation for deductive verification of hybrid systems, we introduce differential dynamic logic as a new logic with which correctness properties of hybrid systems with parameterized system dynamics can be specified and verified naturally. As a verification technique that is suitable for automation, we introduce a free variable proof calculus with a novel combination of realvalued free variables and Skolemisation for lifting quantifier elimination for real arithmetic to dynamic logic. The calculus is compositional, i.e., it reduces properties of hybrid systems successively to properties of their parts. Our main result proves that this calculus axiomatises the transition behaviour of hybrid systems completely relative to differential equations.
Systematically, we develop automated theorem proving techniques for our calculus and present proof procedures to tackle the complexities of integrating decision procedures for real arithmetic. For our logic, we further complement discrete induction with differential induction as a new continuous generalization of induction, with which hybrid systems can be verified by exploiting their differential constraints algebraically without having to solve them. Finally, we develop a fixedpoint algorithm for computing the differential invariants required for differential induction, and we introduce a differential saturation procedure that refines the system dynamics successively with differential invariants until correctness becomes provable. As a systematic combination of logicbased techniques, we obtain a sound verification procedure that is particularly suitable for parametric hybrid systems.
We demonstrate our approach by verifying safety, controllability, liveness, and collision avoidance properties in case studies ranging from train control applications in the European Train Control System to air traffic control, where we prove collision avoidance in aircraft roundabout maneuvers.
Keywords: dynamic logic • differential equations • logic for hybrid systems • free variable calculus • sequent calculus • axiomatisation • automated theorem proving • real arithmetic • verification of hybrid systems • differential induction • fixedpoint engines • train control • air traffic control

André Platzer.
An Objectoriented 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 nonrigid functions: A basis for objectoriented program verification at IJCAR 2006.
[bib  ✂  pdf  slides  IJCAR'06]With the goal of this thesis being to create a dynamic logic for objectoriented languages, ODL is developed along with a sound and relatively complete calculus. The dynamic logic contains only the absolute logical essentials of objectorientation, yet still allows a ``natural'' representation of all other features of common objectoriented programming languages. ODL is an extension of a dynamic logic for imperative While programs by function modification and dynamic type checks. A generalisation of substitutions, called updates, constitute the central technical device for dealing with object aliasing arising from function modification and for retaining a manageable calculus in practical application scenarios. Further, object enumerators realise object creation in a natural yet powerful way. Finally, completeness is proven relative to firstorder arithmetic. Along with the soundness result, this proof constitutes the central part of this thesis and even copes with states containing uncomputable functions.

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]In this thesis we examine the possibility of automatically constructing the program specification from an implementation, both from a theoretical perspective and as a practical approach with a sequent calculus. As a setting for program specifications we choose dynamic logic for the Java programming language. We show thatdespite the undecidable nature of program analysisthe strongest specification of any program can always be constructed algorithmically. Further we outline a practical approach embedded into a sequent calculus for dynamic logic and with a higher focus on readability. Therefor, the central aspect of describing unbounded state changes incorporates the concept of modifies lists for expressing the modifiable portion of the state space. The underlying deductions are carried out by the theorem prover of the KeY System.
Reports

Brandon Bohrer, Manuel Fernández and André Platzer.
dL_{ɩ}: Definite Descriptions in Differential Dynamic Logic.
School of Computer Science, Carnegie Mellon University, CMUCS19111, 2019.
[bib  ✂  pdf  CADE]We introduce dL_{ɩ}, which extends differential dynamic logic (dL) for hybrid systems with definite descriptions and tuples, thus enabling its theoretical foundations to catch up with its implementation in the theorem prover KeYmaera X. Definite descriptions enable partial, nondifferentiable, and discontinuous terms, which have many examples in applications, such as divisions, nth roots, and absolute values. Tuples enable systems of multiple differential equations, arising in almost every application. Together, definite description and tuples combine to support longdesired features such as vector arithmetic.
We overcome the unique challenges posed by extending dL with these features. Unlike in dL, definite descriptions enable nonlocallyLipschitz terms, so our differential equation (ODE) axioms now make their continuity requirements explicit. Tuples are simple when considered in isolation, but in the context of hybrid systems they demand that differentials are treated in full generality. The addition of definite descriptions also makes dL_{ɩ} a free logic; we investigate the interaction of free logic and the ODEs of dL, showing that this combination is sound, and characterize its expressivity. We give an example system that can be defined and verified using these extensions.
Keywords: Dynamic logic • Definite description • Hybrid systems • Theorem proving • Uniform substitution • Partial functions

Brandon Bohrer and André Platzer.
A Hybrid, Dynamic Logic for HybridDynamic Information Flow.
School of Computer Science, Carnegie Mellon University, CMUCS18105, 2018.
[bib  ✂  pdf  LICS'18]Informationflow security is important to the safety and privacy of cyberphysical systems (CPSs) across many domains: information leakage can both violate user privacy and provide information that supports further attacks. CPSs face the challenge that information can flow both in discrete cyber channels and in continuous realvalued physical channels ranging from time to physical flow of resources. We call these hybrid information flows and introduce dHL, the first logic for verifying these flows in hybriddynamical models of CPSs. We achieve verification of hybrid information flows by extending differential dynamic logic (dL) for hybriddynamical systems with hybridlogical features for explicit representation and relation of program states. By verifying hybrid information flows, we ensure security even under a strong attacker model wherein an attacker can observe time and physical values continuously. We present a Hilbertstyle proof calculus for dHL, prove it sound, and compare the expressive power of dHL with dL. We demonstrate dHL's abilities by developing a hybrid system model of the smart electrical grid FREEDM. We verify that the naive model has a previouslyunknown information flow vulnerability and verify that a revised model resolves the vulnerability. To the best of our knowledge, this is both the first information flow proof for hybrid information flows and the first for a hybriddynamical model. We discuss applications of hybrid information flow to a range of critical systems.
Keywords: Dynamic logic • Hybrid logic • Hybrid systems • Information flow • Cyberphysical systems • Formal verification • Smart grid

André Platzer and Yong Kiam Tan.
How to Prove "All" Differential Equation Properties.
School of Computer Science, Carnegie Mellon University, CMUCS17117, 2017. Extended version arXiv:1802.01226
[bib  ✂  pdf  arXiv  LICS'18]We prove the completeness of an axiomatization for differential equation invariants. First, we show that the differential equation axioms in differential dynamic logic are complete for all algebraic invariants. Our proof exploits differential ghosts, which introduce additional variables that can be chosen to evolve freely along new differential equations. Cleverly chosen differential ghosts are the prooftheoretical counterpart of dark matter. They create new hypothetical state, whose relationship to the original state variables satisfies invariants that did not exist before. The reflection of these new invariants in the original system enables its analysis.
We then show that extending the axiomatization with existence and uniqueness axioms makes it complete for all local progress properties, and further extension with a real induction axiom makes it complete for all real arithmetic invariants. This yields a parsimonious axiomatization, which serves as the logical foundation for reasoning about invariants of differential equations. Moreover, our results are purely axiomatic, and so the axiomatization is suitable for sound implementation in foundational theorem provers.
Keywords: Differential equation axiomatization • Differential dynamic logic • Differential ghosts

Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger and André Platzer.
A Componentbased Approach to Hybrid Systems Safety Verification.
School of Computer Science, Carnegie Mellon University, CMUCS16100, 2016.
[bib  ✂  pdf  IFM'16]We study a componentbased approach to simplify the challenges of verifying largescale hybrid systems. Componentbased modeling can be used to split large models into partial models to reduce modeling complexity. Yet, verification results also need to transfer from components to composites. In this paper, we propose a componentbased hybrid system verification approach that combines the advantages of componentbased modeling (e.g., reduced model complexity) with the advantages of formal verification (e.g., guaranteed contract compliance). Our strategy is to decompose the system into components, verify their local safety individually and compose them to form an overall system that provably satisfies a global contract, without proving the whole system. We introduce the necessary formalism to define the structure and behavior of components and a technique how to compose components such that safety properties provably emerge from component safety.
Keywords: Componentbased development • Hybrid systems • Formal verification

André Platzer.
Differential Hybrid Games.
School of Computer Science, Carnegie Mellon University, CMUCS14102, December 2014. Extended version arXiv:1507.04943.
[bib  ✂  pdf  arXiv  TOCL'17]This paper introduces differential hybrid games, which combine differential games with hybrid games. In both kinds of games, two players interact with continuous dynamics. The difference is that hybrid games also provide all the features of hybrid systems and discrete games, but only deterministic differential equations. Differential games, instead, provide differential equations with input by both players, but not the luxury of hybrid games, such as mode switches and discrete or alternating interaction. This paper augments differential game logic with modalities for the combined dynamics of differential hybrid games. It shows how hybrid games subsume differential games and introduces differential game invariants and differential game variants for proving properties of differential games inductively.
Keywords: differential games • hybrid games • differential game game logic • differential game invariants • partial differential equations • viscosity solutions • real algebraic geometry

JeanBaptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki, and André Platzer.
A Formally Verified Hybrid System for the NextGeneration Airborne Collision Avoidance System.
School of Computer Science, Carnegie Mellon University, CMUCS14138, 2014.
[bib  ✂  pdf  study  TACAS'15]The nextgeneration Airborne Collision Avoidance System (ACAS X) is intended to be installed on all large aircraft to give advice to pilots and prevent midair collisions with other aircraft. It is currently being developed by the Federal Aviation Administration (FAA). In this paper we determine the geometric configurations under which the advice given by ACAS X is safe under a precise set of assumptions and formally verify these configurations using hybrid systems theorem proving techniques. We conduct an initial examination of the current version of the real ACAS X system and discuss some cases where our safety theorem conflicts with the actual advisory given by that version, demonstrating how formal, hybrid approaches are helping ensure the safety of ACAS X. Our approach is general and could also be used to identify unsafe advice issued by other collision avoidance systems or confirm their safety.
Keywords: Airborne Collision Avoidance • ACAS X • Hybrid systems • Theorem proving • Federal Aviation Administration • Aircraft • Markov decision processes • Cyberphysical systems

Stefan Mitsch and André Platzer.
ModelPlex: Verified Runtime Validation of Verified Cyberphysical System Models.
School of Computer Science, Carnegie Mellon University, CMUCS14121, 2014.
[bib  ✂  pdf  study  RV'14]Formal verification and validation play a crucial role in making cyberphysical systems (CPS) safe. Formal methods make strong guarantees about the system behavior if accurate models of the system can be obtained, including models of the controller and of the physical dynamics. In CPS, models are essential; but any model we could possibly build necessarily deviates from the real world. If the real system fits to the model, its behavior is guaranteed to satisfy the correctness properties verified w.r.t. the model. Otherwise, all bets are off. This paper introduces ModelPlex, a method ensuring that verification results about models apply to CPS implementations. ModelPlex provides correctness guarantees for CPS executions at runtime: it combines offline verification of CPS models with runtime validation of system executions for compliance with the model. ModelPlex ensures that the verification results obtained for the model apply to the actual system runs by monitoring the behavior of the world for compliance with the model, assuming the system dynamics deviation is bounded. If, at some point, the observed behavior no longer complies with the model so that offline verification results no longer apply, ModelPlex initiates provably safe fallback actions. This paper, furthermore, develops a systematic technique to synthesize provably correct monitors automatically from CPS proofs in differential dynamic logic.
Keywords: Runtime verification • Cyberphysical systems • Hybrid systems • Logic

Khalil Ghorbal and André Platzer.
Characterizing Algebraic Invariants by Differential Radical Invariants.
School of Computer Science, Carnegie Mellon University, CMUCS13129, 2013.
[bib  ✂  pdf  TACAS'14]We prove that any invariant algebraic set of a given polynomial vector field can be algebraically represented by one polynomial and a finite set of its successive Lie derivatives. This socalled differential radical characterization relies on a sound abstraction of the reachable set of solutions by the smallest variety that contains it. The characterization leads to a differential radical invariant proof rule that is sound and complete, which implies that invariance of algebraic equations over realclosed fields is decidable. Furthermore, the problem of generating invariant varieties is shown to be as hard as minimizing the rank of a symbolic matrix, and is therefore NPhard. We investigate symbolic linear algebra tools based on Gaussian elimination to efficiently automate the generation. The approach can, e.g., generate nontrivial algebraic invariant equations capturing the airplane behavior during takeoff or landing in longitudinal motion.
Keywords: Algebraic invariants • Differential ideals • Higherorder Lie derivation • Differential invariants • Differential equations • Invariant generation

Erik Zawadzki, André Platzer, and Geoffrey J. Gordon.
A Generalization of SAT and #SAT for Robust Policy Evaluation.
School of Computer Science, Carnegie Mellon University, CMUCS13107, 2013.
[bib  ✂  pdf  IJCAI'13]Both SAT and #SAT can represent difficult problems in seemingly dissimilar areas such as planning, verification, and probabilistic inference. Here, we examine an expressive new language, #∃SAT, that generalizes both of these languages. #∃SAT problems require counting the number of satisfiable formulas in a conciselydescribable set of existentially quantified, propositional formulas. We characterize the expressiveness and worstcase difficulty of #∃SAT by proving it is complete for the complexity class #PNP[1], and relating this class to more familiar complexity classes. We also experiment with three new generalpurpose #∃SAT solvers on a battery of problem distributions including a simple logistics domain. Our experiments show that, despite the formidable worstcase complexity of #PNP[1], many of the instances can be solved efficiently by noticing and exploiting a particular type of frequent structure.
Keywords: Satisfiablity • Counting • #SAT • Policy evaluation • Quantifier alternation

Yanni Kouskoulas, André Platzer and Peter Kazanzides.
Formal Methods for Robotic System Control Software.
Johns Hopkins APL Technical Digest 32(2), pp. 490498, 2013.
[bib  ✂  pdf]Creating software for controlling robotic machinery has unique challenges. This article describes a formal method called differentialdynamic logic (dL) that can help produce zerodefect algorithms for robotic systems. We take the reader through an example of applying dL to a version of a control algorithm used in an experimental surgical robot. This case study is a simplified variant of an existing control algorithm. It shows how this tool can be useful and illustrates general principles that readers can use when applying this technique to other systems. We describe how to model a control algorithm for the robot and are able to prove that it safely enforces tool movement for a single boundary. Our proof provides a guarantee of the control algorithm’s safe behavior for all possible inputs and is far more comprehensive than what is possible by using testing alone.
Keywords: medical robotics • formal verification • differential dynamic logic

André Platzer.
A Complete Axiomatization of Differential Game Logic for Hybrid Games.
School of Computer Science, Carnegie Mellon University, CMUCS13100R, January 2013, extended in revised version from July 2013. Extended version arXiv:1408.1980.
[bib  ✂  pdf  slides  arXiv  TOCL'15]Differential game logic (dGL) is a logic for specifying and verifying properties of hybrid games, i.e. games that combine discrete, continuous, and adversarial dynamics. Unlike hybrid systems, hybrid games allow choices in the system dynamics to be resolved adversarially by different players with different objectives. The logic dGL can be used to study the existence of winning strategies for such hybrid games, i.e. ways of resolving the player's choices in some way so that he wins by achieving his objective for all choices of the opponent. Hybrid games are determined, i.e. one player has a winning strategy from each state, yet their winning regions may require transfinite closure ordinals. The logic dGL, nevertheless, has a sound and complete axiomatization relative to any expressive logic. Separating axioms are identified that distinguish hybrid games from hybrid systems. Finally, dGL is proved to be strictly more expressive than the corresponding logic of hybrid systems.
Keywords: game logic • hybrid dynamical systems • hybrid games • axiomatization

David Renshaw, Sarah M. Loos and André Platzer.
Mechanized Safety Proofs for DiscConstrained Aircraft.
School of Computer Science, Carnegie Mellon University, CMUCS12132, August 2012.
[bib  ✂  pdf  HSCC'13]As airspace becomes ever more crowded, air traffic management must reduce both space and time between aircraft to increase throughput, and onboard collision avoidance systems become ever more important. These systems and the policies that they implement must be extremely reliable. In this paper we consider implementations of distributed collision avoidance policies designed to work in environments with arbitrarily many aircraft. We formally verify that the policies are safe, even when new planes approach an inprogress avoidance maneuver. We show that the policies are flyable and that in every circumstance which may arise from a set of controllable initial conditions, the aircraft will never get too close to one another. Our approach relies on theorem proving in Quantified Differential Dynamic Logic (QdL) and the KeYmaeraD theorem prover for distributed hybrid systems. It represents an important step in formally verified, flyable, and distributed air traffic control.
Keywords: aircraft maneuvers • distributed hybrid systems • differential dynamic logic • theorem proving • formal verification

André Platzer.
Differential Game Logic for Hybrid Games.
School of Computer Science, Carnegie Mellon University, CMUCS12105, March 2012.
Also see new results.
[bib  ✂  pdf  TOCL'15]We introduce differential game logic (dGL) for specifying and verifying properties of hybrid games, i.e., determined, sequential/dynamic, noncooperative, zerosum games of perfect information on hybrid systems that combine discrete and continuous dynamics. Unlike hybrid systems, hybrid games allow choices in the system dynamics to be resolved by different players with different objectives. The logic dGL can be used to study properties of the resulting adversarial behavior. It unifies differential dynamic logic for hybrid systems with game logic. We define a regular modal semantics for dGL, present a proof calculus for dGL, and prove soundness. We identify separating axioms, i.e., the axioms that distinguish dGL and its game aspects from logics for hybrid systems. We also define an operational game semantics, prove equivalence, and prove determinacy.
Keywords: dynamic logic • game logic • hybrid games • hybrid dynamical systems • proof calculus

André Platzer.
The Complete Proof Theory of Hybrid Systems.
School of Computer Science, Carnegie Mellon University, CMUCS11144, November 2011.
[bib  ✂  pdf  LICS'12]Hybrid systems are a fusion of continuous dynamical systems and discrete dynamical systems. They freely combine dynamical features from both worlds. For that reason, it has often been claimed that hybrid systems are more challenging than continuous dynamical systems and than discrete systems. We now show that, prooftheoretically, this is not the case. We present a complete prooftheoretical alignment that interreduces the discrete dynamics and the continuous dynamics of hybrid systems. We give a sound and complete axiomatization of hybrid systems relative to continuous dynamical systems and a sound and complete axiomatization of hybrid systems relative to discrete dynamical systems. Thanks to our axiomatization, proving properties of hybrid systems is exactly the same as proving properties of continuous dynamical systems and again, exactly the same as proving properties of discrete dynamical 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.
Keywords: proof theory • hybrid dynamical systems • differential dynamic logic • axiomatization • completeness

David W. Renshaw and André Platzer.
Differential Invariants and Symbolic Integration for Distributed Hybrid Systems.
School of Computer Science, Carnegie Mellon University, CMUCS12107, May 2012.
[bib  ✂  pdf]

André Platzer.
The Structure of Differential Invariants and Differential Cut Elimination.
School of Computer Science, Carnegie Mellon University, CMUCS11112, April 2011.
[bib  ✂  pdf  arXiv  LMCS'12]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

André Platzer.
Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs.
School of Computer Science, Carnegie Mellon University, CMUCS11111, 2011.
[bib  ✂  pdf  CADE]Logic is a powerful tool for analyzing and verifying systems, including programs, discrete systems, realtime systems, hybrid systems, and distributed systems. Some applications also have a stochastic behavior, however, either because of fundamental properties of nature, uncertain environments, or simplifications to overcome complexity. Discrete probabilistic systems have been studied using logic. But logic has been chronically underdeveloped in the context of stochastic hybrid systems, i.e., systems with interacting discrete, continuous, and stochastic dynamics. We aim at overcoming this deficiency and introduce a dynamic logic for stochastic hybrid systems. Our results indicate that logic is a promising tool for understanding stochastic hybrid systems and can help taming some of their complexity. We introduce a compositional model for stochastic hybrid systems. We prove adaptivity, cadlag, and Markov time properties, and prove that the semantics of our logic is measurable. We present compositional proof rules, including rules for stochastic differential equations, and prove soundness.
Keywords: dynamic logic • proof calculus • stochastic differential equations • stochastic hybrid systems • stochastic processes

Sarah M. Loos, André Platzer and Ligia Nistor.
Adaptive Cruise Control:
Hybrid, Distributed, and Now Formally Verified.
School of Computer Science, Carnegie Mellon University, CMUCS11107, 2011.
[bib  ✂  pdf  FM'10]Car safety measures can be most effective when the cars on a street coordinate their control actions using distributed cooperative control. While each car optimizes its navigation planning locally to ensure the driver reaches his destination, all cars coordinate their actions in a distributed way in order to minimize the risk of safety hazards and collisions. These systems control the physical aspects of car movement using cyber technologies like local and remote sensor data and distributed V2V and V2I communication. They are thus cyberphysical systems. In this paper, we consider a distributed car control system that is inspired by the ambitions of the California PATH project, the CICAS system, SAFESPOT and PReVENT initiatives. We develop a formal model of a distributed car control system in which every car is controlled by adaptive cruise control. One of the major technical difficulties is that faithful models of distributed car control have both distributed systems and hybrid systems dynamics. They form distributed hybrid systems, which makes them very challenging for verification. In a formal proof system, we verify that the control model satisfies its main safety objective and guarantees collision freedom for arbitrarily many cars driving on a street, even if new cars enter the lane from onramps or multilane streets. The system we present is in many ways one of the most complicated cyberphysical systems that has ever been fully verified formally.
Keywords: distributed car control • multiagent systems • highway traffic safety • formal verification • distributed hybrid systems • adaptive cruise control

André Platzer.
Quantified Differential Dynamic Logic for Distributed Hybrid Systems.
School of Computer Science, Carnegie Mellon University, CMUCS10126, 2010.
[bib  ✂  pdf  CSL'10]We address a fundamental mismatch between the combinations of dynamics that occur in complex physical systems and the limited kinds of dynamics supported in analysis. Modern applications combine communication, computation, and control. They may even form dynamic networks, where neither structure nor dimension stay the same while the system follows mixed discrete and continuous dynamics.
We provide the logical foundations for closing this analytic gap. We develop a system model for distributed hybrid systems that combines quantified differential equations with quantified assignments and dynamic dimensionalitychanges. We introduce a dynamic logic for verifying distributed hybrid systems and present a proof calculus for it. We prove that this calculus is a sound and complete axiomatization of the behavior of distributed hybrid systems relative to quantified differential equations. In our calculus we have proven collision freedom in distributed car control even when new cars may appear dynamically on the road.
Keywords: Dynamic logic • Distributed hybrid systems • Axiomatization • Theorem proving • Quantified differential equations

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, CMUCS10100, 2010.
[bib  ✂  pdf  HSCC'10]We address the problem of model checking stochastic systems, i.e. checking whether a stochastic system satisfies a certain temporal property with a probability greater (or smaller) than a fixed threshold. In particular, we present a novel Statistical Model Checking (SMC) approach based on Bayesian statistics. We show that our approach is feasible for hybrid systems with stochastic transitions, a generalization of Simulink/Stateflow models. Standard approaches to stochastic (discrete) systems require numerical solutions for large optimization problems and quickly become infeasible with larger state spaces. Generalizations of these techniques to hybrid systems with stochastic effects are even more challenging. The SMC approach was pioneered by Younes and Simmons in the discrete and nonBayesian case. It solves the verification problem by combining randomized sampling of system traces (which is very efficient for Simulink/Stateflow) with hypothesis testing or estimation. We believe SMC is essential for scaling up to large Stateflow/Simulink models. While the answer to the verification problem is not guaranteed to be correct, we prove that Bayesian SMC can make the probability of giving a wrong answer arbitrarily small. The advantage is that answers can usually be obtained much faster than with standard, exhaustive model checking techniques. We apply our Bayesian SMC approach to a representative example of stochastic discretetime hybrid system models in Stateflow/Simulink: a fuel control system featuring hybrid behavior and fault tolerance. We show that our technique enables faster verification than stateoftheart statistical techniques, while retaining the same error bounds. We emphasize that Bayesian SMC is by no means restricted to Stateflow/Simulink models: we have in fact successfully applied it to very large stochastic models from Systems Biology.

André Platzer and JanDavid Quesel.
European Train Control System: A Case Study in Formal Verification.
Reports of SFB/TR 14 AVACS 54, 2009. ISSN: 18609821, www.avacs.org.
[bib  ✂  pdf  ICFEM'09]Complex physical systems have several degrees of freedom. They only work correctly when their control parameters obey corresponding constraints. Based on the informal specification of the European Train Control System (ETCS), we design a controller for its cooperation protocol. For its free parameters, we successively identify constraints that are required to ensure collision freedom. We formally prove the parameter constraints to be sharp by characterizing them equivalently in terms of reachability properties of the hybrid system dynamics. Using our deductive verification tool KeYmaera, we formally verify controllability, safety, liveness, and reactivity properties of the ETCS protocol that entail collision freedom. We prove that the ETCS protocol remains correct even in the presence of perturbation by disturbances in the dynamics. We verify that safety is preserved when a PI controlled speed supervision is used.
Keywords: formal verification of hybrid systems • train control • theorem proving • parameter constraint identification • disturbances

André Platzer and Edmund M. Clarke.
Formal Verification of Curved Flight Collision Avoidance Maneuvers: A Case Study.
School of Computer Science, Carnegie Mellon University, CMUCS09147, 2009.
[bib  ✂  pdf  FM'09]Aircraft collision avoidance maneuvers are important and complex applications. Curved flight exhibits nontrivial continuous behavior. In combination with the control choices during air traffic maneuvers, this yields hybrid systems with challenging interactions of discrete and continuous dynamics. As a case study illustrating the use of a new proof assistant for a logic for nonlinear hybrid systems, we analyze collision freedom of roundabout maneuvers in air traffic control, where appropriate curved flight, good timing, and compatible maneuvering are crucial for guaranteeing safe spatial separation of aircraft throughout their flight. We show that formal verification of hybrid systems can scale to curved flight maneuvers required in aircraft control applications. We introduce a fully flyable variant of the roundabout collision avoidance maneuver and verify safety properties by compositional verification.
Keywords: formal verification of hybrid systems • deduction • air traffic control • logic for hybrid systems

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, CMUCS09110, 2009.
[bib  ✂  pdf  CMSB'09]Recently, there has been considerable interest in the use of Model Checking for Systems Biology. Unfortunately, the state space of stochastic biological models is often too large for classical Model Checking techniques. For these models, a statistical approach to Model Checking has been shown to be an effective alternative. Extending our earlier work, we present the first algorithm for performing statistical Model Checking using Bayesian Sequential Hypothesis Testing. We show that our Bayesian approach outperforms current statistical Model Checking techniques, which rely on tests from Classical (aka Frequentist) statistics, by requiring fewer system simulations. Another advantage of our approach is the ability to incorporate prior Biological knowledge about the model being verified. We demonstrate our algorithm on a variety of models from the Systems Biology literature and show that it enables faster verification than stateoftheart techniques, even when no prior knowledge is available.

André Platzer, JanDavid Quesel and Philipp Rümmer.
Real World Verification.
Reports of SFB/TR 14 AVACS 52, 2009. ISSN: 18609821, www.avacs.org.
[bib  ✂  pdf  CADE]Scalable handling of real arithmetic is a crucial part of the verification of hybrid systems, mathematical algorithms, and mixed analog/digital circuits. Despite substantial advances in verification technology, complexity issues with classical decision procedures are still a major obstacle for formal verification of realworld applications, e.g., in automotive and avionic industries. To identify strengths and weaknesses, we examine state of the art symbolic techniques and implementations for the universal fragment of realclosed fields: approaches based on quantifier elimination, Gröbner Bases, and semidefinite programming for the Positivstellensatz. Within a uniform context of the verification tool KeYmaera, we compare these approaches qualitatively and quantitatively on verification benchmarks from hybrid systems, textbook algorithms, and on geometric problems. Finally, we introduce a new decision procedure combining Gröbner Bases and semidefinite programming for the real Nullstellensatz that outperforms the individual approaches on an interesting set of problems.
Keywords: realclosed fields • decision procedures • hybrid systems • software verification

Edmund M. Clarke, Bruce Krogh, André Platzer and Raj Rajkumar.
Analysis and verification challenges for cyberphysical transportation systems.
In NITRD National Workshop for Research on Transportation CyberPhysical Systems: Automotive, Aviation, and Rail, 2008.
Position paper.
[bib  ✂  pdf]Substantial technological and engineering advances in various disciplines make it possible more than ever before to provide autonomous control choices for cars, trains, and aircraft. Correct automatic control can improve overall safety tremendously. Yet, ensuring a safe operation of those control assistants under all circumstances requires analysis techniques that are prepared for the rising complexity resulting from combinations of several computerized safety measures. We identify cases where cyberphysical transportation systems pose particularly demanding challenges for future research in formal analysis techniques.

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]We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations whose righthand sides are polynomials in the state variables. In order to verify nontrivial systems without solving their differential equations and without numerical errors, we use a continuous generalization of induction, for which our algorithm computes the required differential invariants. As a means for combining local differential invariants into global system invariants in a sound way, our fixedpoint algorithm works with a compositional verification logic for hybrid systems. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively with differential invariants until safety becomes provable. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification procedure. We verify roundabout maneuvers in air traffic management and collision avoidance in train control.
Keywords: verification of hybrid systems • differential invariants • verification logic • fixedpoint engine

André Platzer.
Differential Dynamic Logic for Verifying Parametric Hybrid Systems.
Reports of SFB/TR 14 AVACS 15, May 2007. ISSN: 18609821, www.avacs.org.
[bib  ✂  pdf  TABLEAUX'07]We introduce a firstorder dynamic logic for reasoning about systems with discrete and continuous state transitions, and we present a sequent calculus for this logic. As a uniform model, our logic supports hybrid programs with discrete and differential actions. For handling real arithmetic during proofs, we lift quantifier elimination to dynamic logic. To obtain a modular combination, we use side deductions for verifying interacting dynamics. With this, our logic supports deductive verification of hybrid systems with symbolic parameters and firstorder definable flows. Using our calculus, we prove a parametric inductive safety constraint for speed supervision in a train control system.
Keywords: dynamic logic • sequent calculus • verification of parametric hybrid systems • quantifier elimination

André Platzer.
A Temporal Dynamic Logic for Verifying Hybrid System Invariants.
Reports of SFB/TR 14 AVACS 12, February 2007. ISSN: 18609821, www.avacs.org.
[bib  ✂  pdf  LFCS'07]We combine firstorder dynamic logic for reasoning about possible behaviour of hybrid systems with temporal logic for reasoning about the temporal behaviour during their operation. Our logic supports verification of hybrid programs with firstorder definable flows and provides a uniform treatment of discrete and continuous evolution. For our combined logic, we generalise the semantics of dynamic modalities to refer to hybrid traces instead of final states. Further, we prove that this gives a conservative extension of dynamic logic. On this basis, we provide a modular verification calculus that reduces correctness of temporal behaviour of hybrid systems to nontemporal reasoning. Using this calculus, we analyse safety invariants in a train control system and symbolically synthesise parametric safety constraints.
Keywords: dynamic logic • temporal logic • sequent calculus • logic for hybrid systems • deductive verification of embedded systems
Other

Stefan Mitsch and André Platzer.
Verified Runtime Validation for Partially Observable Hybrid Systems.
arXiv:1811.06502, November 2018.
[bib  ✂  pdf  arXiv]Formal verification provides strong safety guarantees about models of cyberphysical systems. Hybrid system models describe the required interplay of computation and physical dynamics, which is crucial to guarantee what computations lead to safe physical behavior (e.g., cars should not collide). Control computations that affect physical dynamics must act in advance to avoid possibly unsafe future circumstances. Formal verification then ensures that the controllers correctly identify and provably avoid unsafe future situations under a certain model of physics. But any model of physics necessarily deviates from reality and, moreover, any observation with real sensors and manipulation with real actuators is subject to uncertainty. This makes runtime validation a crucial step to monitor whether the model assumptions hold for the real system implementation.
The key question is what property needs to be runtimemonitored and what a satisfied runtime monitor entails about the safety of the system: the observations of a runtime monitor only relate back to the safety of the system if they are themselves accompanied by a proof of correctness. For an unbroken chain of correctness guarantees, we, thus, synthesize runtime monitors in a provably correct way from provably safe hybrid system models. This paper advances these techniques to make the synthesized monitoring conditions robust to partial observability of sensor uncertainty and partial controllability due to actuator disturbance. We show that the monitoring conditions result in provable safety guarantees with fallback controllers that react to monitor violation at runtime.
Keywords: Hybrid systems • Cyberphysical systems • Formal verification • Runtime model validation • Monitor synthesis • Differential dynamic logic

Sarah M. Loos and André Platzer.
Teaching CyberPhysical Systems with Logic.
Draft, 2014.
[bib  ✂  pdf  course]This paper reports on a course breaking with the myth that cyberphysical systems are too challenging to be taught at the undergraduate level. Cyberphysical systems (CPSs) such as computercontrolled cars, airplanes or robots play an increasingly crucial role in our daily lives. They are systems that we bet our lives on, so they need to be safe. Getting CPSs safe, however, is an intellectual challenge, because of their intricate interactions of complex control software with their physical behavior. Who can design these notoriously challenging systems with the scrutiny that is required to make sure they can be used safely? How can students, scientists, and practitioners acquire the required background in logic as well as in discrete and continuous mathematics and control in a single course in a way that meets the demands on rigor required in safe CPS design? This paper reports on the experience with a new undergraduate course, Foundations of CyberPhysical Systems, that teaches students how to design a correct CPS, identify required safety properties, and justify that their designs meet these safety goals.
Keywords: Cyberphysical systems • Education • Hybrid systems • Using theorem provers in education • Differential dynamic logic

André Platzer.
Dynamic logics of dynamical systems.
arXiv:1205.4788, May 2012. Long version of LICS'12 invited tutorial.
[bib  ✂  pdf  arXiv  LICS'12]We survey dynamic logics for specifying and verifying properties of dynamical systems, including hybrid systems, distributed hybrid systems, and stochastic hybrid systems. A dynamic logic is a firstorder modal logic with a pair of parametrized modal operators for each dynamical system to express necessary or possible properties of their transition behavior. Due to their full basis of firstorder modal logic operators, dynamic logics can express a rich variety of system properties, including safety, controllability, reactivity, liveness, and quantified parametrized properties, even about relations between multiple dynamical systems. In this survey, we focus on some of the representatives of the family of differential dynamic logics, which share the ability to express properties of dynamical systems having continuous dynamics described by various forms of differential equations.
We explain the dynamical system models, dynamic logics of dynamical systems, their semantics, their axiomatizations, and proof calculi for proving logical formulas about these dynamical systems. We study differential invariants, i.e., induction principles for differential equations. We survey theoretical results, including soundness and completeness and deductive power. Differential dynamic logics have been implemented in automatic and interactive theorem provers and have been used successfully to verify safetycritical applications in automotive, aviation, railway, robotics, and analogue electrical circuits.
Keywords: Logic of dynamical systems • dynamic logic • differential dynamic logic • hybrid systems • distributed hybrid systems • stochastic hybrid systems • axiomatization • deduction
Video Productions

André Platzer.
Videos for Logical Foundations of CyberPhysical Systems.
YouTube 20182019. Videos for 22 lectures of about an hour each.
[bib  ✂  video  Textbook]Cyberphysical systems (CPSs) combine cyber capabilities, such as computation or communication, with physical capabilities, such as motion or other physical processes. Cars, aircraft, and robots are prime examples, because they move physically in space in a way that is determined by discrete computerized control algorithms. Designing these algorithms is challenging due to their tight coupling with physical behavior, while it is vital that these algorithms be correct because we rely on them for safetycritical tasks.
These videos teach undergraduate students the core principles behind CPSs. They show them how to develop models and controls; identify safety specifications and critical properties; reason rigorously about CPS models; leverage multidynamical systems compositionality to tame CPS complexity; verify CPS models of appropriate scale in logic; and develop an intuition for operational effects.
The videos are for an accompanying textbook.