Publications by André Platzer (with abstracts)

Table of Contents
List of Publications Textbooks Books Book Chapters Journal Publications Conference Publications Short & Tool Publications Workshop Publications Invited Papers Theses Video Productions Reports Other

List of Publications

[ORCID | DBLP | Google Scholar | by year | by area | abstracts | guide]

Textbooks

André Platzer. Logical Foundations of Cyber-Physical Systems. Springer, Cham, 2018. 659 pages. ISBN 978-3-319-63587-3. [bib | ⧉ | doi | slides | video | book | web | errata] Cyber-physical 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 safety-critical tasks. This textbook teaches undergraduate students the core principles behind CPSs. It shows them how to develop models and controls; identify safety specifications and critical properties; reason rigorously about CPS models; leverage multi-dynamical systems compositionality to tame CPS complexity; verify CPS models of appropriate scale in logic; and develop an intuition for operational effects. The book is supported with homework exercises, lecture videos, and slides.

Books

André Platzer. Logical Analysis of Hybrid Systems:    Proving Theorems for Complex Dynamics. Springer, Heidelberg, 2010. 426 pages. ISBN 978-3-642-14508-7. [bib | ⧉ | doi | book | web | errata] Hybrid systems are models for complex physical systems and have become a widely used concept for understanding their behaviour. Many applications are safety-critical, including car, railway, and air traffic control, robotics, physical-chemical 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. This is the first book that leverages the power of logic for hybrid systems. The author develops a coherent logical approach for systematic hybrid systems analysis, covering its theory, practice, and applications. It is further shown how the developed verification techniques can be used to study air traffic and railway control systems. This book is intended for researchers, postgraduates, and professionals who are interested in hybrid systems analysis, cyber-physical or embedded systems design, logic and theorem proving, or transportation and automation.

Book Chapters

1. Stefan Mitsch and André Platzer.
   A retrospective on developing hybrid system provers in the KeYmaera family:
      A tale of three provers.
   In Wolfgang Ahrendt et al., editors, Deductive Software Verification: Future Perspectives, volume 12345 of LNCS, pp. 21-64. Springer, 2020. © Springer
   [bib | ⧉ | pdf | doi]

   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

   
   
   
2. André Platzer.
   Overview of logical foundations of cyber-physical systems.
   In Helmut Seidl, editor, Post-proceedings of the Summer School Marktoberdorf: Safety and Security of Software Systems - Logics, Proofs, Applications, TUM University Press, 2020. © The author
   [bib | ⧉ | pdf | eprint | arXiv]

   Cyber-physical systems (CPSs) are important whenever computer technology interfaces with the physical world as it does in self-driving cars or aircraft control support systems. Due to their many subtleties, controllers for cyber-physical 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 next-generation 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 Cyber-Physical Systems. It also explains how safety guarantees obtained in the land of verified models reach the level of CPS execution unharmed.

   Keywords: Cyber-physical systems • Differential dynamic logic • Hybrid systems • Theorem proving • Formal verification

   
   
   
3. 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. 1047-1110. Springer, 2018. © Springer
   [bib | ⧉ | pdf | doi | book]

   Hybrid systems are models with joint discrete and continuous behavior. They occur frequently in safety-critical 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 model-checking is in general undecidable, we present three complementary analysis approaches based on symbolic representations, abstraction, and logic. In particular, we illustrate polyhedron-based reachability analysis, finite quotients, abstraction refinement techniques, and logic-based verification. We survey important tools and application domains of successful hybrid system verification in this vibrant area of research.

   
   
   

Journal Publications

1. Manfred Broy, Achim Brucker, Alessandro Fantechi, Mario Gleirscher, Klaus Havelund, Markus Alexander Kuppe, Alexandra Mendes, André Platzer, Jan Ringert and Allison Sullivan.
   Does every computer scientist need to know formal methods?.
   Form. Asp. Comput. To appear © The authors
   [bib | ⧉ | doi]

   We focus on the integration of Formal Methods as mandatory theme in any Computer Science University curriculum. In particular, when considering the ACM Curriculum for Computer Science, the inclusion of Formal Methods as a mandatory Knowledge Area needs arguing for why and how does every computer science graduate benefit from such knowledge. We do not agree with the sentence “While there is a belief that formal methods are important and they are growing in importance, we cannot state that every computer science graduate will need to use formal methods in their career.” We argue that formal methods are and have to be an integral part of every computer science curriculum. Just as not all graduates will need to know how to work with databases either, it is still important for students to have a basic understanding of how data is stored and managed efficiently. The same way, students have to understand why and how methods work, what their formal background is, and how they are justified. No engineer should be ignorant of the foundations of their subject and the formal methods based on these.In this paper, we aim to highlight why every computer scientist needs to be familiar with formal methods. We argue that education in formal methods plays a key role by shaping students' programming mindset, fostering an appreciation for underlying principles, and encouraging the practice of thoughtful program design and justification, rather than simply writing programs without reflection and deeper understanding. Since integrating formal methods into the computer science curriculum is not a straightforward process, we explore the additional question: what are the trade-offs between one dedicated knowledge area of formal methods in a computer science curriculum versus having formal methods scattered across all knowledge areas? Solving problems while designing software and software-intensive systems demands an understanding of what is required, followed by a specification and formalizing a solution in a programming language. How to do this systematically and correctly on solid grounds is exactly the supported by Formal Methods.

   Keywords: Formal methods • Software and systems engineering • Computer science university curriculum

   
   
   
2. André Platzer.
   Hybrid dynamical systems logic and its refinements.
   Sci. Comput. Program. 239, pp. 103179, 2025. © The authors
   [bib | ⧉ | doi | mypdf]

   Hybrid dynamical systems describe the mixed discrete dynamics and continuous dynamics of cyber-physical systems such as aircraft, cars, trains, and robots. To justify correctness properties of the safety-critical control algorithms for their physical models, differential dynamic logic (dL) provides deductive specification and verification techniques implemented in the theorem prover KeYmaera X. The logic dL is useful for proving, e.g., that all runs of a hybrid dynamical system α satisfy safety property φ (i.e., [α]φ), or that there is a run of the hybrid dynamical system α ultimately reaching the desired goal φ (i.e., ⟨α⟩φ). Logical combinations of dL’s operators naturally represent safety, liveness, stability and other properties. Variations of dL serve additional purposes. Differential refinement logic (dRL) adds an operator α ≤ β expressing that hybrid system α refines hybrid system β, which is useful, e.g., for relating concrete system implementations α to their abstract verification models β. Just like dL, dRL is a logic closed under all operators, which opens up systematic ways of simultaneously relating systems and their properties, of reducing system properties to system relations or, vice versa, reducing system relations to system properties. A second variant of dL, differential game logic (dGL), adds the ability of referring to winning strategies of players in hybrid games, which is useful for establishing correctness properties where the actions of different agents may interfere either because they literally compete with one another or because they may interact accidentally. In the theorem prover KeYmaera X, dL and its variations have been used for verifying ground robot obstacle avoidance, the Federal Aviation Administration’s Next-Generation Airborne Collision Avoidance System ACAS X, and the Federal Railroad Administration’s train control model.

   Keywords: Differential dynamic logic • Differential refinement logic • Differential game logic • Hybrid systems • Hybrid games • Theorem proving

   
   
   
3. Aditi Kabra, Stefan Mitsch and André Platzer.
   Verified train controllers for the Federal Railroad Administration train kinematics model: Balancing competing brake and track forces.
   IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 41(11), pp. 4409-4420, 2022. Special issue for EMSOFT 2022. © IEEE
   Best paper finalist
   [bib | ⧉ | pdf | doi | slides | video | kyx | extra]

   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

   
   
   
4. Rachel Cleveland, Stefan Mitsch and André Platzer.
   Formally verified next-generation airborne collision avoidance games in ACAS X.
   ACM Trans. Embed. Comput. Syst. 22(1), pp. 10:1-10:30, 2023. © The authors
   [bib | ⧉ | pdf | doi | mypdf | 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 Next-Generation Airborne Collision Avoidance System ACAS X, have been analyzed assuming severe restrictions on the intruder's flight maneuvers, limiting their safety guarantees in real-world 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 first-class 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, collision-freedom 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: single-advisory infinite-time models, bounded time models, and infinite time, multi-advisory 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

   
   
   
5. Qin Lin, Stefan Mitsch, André Platzer and John M. Dolan.
   Safe and resilient practical waypoint-following for autonomous vehicles.
   IEEE Control Syst. Lett. 6, pp. 1574-1579, 2022. © IEEE
   [bib | ⧉ | pdf | doi]

   We combine theorem proving and reachability analysis for cyber-physical systems verification to arrive at a practical approach to safe waypoint-following for an autonomous mobile vehicle controlled by a learning-enabled controller. We propose a robust monitor verifying short-term and long-term safety simultaneously at runtime, thereby combining the benefits of both theorem proving and reachability analysis. The proposed novel monitor architecture allows temporary violation of long-term safety while maintaining short-term safety to recover to a state with long-term safety. The recovery is based on a fallback model predictive controller. The experiments conducted in a high-fidelity 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 • Learning-enabled control

   
   
   
6. Brandon Bohrer and André Platzer.
   Structured proofs for adversarial cyber-physical systems.
   ACM Trans. Embed. Comput. Syst. 20(5s), pp. 93:1-93:26, 2021.
   Special issue on EMSOFT 2021. © The authors
   [bib | ⧉ | pdf | doi | mypdf | arXiv]

   Many cyber-physical systems (CPS) are safety-critical, 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 proof-checking tool.

   We introduce Kaisar, the first language and tool for CdGL proofs, which until now could only be written by hand with a low-level proof calculus. Kaisar's structured proofs simplify challenging CPS proof tasks, especially by using programming language principles and high-level 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: Cyber-physical systems • Hybrid games • Formal proof • Structured proofs

   
   
   
7. Yong Kiam Tan and André Platzer.
   An axiomatic approach to existence and liveness for differential equations.
   Formal Aspects of Computing 33(4), pp. 461-518, 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

   
   
   
8. 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. 5-41, 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

   
   
   
9. André Platzer and Yong Kiam Tan.
   Differential equation invariance axiomatization.
   J. ACM 67(1), 6:1-6:66, 2020. © The authors
   [bib | ⧉ | pdf | doi | mypdf | slides | video | arXiv | LICS'18]

   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 proof-theoretical 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

   
   
   
10. 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. 2910-2917, 2019. © IEEE
    [bib | ⧉ | pdf | doi | kyx | study | arXiv]

    We present a reusable formally verified safety net that provides end-to-end safety and liveness guarantees for 2D waypoint-following of Dubins-type 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 waypoint-following 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 trade-off between compliance and performance.

    Keywords: Theorem proving • Safety verification • Liveness verification • Waypoint navigation • Robot motion control • Hybrid systems

    
    
    
11. Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger and André Platzer.
    Tactical contract composition for hybrid system component verification.
    STTT 20(6), pp. 615-643, 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 component-based modeling (e.g., reduced model complexity) with the advantages of formal verification (e.g., guaranteed contract compliance). Component-based 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 soundness-critical 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: Component-based development • Hybrid systems • Component-based verification

    
    
    
12. Stefan Mitsch, Khalil Ghorbal, David Vogelbacher, and André Platzer.
    Formal verification of obstacle avoidance and navigation of ground robots.
    International Journal of Robotics Research 36(12), pp. 1312-1340, 2017. © The authors
    [bib | ⧉ | pdf | doi | kyx | arXiv]

    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

    
    
    
13. Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Aurora Schmidt, Ryan Gardner, Stefan Mitsch, and André Platzer.
    A formally verified hybrid system for safe advisories in the next-generation airborne collision avoidance system.
    STTT 19(6), pp. 717-741, 2017.
    Special issue for selected papers from TACAS'15. © Springer
    [bib | ⧉ | pdf | doi | kyx | study | TACAS'15]

    The Next-Generation Airborne Collision Avoidance System (ACAS X) is intended to be installed on all large aircraft to give advice to pilots and prevent mid-air 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 • Cyber-physical systems

    
    
    
14. André Platzer.
    Differential hybrid games.
    ACM Trans. Comput. Log. 18(3), pp. 19:1-19: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

    
    
    
15. Khalil Ghorbal, Andrew Sogokon, and André Platzer.
    A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets.
    Computer Languages, Systems & Structures 47(1), pp. 19-43, 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 semi-algebraic 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 trade-off 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

    
    
    
16. André Platzer.
    A complete uniform substitution calculus for differential dynamic logic.
    Journal of Automated Reasoning 59(2), pp. 219-265, 2017. © The author
    [bib | ⧉ | pdf | doi | mypdf | arXiv]

    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 soundness-critical 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 soundness-critical 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 first-class 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

    
    
    
17. Stefan Mitsch and André Platzer.
    ModelPlex: Verified runtime validation of verified cyber-physical system models.
    Formal Methods in System Design 49(1), pp. 33-74. 2016.
    Special issue for selected papers from RV'14. © The authors
    [bib | ⧉ | pdf | doi | mypdf | RV'14]

    Formal verification and validation play a crucial role in making cyber-physical 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 correct-by-construction 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 • Cyber-physical systems • Hybrid systems • Differential dynamic logic

    
    
    
18. Jan-David Quesel, Stefan Mitsch, Sarah Loos, Nikos Aréchiga, and André Platzer.
    How to model and prove hybrid systems with KeYmaera: A tutorial on safety.
    STTT 18(1), pp. 67-91, 2016. © The authors
    [bib | ⧉ | pdf | doi | mypdf]

    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 real-world 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 cyber-physical 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

    
    
    
19. André Platzer.
    Differential game logic.
    ACM Trans. Comput. Log. 17(1), pp. 1:1-1: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

    
    
    
20. Stefan Mitsch, André Platzer, Werner Retschitzegger and Wieland Schwinger.
    Logic-based modeling approaches for qualitative and hybrid reasoning in dynamic spatial systems.
    ACM Computing Surveys 48(1), pp. 3:1-3:40. 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 medium-term 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 logic-based 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 logic-based 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 • logic-based reasoning • commonsense reasoning • dynamic reasoning • dynamic spatial systems • knowledge representation • hybrid systems

    
    
    
21. Khalil Ghorbal, Jean-Baptiste 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. 702-713. 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 software-intensive systems as a well-founded 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 mid-air 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 industrial-scale applications and our proposals on how to address these issues.

    
    
    
22. Akshay Rajhans, Ajinkya Bhave, Ivan Ruchkin, Bruce H. Krogh, David Garlan, André Platzer and Bradley Schmerl.
    Supporting heterogeneity in cyber-physical systems architectures.
    IEEE Transactions on Automatic Control 59(12), pp. 3178-3193, 2014.
    Special issue on Control of Cyber-Physical Systems. © IEEE
    [bib | ⧉ | pdf | doi]

    Cyber-physical 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, model-based 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 multi-view architecture framework that treats models as views of the underlying system structure and uses structural and semantic mappings to ensure consistency and enable system-level 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.

    
    
    
23. Stefan Mitsch, Grant Olney Passmore and André Platzer.
    Collaborative verification-driven engineering of hybrid systems.
    Mathematics in Computer Science 8(1), pp. 71-97, 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 real-world cyber-physical systems. The key challenge is to ensure their correct functioning w.r.t. safety requirements. Promising techniques to ensure safety seem to be model-driven engineering to develop hybrid systems in a well-defined and traceable manner, and formal verification to prove their correctness. Their combination forms the vision of verification-driven 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 verification-driven 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 large-scale verification tasks.

    Keywords: Formal verification • Hybrid system • Cyber-physical system • Model-driven engineering

    
    
    
24. 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. 338-367, 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 non-Bayesian 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 discrete-time 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 state-of-the-art 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

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

    We address a fundamental mismatch between the combinations of dynamics that occur in cyber-physical 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 dimensionality-changes. 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

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

    The biggest challenge in hybrid systems verification is the handling of differential equations. Because computable closed-form 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 ad-hoc, 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 trade-offs 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

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

    We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations whose right-hand 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

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

    We generalise dynamic logic to a logic for differential-algebraic programs, i.e., discrete programs augmented with first-order differential-algebraic formulas as continuous evolution constraints in addition to first-order 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 differential-algebraic 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

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

    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 real-valued 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 well-suited 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

1. Samuel Teuber, Stefan Mitsch, and André Platzer.
   Provably safe neural network controllers via differential dynamic logic.
   In A. Globerson and L. Mackey and A. Fan and C. Zhang and D. Belgrave and J. Tomczak and U. Paquet, editors, Advances in Neural Information Processing Systems 37 NeurIPS 2024
   [bib | ⧉ | pdf | arXiv]

   While neural networks (NNs) have a large potential as autonomous controllers for Cyber-Physical Systems, verifying the safety of neural network based control systems (NNCSs) poses significant challenges for the practical use of NNs—especially when safety is needed for unbounded time horizons. One reason for this is the intractability of analyzing NNs, ODEs and hybrid systems. To this end, we introduce VerSAILLE (Verifiably Safe AI via Logically Linked Envelopes): The first general approach that allows reusing control theory literature for NNCS verification. By joining forces, we can exploit the efficiency of NN verification tools while retaining the rigor of differential dynamic logic (dL). Based on a provably safe control envelope in dL, we derive a specification for the NN which is proven with NN verification tools. We show that a proof of the NN’s adherence to the specification is then mirrored by a dL proof on the infinite-time safety of the NNCS.

   The NN verification properties resulting from hybrid systems typically contain nonlinear arithmetic over formulas with arbitrary logical structure while efficient NN verification tools merely support linear constraints. To overcome this divide, we present Mosaic: An efficient, sound and complete verification approach for polynomial real arithmetic properties on piece-wise linear NNs. Mosaic partitions complex NN verification queries into simple queries and lifts off-the-shelf linear constraint tools to the nonlinear setting in a completeness-preserving manner by combining approximation with exact reasoning for counterexample regions. In our evaluation we demonstrate the versatility of VerSAILLE and Mosaic: We prove infinite-time safety on the classical Vertical Airborne Collision Avoidance NNCS verification benchmark for some scenarios while (exhaustively) enumerating counterexample regions in unsafe scenarios. We also show that our approach significantly outperforms the State-of-the-Art tools in closed-loop NNV.

   
   
   
2. Noah Abou El Wafa and André Platzer.
   Complete game logic with sabotage.
   In Pawel Sobocinski, Ugo Dal Lago and Javier Esparza, editors, Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'24, pp. 1:1-1:15, ACM, 2024. © The authors
   [bib | ⧉ | pdf | doi | slides | arXiv]

   We introduce Sabotage Game Logic (GL_s), a simple and natural extension of Parikh's Game Logic with a single additional primitive, which allows players to lay traps for the opponent to avoid. GL_s can be used to model infinite sabotage games, in which players can change the rules during game play. In contrast to Game Logic, which is strictly less expressive, GL_s is exactly as expressive as the modal μ-calculus. This reveals a close connection between the entangled nested recursion inherent in modal fixpoint logics and adversarial dynamic rule changes characteristic for sabotage games.

   Additionally we present a natural Hilbert-style proof calculus for GL_s and prove completeness. The completeness of an extension of Parikh's calculus for Game Logic follows.

   Keywords: Game logic • μ-calculus • Proof theory • Completeness • Expressiveness • Sabotage games

   
   
   
3. Enguerrand Prebet and André Platzer.
   Uniform substitution for differential refinement logic.
   In Christoph Benzmüller, Marijn J. Heule and Renate A. Schmidt, editors, Automated Reasoning, 12th International Joint Conference, IJCAR 2024, Proceedings, volume 14740 of LNCS. pp. 196-215, Springer 2024. © The authors
   [bib | ⧉ | pdf | doi | arXiv]

   This paper introduces a uniform substitution calculus for differential refinement logic dRL. The logic dRL extends the differential dynamic logic dL such that one can simultaneously reason about properties of and relations between hybrid systems. Refinements are useful e.g. for simplifying proofs by relating a concrete hybrid system to an abstract one from which the property can be proved more easily. Uniform substitution is the key to parsimonious prover microkernels. It enables the verbatim use of single axiom formulas instead of axiom schemata with soundness-critical side conditions scattered across the proof calculus. The uniform substitution rule can then be used to instantiate all axioms soundly. Access to differential variables in dRL enables more control over the notion of refinement, which is shown to be decidable on a fragment of hybrid programs.

   Keywords: Uniform substitution • Differential dynamic logic • Refinement • Hybrid systems

   
   
   
4. Aditi Kabra, Jonathan Laurent, Stefan Mitsch, and André Platzer.
   CESAR: control envelope synthesis via angelic refinements.
   In Bernd Finkbeiner and Laura Kovács, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2024, volume 14570 of LNCS, pp. 144-164 Springer, 2024. © The Author(s)
   [bib | ⧉ | pdf | doi | slides | arXiv | artifact]

   This paper presents a synthesis approach for provably correct control envelopes for hybrid systems rooted in hybrid systems game theory. The resulting control envelopes fill in the blanks for a hybrid systems sketch specifying the desired shape of a family of controllers, the possible control actions, and the system's differential equations. In order to maximize the flexibility of the control envelope, the resulting conditions saying which control action can be chosen when are as permissive as possible while establishing a desired safety condition from the available assumptions, which are augmented if needed. Safety of the control envelope stems from the systematic refinement of the optimal game and is justified by formal deductions, while optimality is shown via a dual game characterization. The resulting algorithm, Control Envelope Synthesis via Angelic Refinements (CESAR), is demonstrated in a range of safe control synthesis examples with different control challenges.

   Keywords: Hybrid systems • Program synthesis • Differential game logic

   
   
   
5. Marvin Brieger, Stefan Mitsch and André Platzer.
   Uniform substitution for dynamic logic with communicating hybrid programs.
   In Brigitte Pientka and Cesare Tinelli, editors, International Conference on Automated Deduction, CADE-29, Rome, Italy, Proceedings, volume 14132 of LNCS, pp. 96-115. Springer, 2023. © The Authors
   [bib | ⧉ | pdf | doi | slides | arXiv]

   This paper introduces a uniform substitution calculus for dLCHP, the dynamic logic of communicating hybrid programs. Uniform substitution enables parsimonious prover kernels by using axioms instead of axiom schemata. Instantiations can be recovered from a single proof rule responsible for soundness-critical instantiation checks rather than being spread across axiom schemata in side conditions. Even though communication and parallelism reasoning are notorious for necessitating subtle soundness-critical side conditions, uniform substitution when generalized to dLCHP manages to limit and isolate their conceptual overhead. Since uniform substitution has proven to simplify the implementation of hybrid systems provers substantially, uniform substitution for dLCHP paves the way for a parsimonious implementation of theorem provers for hybrid systems with communication and parallelism.

   Keywords: Uniform substitution • Parallel programs • Differential dynamic logic • Assumption-commitment reasoning • CSP

   
   
   
6. Katherine Kosaian, Yong Kiam Tan, and André Platzer.
   A first complete algorithm for real quantifier elimination in Isabelle/HOL.
   CPP 2023, Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 211-224. ACM, 2023. © ACM
   [bib | ⧉ | pdf | doi | video | Isabelle | arXiv]

   We formalize a multivariate quantifier elimination (QE) algorithm in the theorem prover Isabelle/HOL. Our algorithm is complete, in that it is able to reduce any quantified formula in the first-order logic of real arithmetic to a logically equivalent quantifier-free formula. The algorithm we formalize is a hybrid mixture of Tarski’s original QE algorithm and the Ben-Or, Kozen, and Reif algorithm, and it is the first complete multivariate QE algorithm formalized in Isabelle/HOL.

   Keywords: Quantifier elimination • Theorem proving • Real arithmetic • Multivariate polynomials

   
   
   
7. Jonathan Laurent and André Platzer.
   Learning to find proofs and theorems by learning to refine search strategies:
      The case of loop invariant synthesis.
   In Sanmi Koyejo, Shakir Mohamed, Alekh Agarwal, Danielle Belgrave, Kyunghyun Cho and Alice Oh, editors, Advances in Neural Information Processing Systems 35 NeurIPS 2022 pp. 4843–4856.
   [bib | ⧉ | pdf | eprint | slides | video | poster | arXiv]

   We propose a new approach to automated theorem proving where an AlphaZero-style agent is self-training to refine a generic high-level expert strategy expressed as a nondeterministic program. An analogous teacher agent is self-training 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. As a specific illustration, we consider loop invariant synthesis for imperative programs and use neural networks to refine both the teacher and solver strategies.

   Keywords: Theorem proving • Program synthesis • AlphaZero • Reinforcement learning

   
   
   
8. 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. 1-11. ACM, 2022.
   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 closed-loop 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 function-based 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 non-standard 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

   
   
   
9. 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. 200-217. Springer, 2021. © Springer
   [bib | ⧉ | pdf | doi | slides | Isabelle | arXiv]

   This paper presents a formally verified quantifier elimination (QE) algorithm for first-order real arithmetic by linear and quadratic virtual substitution (VS) in Isabelle/HOL. The Tarski-Seidenberg theorem established that the first-order 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 low-degree 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 general-purpose 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 SMT-RAT. This identified inconsistencies in some tools, underscoring the significance of a verified approach for the intricacies of real arithmetic.

   Keywords: Virtual substitution • Quantifier elimination • Real-closed fields • Theorem proving

   
   
   
10. 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 29-July 1, 2021, Rome, Italy, volume 193 of LIPIcs, pp. 14:1-14:20. Schloss Dagstuhl - Leibniz-Zentrum für Informatik 2021. © The authors
    [bib | ⧉ | pdf | doi | slides | Isabelle | arXiv]

    We formalize the univariate fragment of Ben-Or, Kozen, and Reif's (BKR) decision procedure for first-order 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 follow-up work by Renegar that are well-suited 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

    
    
    
11. 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 IFAC-PapersOnline, pp. 247-252. 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 automata-theoretic and language-based 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

    
    
    
12. 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 first-order 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

    
    
    
13. 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:1-14:19. Schloss Dagstuhl - Leibniz-Zentrum 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

    
    
    
14. Brandon Bohrer and André Platzer.
    Constructive hybrid games.
    In Nicolas Peltier and Viorica Sofronie-Stokkermans, editors, Automated Reasoning, 10th International Joint Conference, IJCAR 2020, Paris, France, Proceedings, Part I, volume 12166 of LNCS, pp. 454-473. Springer 2020. © The authors
    [bib | ⧉ | pdf | doi | mypdf | slides | arXiv]

    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 safety-critical cyber-physical systems. Our contributions include novel semantics as well as soundness and consistency.

    Keywords: Game logic • Constructive logic • Hybrid games • Dependent types

    
    
    
15. 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. 84-111. Springer, 2020. © The authors
    [bib | ⧉ | pdf | doi | mypdf | slides | arXiv]

    Game Logic is an excellent setting to study proofs-about-programs 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 first-order programs à la Pratt’s first-order 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 proof-terms, 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 Curry-Howard interpretation for any program logic to date, and the first at all for Game Logic.

    Keywords: Game logic • Constructive logic • Natural deduction •Proof terms

    
    
    
16. João G. Martins, André Platzer, and João Leite.
    Dynamic doxastic differential dynamic logic for belief-aware cyber-physical systems.
    In Serenella Cerrito and Andrei Popescu, editors, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2019, London, September 3-5, 2019, Proceedings, volume 11714 of LNCS, pp. 428-445. Springer, 2019. © Springer Nature Switzerland AG
    [bib | ⧉ | pdf | doi | slides]

    Cyber-physical 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 first-principles 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⁴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⁴L, which enables us to illustrate the applicability of d⁴L by proving the safety of a simplified belief-triggered controller for an airplane.

    Keywords: Differential dynamic logic • Dynamic epistemic logic • Sequent calculus • Hybrid systems • Cyber-physical systems

    
    
    
17. 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. 138-157. Springer, 2019. © Springer
    FM Best Tool Paper Award.
    [bib | ⧉ | pdf | doi | slides | tool | FMSD'22]

    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 • Cyber-physical systems • Formal verification

    
    
    
18. 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. 371-388. 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 well-known discrete liveness verification techniques, such as loop variants, to the continuous setting. For example, ODE solutions rarely exist in closed-form, 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 well-understood 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

    
    
    
19. Brandon Bohrer, Manuel Fernández and André Platzer.
    dL_ɩ Definite descriptions in differential dynamic logic.
    In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE-27, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 94-110. 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 long-desired features such as vector arithmetic.

    We overcome the unique challenges posed by extending dL with these features. Unlike in dL, definite descriptions enable non-locally-Lipschitz 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

    
    
    
20. Katherine Cordwell and André Platzer.
    Towards physical hybrid systems.
    In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE-27, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 216-232. Springer, 2019. © Springer
    [bib | ⧉ | pdf | doi | slides | arXiv]

    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 cyber-physical 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 first-class 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

    
    
    
21. André Platzer.
    Uniform substitution at one fell swoop.
    In Pascal Fontaine, editor, International Conference on Automated Deduction, CADE-27, Natal, Brazil, Proceedings, volume 11716 of LNCS, pp. 425-441. Springer, 2019. © The author
    [bib | ⧉ | pdf | doi | mypdf | slides | Isabelle | arXiv | errata]

    Uniform substitution of function, predicate, program or game symbols is the core operation in parsimonious provers for hybrid systems and hybrid games. By postponing soundness-critical 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 one-pass uniform substitutions for dGL.

    Keywords: Uniform substitution • Differential game logic • Hybrid games

    
    
    
22. Nathan Fulton and André Platzer.
    Verifiably safe off-model reinforcement learning.
    In Tomas Vojnar and Lijun Zhang, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2019, Proceedings, Part I, volume 11427 of LNCS, pp. 413-430. Springer, 2019. © The authors
    [bib | ⧉ | pdf | doi | arXiv]

    The desire to use reinforcement learning in safety-critical 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 pre-requisite for safe learning, but is ultimately insufficient for systems that operate in complex heterogeneous environments. This paper introduces verification-preserving 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 design-time 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 • Cyber-physical systems • Reinforcement learning • Hybrid systems • Theorem proving

    
    
    
23. Luis Garcia, Stefan Mitsch and André Platzer.
    HyPLC: Hybrid programmable logic controller program translation for verification.
    In Linda Bushnell and Miroslav Pajic, editors, 10th ACM/IEEE International Conference on Cyber-Physical Systems ICCPS'19, pp. 47-56. 2019. © ACM
    Best paper finalist
    [bib | ⧉ | pdf | doi | tool | arXiv]

    Programmable Logic Controllers (PLCs) provide a prominent choice of implementation platform for safety-critical industrial control systems. Formal verification provides ways of establishing correctness guarantees, which can be quite important for such safety-critical 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 cyber-physical interfaces for safety-critical industrial control applications, and HyPLC serves as a pragmatic tool for bridging formal verification of complex cyber-physical 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

    
    
    
24. Brandon Bohrer, Adriel Luo, Xue An Chuang and André Platzer.
    CoasterX: A case study in component-driven 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 IFAC-PapersOnline, pp. 55-60, 2018. © IFAC
    [bib | ⧉ | pdf | doi | slides]

    Component-driven proof automation (CDPA) exploits component structure to automate deductive verification of large-scale hybrid systems with non-trivial continuous dynamics. We use CDPA to implement a case study CoasterX, which is a toolchain for designing and verifying safety of 2-dimensional roller coaster track designs. Specifically, we verify velocity and acceleration bounds. CoasterX starts with a graphical front-end for point-and-click design of tracks. The CoasterX back-end 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 • Component-driven verification

    
    
    
25. 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 15-17, 2018, Proceedings, volume 10951 of LNCS, pp. 418-437. Springer, 2018. © Springer
    [bib | ⧉ | pdf | doi | slides]

    Vector Lyapunov functions are a multi-dimensional extension of the more familiar (scalar) Lyapunov functions, commonly used to prove stability properties in systems described by non-linear ordinary differential equations (ODEs). This paper explores an analogous vector extension for so-called 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

    
    
    
26. Brandon Bohrer and André Platzer.
    A hybrid, dynamic logic for hybrid-dynamic information flow.
    In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, pp. 115-124. ACM 2018. © The authors. Publication rights licensed to ACM
    [bib | ⧉ | pdf | doi | slides | TR]

    Information-flow security is important to the safety and privacy of cyber-physical 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 real-valued 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 hybrid-dynamical models of CPSs. We achieve verification of hybrid information flows by extending differential dynamic logic (dL) for hybrid-dynamical systems with hybrid-logical 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 Hilbert-style 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 previously-unknown 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 hybrid-dynamical model. We discuss applications of hybrid information flow to a range of critical systems.

    Keywords: Dynamic logic • Hybrid logic • Hybrid systems • Information flow • Cyber-physical systems • Formal verification • Smart grid

    
    
    
27. André Platzer and Yong Kiam Tan.
    Differential equation axiomatization:
       The impressive power of differential ghosts.
    In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'18, pp. 819-828. ACM 2018. © The authors
    [bib | ⧉ | pdf | doi | 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 proof-theoretical 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

    
    
    
28. 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. 211-227. 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 soundness-critical 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

    
    
    
29. Brandon Bohrer, Yong Kiam Tan, Stefan Mitsch, Magnus O. Myreen and André Platzer.
    VeriPhy: Verified controller executables from verified cyber-physical system models.
    In Dan Grossmann, editor, Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, pp. 617-630. ACM 2018. © The authors
    [bib | ⧉ | pdf | doi | mypdf | slides | video]

    We present VeriPhy, a verified pipeline which automatically transforms verified high-level models of safety-critical cyber-physical systems (CPSs) in differential dynamic logic (dL) to verified controller executables. VeriPhy proves that all safety results are preserved end-to-end 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 differential-equation 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 cross-verify KeYmaera X in Isabelle/HOL. We evaluate the resulting controller and monitors on commodity robotics hardware.

    Keywords: Cyber-physical systems • Hybrid systems • Formal verification • Verified compilation • Verified executables

    
    
    
30. Nathan Fulton and André Platzer.
    Safe reinforcement learning via formal methods:
       Toward safe control through proof and learning.
    In Sheila A. McIlraith and Kilian Q. Weinberger, editors, AAAI Conference on Artificial Intelligence, pp. 6485-6492. AAAI 2018. © AAAI Press
    [bib | ⧉ | pdf | doi | eprint | slides]

    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 Cyber-Physical Systems because high-fidelity physical models of systems are expensive to develop and often intractable to verify. Conversely, reinforcement learning-based 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 off-line 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 • Cyber-physical systems

    
    
    
31. Stefan Mitsch, Marco Gario, Christof J. Budnik, Michael Golm and André Platzer.
    Formal verification of train control with air pressure brakes.
    In Alessandro Fantechi, Thierry Lecomte and Alexander Romanovsky, editors, RSSRail 2017: Reliability, Safety, and Security of Railway Systems, volume 10598 of LNCS, pp. 173-191. Springer, 2017. © Springer
    [bib | ⧉ | pdf | doi | slides]

    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

    
    
    
32. Nathan Fulton, Stefan Mitsch, Brandon Bohrer and André Platzer.
    Bellerophon: Tactical theorem proving for hybrid systems.
    In Mauricio Ayala-Rincón and César A. Muñoz, editors, Interactive Theorem Proving, International Conference, ITP 2017, volume 10499 of LNCS, pp. 207-224. 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 general-purpose 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 non-solvable system.

    Keywords: Hybrid systems • Tactical theorem proving • Differential dynamic logic

    
    
    
33. 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. 134-151. Springer, 2017. © Springer
    [bib | ⧉ | pdf | doi | slides | study | STTT'18]

    In this paper, we present reasoning techniques for a component-based 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 component-based 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: component-based development • hybrid systems • formal verification

    
    
    
34. 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 16-17, 2017, pp. 208-221, 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 • hybrid-system verification • KeYmaera X • formalization

    
    
    
35. Sarah M. Loos and André Platzer.
    Differential refinement logic.
    ACM/IEEE Symposium on Logic in Computer Science, LICS 2016, July 5–8, 2016, New York, NY, USA, pp. 505-514. ACM, 2016. © The authors
    [bib | ⧉ | pdf | doi | mypdf | slides]

    We introduce differential refinement logic (dRL), a logic with first-class 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 implementation-specific. 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 better-structured proofs.

    Keywords: differential dynamic logic • hybrid systems •cyber-physical systems •theorem proving • refinement

    
    
    
36. Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger and André Platzer.
    A component-based approach to hybrid systems safety verification.
    In Erika Abraham and Marieke Huisman, editors, Integrated Formal Methods - 12th International Conference, iFM 2016, Reykjavik, Iceland, June 1-4, 2016, Proceedings, volume 9681 of LNCS, pp. 441-456. Springer, 2016. © Springer
    [bib | ⧉ | pdf | doi | slides | TR]

    We study a component-based approach to simplify the challenges of verifying large-scale hybrid systems. Component-based 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 component-based hybrid system verification approach that combines the advantages of component-based 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:  Component-based development • Hybrid systems • Formal verification

    
    
    
37. 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 18-19, 2016, pp. 110-121. 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 cyber-physical systems. Theorem provers based on differential dynamic logic have been used to verify safety properties for models of self-driving 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 soundness-critical and extra-logical extensions to the theorem prover. Examples include: an unambiguous separation between proof checking and proof search, the ability to extract program traces corresponding to counter-examples, and synthesis of surely-live 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:  cyber-physical systems • differential dynamic logic • hybrid systems • proof terms

    
    
    
38. 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 17-19, 2016, Proceedings, volume 9583 of LNCS, pp. 268-288. Springer, 2016. © Springer
    [bib | ⧉ | pdf | doi | slides]

    This paper presents a method for generating semi-algebraic invariants for systems governed by non-linear polynomial ordinary differential equations under semi-algebraic evolution constraints. Based on the notion of discrete abstraction, our method eliminates unsoundness and unnecessary coarseness found in existing approaches for computing abstractions for non-linear continuous systems and is able to construct invariants with intricate boolean structure, in contrast to invariants typically generated using template-based 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 divide-and-conquer (DDC), which splits the verification problem into smaller sub-problems. 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

    
    
    
39. Andreas Müller and Stefan Mitsch and André Platzer.
    Verified traffic networks: Component-based verification of cyber-physical flow systems.
    In Intelligent Transportation Systems ITSC'15', IEEE 18th International Conference on, pp. 757-764, 2015. © IEEE
    [bib | ⧉ | pdf | doi | slides]

    We address the problem how high-fidelity verification results about the hybrid systems dynamics of cyber-physical 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 higher-fidelity 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 model-based analysis and design tool for traffic flow networks.

    Keywords:  Automobiles • Contracts • Load modeling •Mathematical model • Roads • Safety

    
    
    
40. 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. 227-236. 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, state-of-the-art 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.

    
    
    
41. André Platzer.
    A uniform substitution calculus for differential dynamic logic.
    In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE-25, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 467-481. Springer, 2015. © Springer
    [bib | ⧉ | pdf | doi | slides | arXiv | JAR'17]

    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 soundness-critical 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 first-class citizens in the logic.

    Keywords: differential dynamic logic • uniform substitution • axioms • differentials • static semantics

    
    
    
42. Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki, and André Platzer.
    A formally verified hybrid system for the next-generation airborne collision avoidance system.
    In Christel Baier and Cesare Tinelli, editors, Tools and Algorithms for the Construction and Analysis of Systems - 21st International Conference, TACAS 2015, London, UK, April 11-18, 2015, Proceedings, volume 9035 of LNCS, pp. 21-36. Springer, 2015. © Springer
    [bib | ⧉ | pdf | doi | study | TR | STTT'17]

    The next-generation Airborne Collision Avoidance System (ACAS X) is intended to be installed on all large aircraft to give advice to pilots and prevent mid-air 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 • Cyber-physical systems

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

    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 trade-off 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

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

    Formal verification and validation play a crucial role in making cyber-physical 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 • Cyber-physical systems • Hybrid systems • Logic

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

    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

    
    
    
46. Jean-Baptiste Jeannin and André Platzer.
    dTL²: Differential temporal dynamic logic with nested temporalities for hybrid systems.
    In Stéphane Demri, Deepak Kapur and Christoph Weidenbach, editors, Automated Reasoning, 7th International Joint Conference, IJCAR 2014, Vienna, Austria, July 19-22, 2014, Proceedings, volume 8562 of LNCS, pp. 292-306. Springer, 2014. © Springer
    [bib | ⧉ | pdf | doi | slides]

    The differential temporal dynamic logic dTL² 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² 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², 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

    
    
    
47. Stefan Mitsch, Jan-David Quesel and André Platzer.
    Refactoring, refinement, and reasoning:
       A logical characterization for hybrid systems.
    In Cliff B. Jones, Pekka Pihlajasaari and Jun Sun, editors, 19th International Symposium on Formal Methods, FM'14, Singapore, Proceedings, volume 8442 of LNCS, pp. 481-496. Springer, 2014. © Springer
    [bib | ⧉ | pdf | doi | slides]

    Refactoring of code is a common device in classical programs. As cyber-physical 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 proof-aware 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 safety-preserving and liveness preserving refactorings. For some of these we can give strong results by proving on a meta-level 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 • model-driven engineering

    
    
    
48. Khalil Ghorbal and André Platzer.
    Characterizing algebraic invariants by differential radical invariants.
    In Erika Ábrahám and Klaus Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014, Proceedings, volume 8413 of LNCS, pp. 279-294. Springer, 2014. © Springer
    [bib | ⧉ | pdf | doi | slides | study | TR]

    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 so-called 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 real-closed 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 NP-hard. 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 take-off or landing in longitudinal motion.

    Keywords:  Algebraic invariants • Differential ideals • Higher-order Lie derivation • Differential invariants • Differential equations • Invariant generation

    
    
    
49. 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 provably-safe 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

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

    
    
    
51. 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 3-9, 2013, pp. 2583-2589, 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 concisely-describable set of existentially-quantified, propositional formulas. We characterize the expressiveness and worst-case 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 general-purpose #ESAT solvers on a battery of problem distributions including a simple logistics domain. Our experiments show that, despite the formidable worst-case 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

    
    
    
52. Yanni Kouskoulas, David W. Renshaw, André Platzer and Peter Kazanzides.
    Certifying the safe design of a virtual fixture control algorithm for a surgical robot.
    In Calin Belta and Franjo Ivancic, editors, Hybrid Systems: Computation and Control (part of CPS Week 2013), HSCC'13, Philadelphia, PA, USA, April 8-13, 2013, pp. 263-272. ACM, 2013. © ACM
    [bib | ⧉ | pdf | doi | slides | study]

    We applied quantified differential-dynamic 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 machine-checked proof that guarantees the new algorithm is safe for all possible inputs.

    Keywords: quantified differential dynamic logic • medical robotics • formal verification

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

    As airspace becomes ever more crowded, air traffic management must reduce both space and time between aircraft to increase throughput, making on-board collision avoidance systems ever more important. These safety-critical 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 in-progress 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

    
    
    
54. 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 17-20, London, UK, pp. 84-93. 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

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

    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

    
    
    
56. André Platzer.
    The complete proof theory of hybrid systems.
    ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pp. 541-550. IEEE 2012. © IEEE
    [bib | ⧉ | pdf | doi | slides | TR]

    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, proof-theoretically, this is not the case. We present a complete proof-theoretical 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

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

    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 closed-loop 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 left-turn assist. In each case, safety of the closed-loop system proved using KeYmaera provides static sufficient conditions that are checked for the controller design.

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

    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 trade-offs for practical system implementations even for design parameters that are not modeled formally.

    Keywords: freeway traffic control • intelligent speed adaptation • hybrid system

    
    
    
59. 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'11. pp. 2705-2710, IEEE. 2011. © IEEE
    [bib | ⧉ | pdf | doi | TAC'14]

    Current methods for designing cyber-physical 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 system-level specification. Interdependencies and connections between the constraints in the architectural views are managed in the base architecture using first-order logic of real arithmetic to ensure consistency and correct reasoning. The approach is illustrated in the context of heterogeneous verification of a leader-follower vehicle scenario.

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

    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.

    
    
    
61. 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. 131-146. 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 real-world power consumption). We propose Distributed Probabilistic-Control 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 model-checking 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

    
    
    
62. 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. 356-371. 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

    
    
    
63. André Platzer.
    Stochastic differential dynamic logic for stochastic hybrid programs.
    In Nikolaj Bjørner and Viorica Sofronie-Stokkermans, editors, International Conference on Automated Deduction, CADE-23, Wroclaw, Poland, Proceedings, volume 6803 of LNCS, pp. 446-460. Springer, 2011. © Springer
    [bib | ⧉ | pdf | doi | slides | TR]

    Logic is a powerful tool for analyzing and verifying systems, including programs, discrete systems, real-time 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

    
    
    
64. 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 21-24, 2011, Proceedings, volume 6742 of LNCS, pp. 140-157. Springer, 2011. © Springer
    [bib | ⧉ | pdf | doi | arXiv]

    We give an algebraic quantifier elimination algorithm for the first-order 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

    
    
    
65. Sarah M. Loos, André Platzer and Ligia Nistor.
    Adaptive cruise control:
       Hybrid, distributed, and now formally verified.
    In Michael Butler and Wolfram Schulte, editors, 17th International Symposium on Formal Methods, FM, Limerick, Ireland, Proceedings, volume 6664 of LNCS, pp. 42-56. Springer, 2011. © Springer
    [bib | ⧉ | pdf | doi | slides | study | TR]

    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 cyber-physical 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 on-ramps or multi-lane streets. The system we present is in many ways one of the most complicated cyber-physical systems that has ever been fully verified formally.

    Keywords: distributed car control • multi-agent systems • highway traffic safety • formal verification • distributed hybrid systems • adaptive cruise control

    
    
    
66. Erik P. Zawadzki, Geoffrey J. Gordon and André Platzer.
    An Instantiation-Based Theorem Prover for First-Order Programming.
    In 14th International Conference on Artificial Intelligence and Statistics (AISTATS) 2011, Fort Lauderdale, FL, USA, Proceedings, volume 15 of JMLR W&CP, pp. 855-863, 2011.
    [bib | ⧉ | pdf | poster | proceedings]

    First-order programming (FOP) is a new representation language that combines the strengths of mixed-integer linear programming (MILP) and first-order logic (FOL). In this paper we describe a novel feasibility proving system for FOP formulas that combines MILP solving with instance-based 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 first-order planning problem.

    
    
    
67. André Platzer.
    Quantified differential invariants.
    In Emilio Frazzoli and Radu Grosu, editors, Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, USA, April 12-14, pp. 63-72. ACM, 2011. © ACM
    [bib | ⧉ | pdf | doi | slides]

    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 real-closed fields. This gives a computationally attractive technique, because it works without having to solve the infinite-dimensional 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

    
    
    
68. André Platzer.
    Quantified differential dynamic logic for distributed hybrid systems.
    In Anuj Dawar and Helmut Veith, editors, Computer Science Logic, 19th EACSL Annual Conference, CSL 2010, Brno, Czech Republic, August 23-27, 2010. Proceedings, volume 6247 of LNCS, pp. 469-483. Springer, 2010. © Springer
    [bib | ⧉ | pdf | doi | slides | TR | LMCS'12]

    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 dimensionality-changes. 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

    
    
    
69. Paolo Zuliani, André Platzer and Edmund M. Clarke.
    Bayesian statistical model checking with application to Simulink/Stateflow verification.
    In Karl Henrik Johansson and Wang Yi, editors, Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, April 12-15, pp. 243-252. ACM, 2010. © ACM
    [bib | ⧉ | pdf | doi | slides | TR]

    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 non-Bayesian 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 discrete-time 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 state-of-the-art 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.

    
    
    
70. André Platzer and Jan-David Quesel.
    European Train Control System: A case study in formal verification.
    In Karin Breitman and Ana Cavalcanti, editors, 11th International Conference on Formal Engineering Methods, ICFEM'09, Rio de Janeiro, Brasil, Proceedings, volume 5885 of LNCS, pp. 246-265. Springer, 2009. © Springer
    [bib | ⧉ | pdf | doi | slides | kyx | TR | old]

    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

    
    
    
71. André Platzer and Edmund M. Clarke.
    Formal verification of curved flight collision avoidance maneuvers: A case study.
    In Ana Cavalcanti and Dennis Dams, editors, 16th International Symposium on Formal Methods, FM, Eindhoven, Netherlands, Proceedings, volume 5850 of LNCS, pp. 547-562. Springer, 2009. © Springer
    FM Best Paper Award.
    [bib | ⧉ | pdf | doi | slides | study | TR]

    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

    
    
    
72. 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. 218-234. 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 state-of-the-art techniques, even when no prior knowledge is available.

    
    
    
73. André Platzer, Jan-David Quesel and Philipp Rümmer.
    Real world verification.
    In Renate A. Schmidt, editor, International Conference on Automated Deduction, CADE-22, Montreal, Canada, Proceedings, volume 5663 of LNCS, pp. 485-501. Springer, 2009. © Springer
    [bib | ⧉ | pdf | doi | slides | study | TR | smtlib]
    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 real-world 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 real-closed 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: real-closed fields • decision procedures • hybrid systems • software verification

    
    
    
74. André Platzer and Edmund M. Clarke.
    Computing differential invariants of hybrid systems as fixedpoints.
    In Aarti Gupta and Sharad Malik, editors, Computer Aided Verification, CAV 2008, Princeton, USA, Proceedings, volume 5123 of LNCS, pp. 176-189, Springer, 2008. © Springer
    [bib | ⧉ | pdf | doi | slides | study | TR | FMSD'09]

    We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations whose right-hand 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

    
    
    
75. André Platzer.
    Differential dynamic logic for verifying parametric hybrid systems.
    In Nicola Olivetti, editor, Automated Reasoning with Analytic Tableaux and Related Methods, International Conference, TABLEAUX 2007, Aix en Provence, France, July 3-6, 2007, Proceedings, volume 4548 of LNCS, pp. 216-232. Springer, 2007. © Springer
    TABLEAUX Best Paper Award.
    [bib | ⧉ | pdf | doi | slides | study | TR]

    We introduce a first-order 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 first-order 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

    
    
    
76. André Platzer.
    A temporal dynamic logic for verifying hybrid system invariants.
    In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, International Symposium, LFCS 2007, New York, USA, Proceedings, volume 4514 of LNCS, pp. 457-471. Springer, 2007. © Springer
    [bib | ⧉ | pdf | doi | slides | study | TR]

    We combine first-order 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 first-order 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 non-temporal 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

    
    
    
77. André Platzer and Edmund M. Clarke.
    The image computation problem in hybrid systems model checking.
    In Alberto Bemporad, Antonio Bicchi and Giorgio Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pp. 473-486. Springer, 2007, © Springer
    [bib | ⧉ | pdf | doi | slides | tool]

    In this paper, we analyze limits of approximation techniques for (non-linear) 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

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

    We introduce a dynamic logic that is enriched by non-rigid 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, non-rigid functions allow to embed notions of object-orientation in dynamic logic, thereby forming a basis for verification of object-oriented 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 object-oriented 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 • object-orientation

    
    
    

Short & Tool Publications

1. 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 7-12, 2022, Proceedings. volume 13385 of LNCS, pp. 723-733. Springer, 2022. © The authors
   [bib | ⧉ | pdf | doi | slides | 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 user-defined 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 soundness-critical kernel with a single axiom scheme that expands function occurrences with their implicit characterization. Users are provided with a high-level interface for defining functions and non-soundness-critical tactics that automate low-level reasoning over implicit characterizations in hybrid system proofs.

   Keywords: Definitions • Differential dynamic logic • Verification of hybrid systems • Theorem proving

   
   
   
2. Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp and André Platzer.
   KeYmaera X: An aXiomatic tactical theorem prover for hybrid systems.
   In Amy P. Felty and Aart Middeldorp, editors, International Conference on Automated Deduction, CADE-25, Berlin, Germany, Proceedings, volume 9195 of LNCS, pp. 527-538. Springer, 2015. © Springer
   [bib | ⧉ | pdf | doi | slides | poster | tool | tooldoi]

   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 features---and user-defined tactics in particular---are 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 soundness-critical 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

   
   
   
3. André Platzer and Jan-David Quesel.
   KeYmaera: A hybrid theorem prover for hybrid systems.
   In Alessandro Armando, Peter Baumgartner and Gilles Dowek, editors, Automated Reasoning, Fourth International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings, volume 5195 of LNCS, pp. 171-178. Springer, 2008. © Springer
   [bib | ⧉ | pdf | doi | slides | tool]

   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 real-valued first-order dynamic logic for hybrid programs, a program notation for hybrid automata. For automating the verification process, KeYmaera implements a generalized free-variable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically. To overcome the complexity of real arithmetic, we integrate real quantifier elimination following an iterative background closure strategy. Our tool is particularly suitable for verifying parametric hybrid systems and has been used successfully for verifying collision avoidance in case studies from train control and air traffic management.

   Keywords: dynamic logic • automated theorem proving • decision procedures • computer algebra • verification of hybrid systems

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

   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 logic-based 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

   
   
   
5. André Platzer.
   Differential logic for reasoning about hybrid systems.
   In Alberto Bemporad, Antonio Bicchi and Giorgio Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pp. 746-749. Springer, 2007. © Springer
   [bib | ⧉ | pdf | doi | poster]

   We propose a first-order 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 first-order 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

1. Andreas Müller, Stefan Mitsch, Wieland Schwinger and André Platzer.
   A component-based 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. Model-Based Design, revised selected papers, volume 11615 of LNCS, pp. 91-110. Springer, 2019. © Springer
   [bib | ⧉ | pdf | doi]

   Safety-critical cyber-physical 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 component-based 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 component-based 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: Component-based development • Hybrid systems • Formal verification

   
   
   
2. 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 F-IDE 2016, volume 240 of EPTCS, pp. 67-81, 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.

   
   
   
3. Stefan Mitsch, Jan-David Quesel, and André Platzer.
   From safety to guilty & from liveness to niceness.
   In Calin Belta and Hadas Kress-Gazit, 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.

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

   
   
   
5. André Platzer.
   Teaching CPS foundations with contracts.
   First Workshop on Cyber-Physical Systems Education (CPS-Ed 2013), pp. 7-10. 2013.
   [bib | ⧉ | pdf | eprint | slides | poster | course]

   We describe the experience with courses that teach the Foundations of Cyber-physical 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: cyber-physical systems • foundations • education • correctness • contracts

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

   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

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

   In this paper, we present an abstraction refinement approach for model checking safety properties of real-time systems using SAT-solving. 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 linear-size 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 counterexample-guided abstraction refinement with syntactic information about Craig interpolants. To support generalisations, our overall approach identifies the algebraic and logical principles required for logic-based abstraction refinement.

   Keywords: abstraction refinement • model checking • real-time systems • SAT • Craig interpolation

   
   
   
8. André Platzer.
   Towards a hybrid dynamic logic for hybrid dynamic systems.
   In Patrick Blackburn, Thomas Bolander, Torben Braüner, Valeria de Paiva and Jørgen Villadsen, editors, Proc., International Workshop on Hybrid Logic, HyLo 2006, Seattle, USA, Electr. Notes Theor. Comput. Sci. 174(6):63-77, 2007.
   [bib | ⧉ | pdf | doi | slides]

   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 state-based 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 goal-oriented 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 • real-time hybrid dynamic systems

   
   
   

Invited Papers

1. André Platzer.
   Intersymbolic AI:
      Interlinking symbolic AI and subsymbolic AI.
   In Tiziana Margaria and Bernhard Steffen, editors, ISoLA 2024, Proceedings, volume 15222 of LNCS, pp. 162-180. Springer 2024. © The Author(s), under exclusive license to Springer Nature
   Invited paper.
   [bib | ⧉ | pdf | doi | slides | arXiv]

   This perspective piece calls for the study of the new field of Intersymbolic AI, by which we mean the combination of symbolic AI, whose building blocks have inherent significance/meaning, with subsymbolic AI, whose entirety creates significance/effect despite the fact that individual building blocks escape meaning. Canonical kinds of symbolic AI are logic, games and planning. Canonical kinds of subsymbolic AI are (un)supervised machine and reinforcement learning. Intersymbolic AI interlinks the worlds of symbolic AI with its compositional symbolic significance and meaning and of subsymbolic AI with its summative significance or effect to enable culminations of insights from both worlds by going between and across symbolic AI insights with subsymbolic AI techniques that are being helped by symbolic AI principles. For example, Intersymbolic AI may start with symbolic AI to understand a dynamic system, continue with subsymbolic AI to learn its control, and end with symbolic AI to safely use the outcome of the learned subsymbolic AI controller in the dynamic system. Intersymbolic AI combines both symbolic and subsymbolic AI to increase the effectiveness of AI compared to either kind of AI alone, in much the same way that the combination of both conscious and subconscious thought increases the effectiveness of human thought compared to either kind of thought alone. Some successful contributions to the Intersymbolic AI paradigm are surveyed here but many more are considered possible by advancing Intersymbolic AI.

   Keywords: Artificial Intelligence • Symbolic AI • Subsymbolic AI • Intersymbolic AI • Logic • Verification • Machine Learning

   
   
   
2. André Platzer.
   The significance of symbolic logic for scientific education.
   In Emil Sekerinski and Leila Ribeiro, editors, Formal Methods Teaching: 6th International Workshop, FMTea 2024, Proceedings, volume 14939 of LNCS, pp. 3-22. Springer 2024. © The Author(s)
   Invited paper.
   [bib | ⧉ | pdf | doi | slides | arXiv]

   This invited paper is a passionate pitch for the significance of logic in scientific education. Logic helps focus on the essential core to identify the foundations of ideas and provides corresponding longevity with the resulting approach to new and old problems. Logic operates symbolically, where each part has a precise meaning and the meaning of the whole is compositional, so a simple function of the meaning of the pieces. This compositionality in the meaning of logical operators is the basis for compositionality in reasoning about logical operators. Both semantic and deductive compositionalities help explain what happens in reasoning. The correctness-critical core of an idea or an algorithm is often expressible eloquently and particularly concisely in logic. The opinions voiced in this paper are influenced by the author's teaching of courses on cyber-physical systems, constructive logic, compiler design, programming language semantics, and imperative programming principles. In each of those courses, different aspects of logic come up for different purposes to elucidate significant ideas particularly clearly. While there is a bias of the thoughts in this paper toward computer science, some courses have been heavily frequented by students from other majors so that some transfer of the thoughts to other science and engineering disciplines is plausible.

   Keywords: Education • Logic • Logic of dynamical systems • Constructive logic • Proofs • Programs • Program semantics

   
   
   
3. André Platzer.
   Refinements of hybrid dynamical systems logic.
   In Uwe Glässer, José Creissac Campos, Dominique Méry, Philippe Palanque, editors, Rigorous State-Based Methods - 9th International Conference, ABZ 2023, Nancy, France, Proceedings. volume 14010 of LNCS. pp 3-14. Springer, 2023. © The author under exclusive license to Springer Nature
   Invited paper.
   [bib | ⧉ | doi | slides | SCP'25]

   Hybrid dynamical systems describe the mixed discrete dynamics and continuous dynamics of cyber-physical systems such as aircraft, cars, trains, and robots. To justify correctness of their safety-critical controls for their physical models, differential dynamic logic (dL) provides deductive specification and verification techniques implemented in the theorem prover KeYmaera X. The logic dL is useful for proving, e.g., that all runs of a hybrid dynamical system are safe ([α]ɸ), or that there is a run of the hybrid dynamical system ultimately reaching the desired goal (<α>ɸ). Combinations of dL's operators naturally represent safety, liveness, stability and other properties. Variations of dL serve additional purposes. Differential refinement logic (dRL) adds an operator α ≤ β expressing that hybrid system α refines hybrid system β, which is useful, e.g., for relating concrete system implementations to their abstract verification models. Just like dL, dRL is a logic closed under all operators, which opens up systematic ways of simultaneously relating systems and their properties, of reducing system properties to system relations or, vice versa, reducing system relations to system properties. Differential game logic (dGL) adds the ability of referring to winning strategies of players in hybrid games, which is useful for establishing correctness properties of systems where the actions of different agents may interfere. dL and its variations have been used in KeYmaera X for verifying ground robot obstacle avoidance, the Next-Generation Airborne Collision Avoidance System ACAS X, and the kinematics of train control in the Federal Railroad Administration model with track terrain influence and air pressure brake propagation.

   Keywords: Differential dynamic logic • Differential refinement logic • Differential game logic • Hybrid systems • Hybrid games • Theorem proving

   
   
   
4. André Platzer.
   The logical path to autonomous cyber-physical 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. 25-33. Springer, 2019. © Springer
   Invited paper.
   [bib | ⧉ | pdf | doi | slides]

   Autonomous cyber-physical 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 self-driving 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 cyber-physical 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 cyber-physical systems in multiple steps. First, differential dynamic logic (dL) provides a logical foundation for developing cyber-physical system models with the mathematical rigor that their safety-critical 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 cyber-physical systems • Safe AI • Hybrid systems • Differential dynamic logic • Formal verification • Runtime verification

   
   
   
5. 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 cyber-physical systems -- such as self-driving 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 cyber-physical systems that use AI for planning and control by combining the rigor of formal proofs with the flexibility of reinforcement learning.

   Keywords: AI safety • Cyber-physical systems • Formal methods • Safe reinforcement learning • Hybrid systems • Theorem proving

   
   
   
6. 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.
   High-assurance SPIRAL:
      End-to-end guarantees for robot and car control.
   IEEE Control Systems 37(2), pp. 82-103. 2017. © IEEE
   [bib | ⧉ | pdf | doi]
   
   
7. André Platzer.
   Logic & proofs for cyber-physical systems.
   In Nicola Olivetti and Ashish Tiwari, editors, Automated Reasoning, 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, Proceedings, volume 9706 of LNCS, pp. 15-21. Springer, 2016. © Springer
   Invited paper.
   [bib | ⧉ | pdf | doi | slides]

   Cyber-physical systems (CPS) combine cyber aspects such as communication and computer control with physical aspects such as movement in space, which arise frequently in many safety-critical 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 cyber-physical 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.

   Multi-dynamical 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 skull-base 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 • Cyber-physical systems • Multi-dynamical systems • Differential dynamic logic • KeYmaera X

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

   
   
   
9. Jean-Baptiste 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. 127-136. 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 engineering-focused 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 • Cyber-physical systems

   
   
   
10. 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 light-weight 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 cyber-physical 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 Church-Turing? 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.

    
    
    
11. André Platzer.
    Logical analysis of hybrid systems:
       A complete answer to a complexity challenge.
    Journal of Automata, Languages and Combinatorics 17(2-4), pp. 265-275. 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

    
    
    
12. 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. 43-49. 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

    
    
    
13. André Platzer.
    A differential operator approach to equational differential invariants.
    In Lennart Beringer and Amy Felty, editors, Interactive Theorem Proving, International Conference, ITP 2012, August 13-15, Princeton, USA, Proceedings, volume 7406 of LNCS, pp. 28-48. Springer, 2012. © Springer
    Invited paper.
    [bib | ⧉ | pdf | doi | slides]

    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

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

    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 cyber-physical 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 safety-critical applications in automotive, aviation, railway, robotics, and analogue electrical circuits.

    Keywords: logic of dynamical systems • dynamic logic • differential dynamic logic • hybrid systems • axiomatization • deduction

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

    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 closed-loop 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 left-turn assist. In each case, safety of the closed-loop system proved using KeYmaera provides static sufficient conditions that are checked for the controller design.

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

    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.

    
    
    
17. André Platzer.
    Logic and compositional verification of hybrid systems.
    In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification, CAV 2011, Snowbird, UT, USA, Proceedings, volume 6806 of LNCS, pp. 28-43. Springer, 2011. © Springer
    Invited tutorial.
    [bib | ⧉ | pdf | doi | slides]

    Hybrid systems are models for complex physical systems and have become a widely used concept for understanding their behavior. Many applications are safety-critical, including car, railway, and air traffic control, robotics, physical-chemical 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 state-transitions 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 state-of-the-art 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.

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

    Designing and analyzing hybrid systems, which are models for complex physical systems, is expensive and error-prone. 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.

    
    
    
19. André Platzer.
    Verification of cyberphysical transportation systems.
    IEEE Intelligent Systems 24(4), pp. 10-13, 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. Logic-based analysis can verify the correct functioning of these cyberphysical systems.

    Keywords: cyber-physical transportation systems • train control • air traffic control • logic-based analysis • verification

    
    
    
20. Werner Damm, Alfred Mikschl, Jens Oehlerking, Ernst-Rüdiger Olderog, Jun Pang, André Platzer, Marc Segelken and Boris Wirtz.
    Automating verification of cooperation, control, and design in traffic applications.
    In Cliff Jones, Zhiming Liu and Jim Woodcock, editors, Formal Methods and Hybrid Real-Time Systems, volume 4700 of LNCS, pp. 115-169. 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 pre-verified design patterns, automatic synthesis of Lyapunov functions, constraint generation for parameterized designs, model-checking 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

1. 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 real-valued 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 logic-based 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

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

   With the goal of this thesis being to create a dynamic logic for object-oriented languages, ODL is developed along with a sound and relatively complete calculus. The dynamic logic contains only the absolute logical essentials of object-orientation, yet still allows a ``natural'' representation of all other features of common object-oriented 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 first-order arithmetic. Along with the soundness result, this proof constitutes the central part of this thesis and even copes with states containing uncomputable functions.

   
   
   
3. 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 that---despite the undecidable nature of program analysis---the 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.

   
   
   

Video Productions

1. André Platzer.
   Videos for Logical Foundations of Cyber-Physical Systems.
   YouTube 2018-2019. Videos for 22 lectures of about an hour each.
   [bib | ⧉ | video | Textbook]

   Cyber-physical 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 safety-critical 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 multi-dynamical 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.

   
   
   

Reports

1. Brandon Bohrer, Manuel Fernández and André Platzer.
   dL_ɩ: Definite Descriptions in Differential Dynamic Logic.
   School of Computer Science, Carnegie Mellon University, CMU-CS-19-111, 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 long-desired features such as vector arithmetic.

   We overcome the unique challenges posed by extending dL with these features. Unlike in dL, definite descriptions enable non-locally-Lipschitz 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

   
   
   
2. Brandon Bohrer and André Platzer.
   A Hybrid, Dynamic Logic for Hybrid-Dynamic Information Flow.
   School of Computer Science, Carnegie Mellon University, CMU-CS-18-105, 2018.
   [bib | ⧉ | pdf | LICS'18]

   Information-flow security is important to the safety and privacy of cyber-physical 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 real-valued 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 hybrid-dynamical models of CPSs. We achieve verification of hybrid information flows by extending differential dynamic logic (dL) for hybrid-dynamical systems with hybrid-logical 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 Hilbert-style 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 previously-unknown 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 hybrid-dynamical model. We discuss applications of hybrid information flow to a range of critical systems.

   Keywords: Dynamic logic • Hybrid logic • Hybrid systems • Information flow • Cyber-physical systems • Formal verification • Smart grid

   
   
   
3. André Platzer and Yong Kiam Tan.
   How to Prove "All" Differential Equation Properties.
   School of Computer Science, Carnegie Mellon University, CMU-CS-17-117, 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 proof-theoretical 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

   
   
   
4. Andreas Müller, Stefan Mitsch, Werner Retschitzegger, Wieland Schwinger and André Platzer.
   A Component-based Approach to Hybrid Systems Safety Verification.
   School of Computer Science, Carnegie Mellon University, CMU-CS-16-100, 2016.
   [bib | ⧉ | pdf | IFM'16]

   We study a component-based approach to simplify the challenges of verifying large-scale hybrid systems. Component-based 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 component-based hybrid system verification approach that combines the advantages of component-based 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:  Component-based development • Hybrid systems • Formal verification

   
   
   
5. André Platzer.
   Differential Hybrid Games.
   School of Computer Science, Carnegie Mellon University, CMU-CS-14-102, 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

   
   
   
6. Jean-Baptiste Jeannin, Khalil Ghorbal, Yanni Kouskoulas, Ryan Gardner, Aurora Schmidt, Erik Zawadzki, and André Platzer.
   A Formally Verified Hybrid System for the Next-Generation Airborne Collision Avoidance System.
   School of Computer Science, Carnegie Mellon University, CMU-CS-14-138, 2014.
   [bib | ⧉ | pdf | study | TACAS'15]

   The next-generation Airborne Collision Avoidance System (ACAS X) is intended to be installed on all large aircraft to give advice to pilots and prevent mid-air 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 • Cyber-physical systems

   
   
   
7. Stefan Mitsch and André Platzer.
   ModelPlex: Verified Runtime Validation of Verified Cyber-physical System Models.
   School of Computer Science, Carnegie Mellon University, CMU-CS-14-121, 2014.
   [bib | ⧉ | pdf | study | RV'14]

   Formal verification and validation play a crucial role in making cyber-physical 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 • Cyber-physical systems • Hybrid systems • Logic

   
   
   
8. Khalil Ghorbal and André Platzer.
   Characterizing Algebraic Invariants by Differential Radical Invariants.
   School of Computer Science, Carnegie Mellon University, CMU-CS-13-129, 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 so-called 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 real-closed 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 NP-hard. 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 take-off or landing in longitudinal motion.

   Keywords:  Algebraic invariants • Differential ideals • Higher-order Lie derivation • Differential invariants • Differential equations • Invariant generation

   
   
   
9. 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, CMU-CS-13-107, 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 concisely-describable set of existentially quantified, propositional formulas. We characterize the expressiveness and worst-case 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 general-purpose #∃SAT solvers on a battery of problem distributions including a simple logistics domain. Our experiments show that, despite the formidable worst-case 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

   
   
   
10. Yanni Kouskoulas, André Platzer and Peter Kazanzides.
    Formal Methods for Robotic System Control Software.
    Johns Hopkins APL Technical Digest 32(2), pp. 490-498, 2013.
    [bib | ⧉ | pdf]

    Creating software for controlling robotic machinery has unique challenges. This article describes a formal method called differential-dynamic logic (dL) that can help produce zero-defect 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

    
    
    
11. André Platzer.
    A Complete Axiomatization of Differential Game Logic for Hybrid Games.
    School of Computer Science, Carnegie Mellon University, CMU-CS-13-100R, 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

    
    
    
12. David Renshaw, Sarah M. Loos and André Platzer.
    Mechanized Safety Proofs for Disc-Constrained Aircraft.
    School of Computer Science, Carnegie Mellon University, CMU-CS-12-132, 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 on-board 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 in-progress 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

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

    We introduce differential game logic (dGL) for specifying and verifying properties of hybrid games, i.e., determined, sequential/dynamic, non-cooperative, zero-sum 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

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

    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, proof-theoretically, this is not the case. We present a complete proof-theoretical 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

    
    
    
15. David W. Renshaw and André Platzer.
    Differential Invariants and Symbolic Integration for Distributed Hybrid Systems.
    School of Computer Science, Carnegie Mellon University, CMU-CS-12-107, May 2012.
    [bib | ⧉ | pdf]
    
    
16. André Platzer.
    The Structure of Differential Invariants and Differential Cut Elimination.
    School of Computer Science, Carnegie Mellon University, CMU-CS-11-112, April 2011.
    [bib | ⧉ | pdf | arXiv | LMCS'12]

    The biggest challenge in hybrid systems verification is the handling of differential equations. Because computable closed-form 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 ad-hoc, 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 trade-offs 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

    
    
    
17. André Platzer.
    Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs.
    School of Computer Science, Carnegie Mellon University, CMU-CS-11-111, 2011.
    [bib | ⧉ | pdf | CADE]

    Logic is a powerful tool for analyzing and verifying systems, including programs, discrete systems, real-time 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

    
    
    
18. Sarah M. Loos, André Platzer and Ligia Nistor.
    Adaptive Cruise Control:
       Hybrid, Distributed, and Now Formally Verified.
    School of Computer Science, Carnegie Mellon University, CMU-CS-11-107, 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 cyber-physical 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 on-ramps or multi-lane streets. The system we present is in many ways one of the most complicated cyber-physical systems that has ever been fully verified formally.

    Keywords: distributed car control • multi-agent systems • highway traffic safety • formal verification • distributed hybrid systems • adaptive cruise control

    
    
    
19. André Platzer.
    Quantified Differential Dynamic Logic for Distributed Hybrid Systems.
    School of Computer Science, Carnegie Mellon University, CMU-CS-10-126, 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 dimensionality-changes. 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

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

    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 non-Bayesian 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 discrete-time 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 state-of-the-art 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.

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

    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

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

    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

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

    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 state-of-the-art techniques, even when no prior knowledge is available.

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

    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 real-world 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 real-closed 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: real-closed fields • decision procedures • hybrid systems • software verification

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

    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 cyber-physical transportation systems pose particularly demanding challenges for future research in formal analysis techniques.

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

    We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations whose right-hand 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

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

    We introduce a first-order 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 first-order 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

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

    We combine first-order 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 first-order 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 non-temporal 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

1. 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 cyber-physical 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 runtime-monitored 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 • Cyber-physical systems • Formal verification • Runtime model validation • Monitor synthesis • Differential dynamic logic

   
   
   
2. Sarah M. Loos and André Platzer.
   Teaching cyber-physical systems with logic.
   Draft, 2014.
   [bib | ⧉ | pdf | course]

   This paper reports on a course breaking with the myth that cyber-physical systems are too challenging to be taught at the undergraduate level. Cyber-physical systems (CPSs) such as computer-controlled 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 Cyber-Physical Systems, that teaches students how to design a correct CPS, identify required safety properties, and justify that their designs meet these safety goals.

   Keywords:  Cyber-physical systems • Education • Hybrid systems • Using theorem provers in education • Differential dynamic logic

   
   
   
3. 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 first-order 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 first-order 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 safety-critical 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

   
   
   

Copyright of publications is with the publisher or author as indicated. Author's versions of papers are posted with permission of the publisher for your personal use. Not for redistribution or commercial purpose. Slides are copyright © by the author. All information and materials on this site are provided solely for informational purposes on an AS-IS basis, and any and all implied warranties are expressly disclaimed.