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

Book Chapters

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. Springer, 2017.
[bib  doi  book]Hybrid systems are models with joint discrete and continuous behavior. They occur frequently in safetycritical applications in various domains such as health care, transportation, and robotics, as a result of interactions between a digital controller and a physical environment. They also have relevance in other areas such as systems biology, in which the discrete dynamics arises as an abstraction of fast continuous processes. One of the prominent models is that of hybrid automata, where differential equations are associated with each node, and jump constraints such as guards and resets are associated with each edge.
In this chapter, we focus on the problem of model checking of hybrid automata against reachability and invariance properties, enabling the techniques for the verification of general temporal logic specifications. We review the main decidability results for hybrid automata, and since modelchecking is in general undecidable, we present three complementary analysis approaches based on symbolic representations, abstraction, and logic. In particular, we illustrate polyhedronbased reachability analysis, finite quotients, abstraction refinement techniques, and logicbased verification. We survey important tools and application domains of successful hybrid system verification in this vibrant area of research.
Journal Publications

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

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

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

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

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

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

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

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

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

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

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

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

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

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

André Platzer.
The structure of differential invariants and differential cut elimination.
Logical Methods in Computer Science, 8(4), pp. 138, 2012. © The author
[bib  pdf  doi  eprint  arXiv]The biggest challenge in hybrid systems verification is the handling of differential equations. Because computable closedform solutions only exist for very simple differential equations, proof certificates have been proposed for more scalable verification. Search procedures for these proof certificates are still rather adhoc, though, because the problem structure is only understood poorly. We investigate differential invariants, which define an induction principle for differential equations and which can be checked for invariance along a differential equation just by using their differential structure, without having to solve them. We study the structural properties of differential invariants. To analyze tradeoffs for proof search complexity, we identify more than a dozen relations between several classes of differential invariants and compare their deductive power. As our main results, we analyze the deductive power of differential cuts and the deductive power of differential invariants with auxiliary differential variables. We refute the differential cut elimination hypothesis and show that, unlike standard cuts, differential cuts are fundamental proof principles that strictly increase the deductive power. We also prove that the deductive power increases further when adding auxiliary differential variables to the dynamics.
Keywords: proof theory • differential equations • differential invariants • differential cut elimination • differential dynamic logic • hybrid systems • logics of programs • real differential semialgebraic geometry

André Platzer and Edmund M. Clarke.
Computing differential invariants of hybrid systems as fixedpoints.
Formal Methods in System Design, 35(1), pp. 98120, 2009.
Special issue for selected papers from CAV'08. © SpringerVerlag
[bib  pdf  doi  study  CAV'08]We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations whose righthand sides are polynomials in the state variables. In order to verify nontrivial systems without solving their differential equations and without numerical errors, we use a continuous generalization of induction, for which our algorithm computes the required differential invariants. As a means for combining local differential invariants into global system invariants in a sound way, our fixedpoint algorithm works with a compositional verification logic for hybrid systems. With this compositional approach we exploit locality in system designs. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively with differential invariants until safety becomes provable. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification procedure. We verify roundabout maneuvers in air traffic management and collision avoidance in train control and car control.
Keywords: verification of hybrid systems • differential invariants • verification logic • fixedpoint engine

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

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

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, International conference on reliability, safety and security of railway systems: modelling, analysis, verification and certification  RSSRail, volume 10598 of LNCS. Springer, 2017. © SpringerVerlag
[bib  pdf  doi]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#160;X.
Keywords: Train control safety • Braking model verification • Performance analysis • Hybrid systems • Differential dynamic logic

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

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

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

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

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

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

Andrew Sogokon, Khalil Ghorbal, Paul B. Jackson and André Platzer.
A method for invariant generation for polynomial continuous systems.
In Barbara Jobstmann and K. Rustan M. Leino, editors, Verification, Model Checking, and Abstract Interpretation  17th International Conference, VMCAI 2016, St. Petersburg, Florida, USA, January 1719, 2016, Proceedings, volume 9583 of LNCS, pp. 268288. Springer, 2016. © SpringerVerlag
[bib  pdf  doi  study]This paper presents a method for generating semialgebraic invariants for systems governed by nonlinear polynomial ordinary differential equations under semialgebraic evolution constraints. Based on the notion of discrete abstraction, our method eliminates unsoundness and unnecessary coarseness found in existing approaches for computing abstractions for nonlinear continuous systems and is able to construct invariants with intricate boolean structure, in contrast to invariants typically generated using templatebased methods. In order to tackle the state explosion problem associated with discrete abstraction, we present invariant generation algorithms that exploit sound proof rules for safety verification, such as differential cut (DC), and a new proof rule that we call differential divideandconquer (DDC), which splits the verification problem into smaller subproblems. The resulting invariant generation method is observed to be much more scalable and efficient than the naïve approach, exhibiting orders of magnitude performance improvement on many of the problems.
Keywords: Continuous systems • Differential equations • Invariant generation • Formal safety verification • Hybrid systems

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

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

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

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

Khalil Ghorbal, Andrew Sogokon, and André Platzer.
A hierarchy of proof rules for checking differential invariance of algebraic sets.
In Deepak D'Souza, Akash Lal, and Kim Guldstrand Larsen, editors, Verification, Model Checking, and Abstract Interpretation  16th International Conference, VMCAI 2015, Mumbai, India, January 1214, 2015, Proceedings, volume 8931 of LNCS, pp. 431448. Springer, 2015. © SpringerVerlag
[bib  pdf  doi  slides  study  ComLan'17]This paper presents a theoretical and experimental comparison of sound proof rules for proving invariance of algebraic sets, that is, sets satisfying polynomial equalities, under the flow of polynomial ordinary differential equations. Problems of this nature arise in formal verification of continuous and hybrid dynamical systems, where there is an increasing need for methods to expedite formal proofs. We study the tradeoff between proof rule generality and practical performance and evaluate our theoretical observations on a set of heterogeneous benchmarks. The relationship between increased deductive power and running time performance of the proof rules is far from obvious; we discuss and illustrate certain classes of problems where this relationship is interesting.
Keywords: Inductive invariants • Theorem proving • Deductive power of proof rules • Dynamical and hybrid systems

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

Khalil Ghorbal, Andrew Sogokon, and André Platzer.
Invariance of conjunctions of polynomial equalities for algebraic differential equations.
In Markus MüllerOlm and Helmut Seidl, editors, 21st International Static Analysis Symposium, volume 8723 of LNCS, pp. 151167. Springer, 2014. © SpringerVerlag
[bib  pdf  doi  study]In this paper we seek to provide greater automation for formal deductive verification tools working with continuous and hybrid dynamical systems. We present an efficient procedure to check invariance of conjunctions of polynomial equalities under the flow of polynomial ordinary differential equations. The procedure is based on a necessary and sufficient condition that characterizes invariant conjunctions of polynomial equalities. We contrast this approach to an alternative one which combines fast and sufficient (but not necessary) conditions using differential cuts for soundly restricting the system evolution domain.
Keywords: Checking algebraic invariance • Algebraic differential equations • Theorem proving • Continuous systems • Hybrid systems verification

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

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

Khalil Ghorbal and André Platzer.
Characterizing algebraic invariants by differential radical invariants.
In Erika Ábrahám and Klaus Havelund, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2014, Proceedings, volume 8413 of LNCS, pp. 279294. Springer, 2014. © SpringerVerlag
[bib  pdf  doi  slides  study  TR]We prove that any invariant algebraic set of a given polynomial vector field can be algebraically represented by one polynomial and a finite set of its successive Lie derivatives. This socalled differential radical characterization relies on a sound abstraction of the reachable set of solutions by the smallest variety that contains it. The characterization leads to a differential radical invariant proof rule that is sound and complete, which implies that invariance of algebraic equations over realclosed fields is decidable. Furthermore, the problem of generating invariant varieties is shown to be as hard as minimizing the rank of a symbolic matrix, and is therefore NPhard. We investigate symbolic linear algebra tools based on Gaussian elimination to efficiently automate the generation. The approach can, e.g., generate nontrivial algebraic invariant equations capturing the airplane behavior during takeoff or landing in longitudinal motion.
Keywords: Algebraic invariants • Differential ideals • Higherorder Lie derivation • Differential invariants • Differential equations • Invariant generation

Sarah M. Loos, David Witmer, Peter Steenkiste and André Platzer.
Efficiency analysis of formally verified adaptive cruise controllers.
In Andreas Hegyi and Bart De Schutter, editors, 16th International IEEE Conference on Intelligent Transportation Systems, ITSC'13, The Hague, Netherlands, Proceedings, 2013. © IEEE
[bib  pdf  doi  slides  study]We consider an adaptive cruise control system in which control decisions are made based on position and velocity information received from other vehicles via V2V wireless communication. If the vehicles follow each other at a close distance, they have better wireless reception but collisions may occur when a follower car does not receive notice about the decelerations of the leader car fast enough to react before it is too late. If the vehicles are farther apart, they would have a bigger safety margin, but the wireless communication drops out more often, so that the follower car no longer receives what the leader car is doing. In order to guarantee safety, such a system must return control to the driver if it does not receive an update from a nearby vehicle within some timeout period. The value of this timeout parameter encodes a tradeoff between the likelihood that an update is received and the maximum safe acceleration. Combining formal verification techniques for hybrid systems with a wireless communication model, we analyze how the expected efficiency of a provablysafe adaptive cruise control system is affected by the value of this timeout.
Keywords: Traffic theory for ITS • Network modeling • Driver assistance systems • V2V wireless communication • Hybrid systems • Formal verification

Stefan Mitsch, Khalil Ghorbal and André Platzer.
On provably safe obstacle avoidance for autonomous robotic ground vehicles.
In Paul Newman, Dieter Fox, and David Hsu, editors, Robotics: Science and Systems, 2013. © The author
[bib  pdf  slides  study  eprint  talk]Nowadays, robots interact more frequently with a dynamic environment outside limited manufacturing sites and in close proximity with humans. Thus, safety of motion and obstacle avoidance are vital safety features of such robots. We formally study two safety properties of avoiding both stationary and moving obstacles: (i) passive safety, which ensures that no collisions can happen while the robot moves, and (ii) the stronger passive friendly safety in which the robot further maintains sufficient maneuvering distance for obstacles to avoid collision as well. We use hybrid system models and formal verification techniques that describe and formally verify the robot's discrete control decisions along with its continuous, physical motion. Moreover, we formally prove that safety can still be guaranteed despite location and actuator uncertainty.
Keywords: autonomous robotics obstacle avoidance • formal verification • hybrid systems • dynamic window approach

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

Yanni Kouskoulas, David W. Renshaw, André Platzer and Peter Kazanzides.
Certifying the safe design of a virtual fixture control algorithm for a surgical robot.
In Calin Belta and Franjo Ivancic, editors, Hybrid Systems: Computation and Control (part of CPS Week 2013), HSCC'13, Philadelphia, PA, USA, April 813, 2013, pp. 263272. ACM, 2013. © ACM
[bib  pdf  doi  study]We applied quantified differentialdynamic logic (QdL) to analyze a control algorithm designed to provide directional force feedback for a surgical robot. We identified problems with the algorithm, proved that it was in general unsafe, and described exactly what could go wrong. We then applied QdL to guide the development of a new algorithm that provides safe operation along with directional force feedback. Using KeYmaeraD (a tool that mechanizes QdL), we created a machinechecked proof that guarantees the new algorithm is safe for all possible inputs.
Keywords: quantified differential dynamic logic • medical robotics • formal verification

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

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

JanDavid Quesel and André Platzer.
Playing hybrid games with KeYmaera.
In Bernhard Gramlich, Dale Miller and Ulrike Sattler, editors, Automated Reasoning, 6th International Joint Conference, IJCAR'12, Manchester, UK, Proceedings, volume 7364 of LNCS, pp. 439453. Springer, 2012. © SpringerVerlag
[bib  pdf  doi  study]We propose a new logic, called differential dynamic game logic (dDGL), that adds several game constructs on top of differential dynamic logic (dL) so that it can be used for hybrid games. The logic dDGL is a conservative extension of dL, which we exploit for our implementation of dDGL in the theorem prover KeYmaera. We provide rules for extending the dL sequent proof calculus to handle the dDGL constructs by identifying analogs to operators of dL. We have implemented dDGL in an extension of KeYmaera and verified a case study in which a robot satisfies a joint safety and liveness objective in a factory automation scenario, in which the factory may perform interfering actions independently.
Keywords: differential dynamic logic • hybrid games • sequent calculus • theorem proving • logics for hybrid systems • factory automation

André Platzer.
The complete proof theory of hybrid systems.
ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pp. 541550. IEEE 2012. © IEEE
[bib  pdf  doi  slides  TR]Hybrid systems are a fusion of continuous dynamical systems and discrete dynamical systems. They freely combine dynamical features from both worlds. For that reason, it has often been claimed that hybrid systems are more challenging than continuous dynamical systems and than discrete systems. We now show that, prooftheoretically, this is not the case. We present a complete prooftheoretical alignment that interreduces the discrete dynamics and the continuous dynamics of hybrid systems. We give a sound and complete axiomatization of hybrid systems relative to continuous dynamical systems and a sound and complete axiomatization of hybrid systems relative to discrete dynamical systems. Thanks to our axiomatization, proving properties of hybrid systems is exactly the same as proving properties of continuous dynamical systems and again, exactly the same as proving properties of discrete dynamical systems. This fundamental cornerstone sheds light on the nature of hybridness and enables flexible and provably perfect combinations of discrete reasoning with continuous reasoning that lift to all aspects of hybrid systems and their fragments.
Keywords: proof theory • hybrid dynamical systems • differential dynamic logic • axiomatization • completeness

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

Stefan Mitsch, Sarah M. Loos and André Platzer.
Towards formal verification of freeway traffic control.
In Chenyang Lu, editor, ACM/IEEE Third International Conference on CyberPhysical Systems, Beijing, China, April 1719. pp. 171180, IEEE. 2012. © IEEE
[bib  pdf  doi  slides  study]We study how CPS technology can help improve freeway traffic by combining local car GPS positioning, traffic center control decisions, and communication to achieve more tightly coupled feedback control in intelligent speed adaptation. We develop models for an intelligent speed adaptation that respects variable speed limit control and incident management. We identify safe ranges for crucial design parameters in these systems and, using the theorem prover KeYmaera, formally verify safety of the resulting CPS models. Finally, we show how those parameter ranges can be used to decide tradeoffs for practical system implementations even for design parameters that are not modeled formally.
Keywords: freeway traffic control • intelligent speed adaptation • hybrid system

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

Sarah M. Loos and André Platzer.
Safe intersections: At the crossing of hybrid systems and verification.
In Kyongsu Yi, editor, 14th International IEEE Conference on Intelligent Transportation Systems, ITSC'11, Washington, DC, USA, Proceedings, pp. 11811186. 2011. © IEEE
[bib  pdf  doi  slides  study]Intelligent vehicle systems have interesting prospects for solving inefficiencies and risks in ground transportation, e.g., by making cars aware of their environment and regulating speed intelligently. If the computer control technology reacts fast enough, intelligent control can be used to increase the density of cars on the streets. The technology may also help prevent crashes at intersections, which cost the US $97 Billion in the year 2000. The crucial prerequisite for intelligent vehicle control, however, is that it must be correct, for it may otherwise do more harm than good. Formal verification techniques provide the best reliability guarantees but have had difficulties in the past with scaling to such complex systems. We report our successes with a logical approach to hybrid systems verification, which can capture discrete control decisions and continuous driving dynamics. We present a model for the interaction of two cars and a traffic light at a two lane intersection and verify with a formal proof that our system always ensures collision freedom and that our controller always prevents cars from running red lights.

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

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

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

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

Sarah M. Loos, André Platzer and Ligia Nistor.
Adaptive cruise control: Hybrid, distributed, and now formally verified.
In Michael Butler and Wolfram Schulte, editors, 17th International Symposium on Formal Methods, FM, Limerick, Ireland, Proceedings, volume 6664 of LNCS, pp. 4256. Springer, 2011. © SpringerVerlag
[bib  pdf  doi  slides  study  TR]Car safety measures can be most effective when the cars on a street coordinate their control actions using distributed cooperative control. While each car optimizes its navigation planning locally to ensure the driver reaches his destination, all cars coordinate their actions in a distributed way in order to minimize the risk of safety hazards and collisions. These systems control the physical aspects of car movement using cyber technologies like local and remote sensor data and distributed V2V and V2I communication. They are thus cyberphysical systems. In this paper, we consider a distributed car control system that is inspired by the ambitions of the California PATH project, the CICAS system, SAFESPOT and PReVENT initiatives. We develop a formal model of a distributed car control system in which every car is controlled by adaptive cruise control. One of the major technical difficulties is that faithful models of distributed car control have both distributed systems and hybrid systems dynamics. They form distributed hybrid systems, which makes them very challenging for verification. In a formal proof system, we verify that the control model satisfies its main safety objective and guarantees collision freedom for arbitrarily many cars driving on a street, even if new cars enter the lane from onramps or multilane streets. The system we present is in many ways one of the most complicated cyberphysical systems that has ever been fully verified formally.
Keywords: distributed car control • multiagent systems • highway traffic safety • formal verification • distributed hybrid systems • adaptive cruise control

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

André Platzer.
Quantified differential invariants.
In Emilio Frazzoli and Radu Grosu, editors, Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, USA, April 1214, pp. 6372. ACM, 2011. © ACM
[bib  pdf  doi  slides]We address the verification problem for distributed hybrid systems with nontrivial dynamics. Consider air traffic collision avoidance maneuvers, for example. Verifying dynamic appearance of aircraft during an ongoing collision avoidance maneuver is a longstanding and essentially unsolved problem. The resulting systems are not hybrid systems and their state space is not of the form R^n. They are distributed hybrid systems with nontrivial continuous and discrete dynamics in distributed state spaces whose dimension and topology changes dynamically over time. We present the first formal verification technique that can handle the complicated nonlinear dynamics of these systems. We introduce quantified differential invariants, which are properties that can be checked for invariance along the dynamics of the distributed hybrid system based on differentiation, quantified substitution, and quantifier elimination in realclosed fields. This gives a computationally attractive technique, because it works without having to solve the infinitedimensional differential equation systems underlying distributed hybrid systems. We formally verify a roundabout maneuver in which aircraft can appear dynamically.
Keywords: distributed hybrid systems • verification logic • quantified differential equations • quantified differential invariants

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

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

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

André Platzer and Edmund M. Clarke.
Formal verification of curved flight collision avoidance maneuvers: A case study.
In Ana Cavalcanti and Dennis Dams, editors, 16th International Symposium on Formal Methods, FM, Eindhoven, Netherlands, Proceedings, volume 5850 of LNCS, pp. 547562. Springer, 2009. © SpringerVerlag
This paper was awarded the FM Best Paper Award.
[bib  pdf  doi  slides  study  TR]Aircraft collision avoidance maneuvers are important and complex applications. Curved flight exhibits nontrivial continuous behavior. In combination with the control choices during air traffic maneuvers, this yields hybrid systems with challenging interactions of discrete and continuous dynamics. As a case study illustrating the use of a new proof assistant for a logic for nonlinear hybrid systems, we analyze collision freedom of roundabout maneuvers in air traffic control, where appropriate curved flight, good timing, and compatible maneuvering are crucial for guaranteeing safe spatial separation of aircraft throughout their flight. We show that formal verification of hybrid systems can scale to curved flight maneuvers required in aircraft control applications. We introduce a fully flyable variant of the roundabout collision avoidance maneuver and verify safety properties by compositional verification.
Keywords: formal verification of hybrid systems • deduction • air traffic control • logic for hybrid systems

Sumit Kumar Jha, Edmund Clarke, Christopher Langmead, Axel Legay, André Platzer and Paolo Zuliani.
A Bayesian approach to model checking biological systems.
In Pierpaolo Degano and Roberto Gorrieri, editors, Computational Methods in Systems Biology, 7th International Conference, CMSB 2009, Bologna, Italy, Proceedings, volume 5688 of LNCS, pp. 218234. Springer, 2009. © SpringerVerlag
[bib  pdf  doi  TR]Recently, there has been considerable interest in the use of Model Checking for Systems Biology. Unfortunately, the state space of stochastic biological models is often too large for classical Model Checking techniques. For these models, a statistical approach to Model Checking has been shown to be an effective alternative. Extending our earlier work, we present the first algorithm for performing statistical Model Checking using Bayesian Sequential Hypothesis Testing. We show that our Bayesian approach outperforms current statistical Model Checking techniques, which rely on tests from Classical (aka Frequentist) statistics, by requiring fewer system simulations. Another advantage of our approach is the ability to incorporate prior Biological knowledge about the model being verified. We demonstrate our algorithm on a variety of models from the Systems Biology literature and show that it enables faster verification than stateoftheart techniques, even when no prior knowledge is available.

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

André Platzer and Edmund M. Clarke.
Computing differential invariants of hybrid systems as fixedpoints.
In Aarti Gupta and Sharad Malik, editors, Computer Aided Verification, CAV 2008, Princeton, USA, Proceedings, volume 5123 of LNCS, pp. 176189, Springer, 2008. © SpringerVerlag
[bib  pdf  doi  slides  study  TR  FMSD'09]We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations whose righthand sides are polynomials in the state variables. In order to verify nontrivial systems without solving their differential equations and without numerical errors, we use a continuous generalization of induction, for which our algorithm computes the required differential invariants. As a means for combining local differential invariants into global system invariants in a sound way, our fixedpoint algorithm works with a compositional verification logic for hybrid systems. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively with differential invariants until safety becomes provable. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification procedure. We verify roundabout maneuvers in air traffic management and collision avoidance in train control.
Keywords: verification of hybrid systems • differential invariants • verification logic • fixedpoint engine

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

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

André Platzer and Edmund M. Clarke.
The image computation problem in hybrid systems model checking.
In Alberto Bemporad, Antonio Bicchi and Giorgio Buttazzo, editors, Hybrid Systems: Computation and Control, 10th International Conference, HSCC 2007, Pisa, Italy, Proceedings, volume 4416 of LNCS, pp. 473486. Springer, 2007, © SpringerVerlag
[bib  pdf  doi  slides  tool]In this paper, we analyze limits of approximation techniques for (nonlinear) continuous image computation in model checking hybrid systems. In particular, we show that even a single step of continuous image computation is not semidecidable numerically even for a very restricted class of functions. Moreover, we show that symbolic insight about derivative bounds provides sufficient additional information for approximation refinement model checking. Finally, we prove that purely numerical algorithms can perform continuous image computation with arbitrarily high probability. Using these results, we analyze the prerequisites for a safe operation of the roundabout maneuver in air traffic collision avoidance.
Keywords: model checking • hybrid systems • image computation

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

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

André Platzer and JanDavid Quesel.
KeYmaera: A hybrid theorem prover for hybrid systems.
In Alessandro Armando, Peter Baumgartner and Gilles Dowek, editors, Automated Reasoning, Fourth International Joint Conference, IJCAR 2008, Sydney, Australia, Proceedings, volume 5195 of LNCS, pp. 171178. Springer, 2008. © SpringerVerlag
[bib  pdf  doi  slides  tool]KeYmaera is a hybrid verification tool for hybrid systems that combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive theorem prover for a natural specification and verification logic for hybrid systems. KeYmaera supports differential dynamic logic, which is a realvalued firstorder dynamic logic for hybrid programs, a program notation for hybrid automata. For automating the verification process, KeYmaera implements a generalized freevariable sequent calculus and automatic proof strategies that decompose the hybrid system specification symbolically. To overcome the complexity of real arithmetic, we integrate real quantifier elimination following an iterative background closure strategy. Our tool is particularly suitable for verifying parametric hybrid systems and has been used successfully for verifying collision avoidance in case studies from train control and air traffic management.
Keywords: dynamic logic • automated theorem proving • decision procedures • computer algebra • verification of hybrid systems

André Platzer and JanDavid Quesel.
Logical verification and systematic parametric analysis in train contro.
In Magnus Egerstedt and Bud Mishra, editors, Hybrid Systems: Computation and Control, 11th International Conference, HSCC 2008, St. Louis, USA, Proceedings, volume 4981 of LNCS, pp. 646649. Springer, 2008. © SpringerVerlag
[bib  pdf  doi  poster]We formally verify hybrid safety properties of cooperation protocols in a fully parametric version of the European Train Control System (ETCS). We present a formal model using hybrid programs and verify correctness using our logicbased decomposition procedure. This procedure supports free parameters and parameter discovery, which is required to determine correct design choices for free parameters of ETCS.
Keywords: parametric verification • logic for hybrid systems • symbolic decomposition

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

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

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

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

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

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

Stephanie Kemper and André Platzer.
SATbased abstraction refinement for realtime systems.
In Frank S. de Boer and Vladimir Mencl, editors, Formal Aspects of Component Software, Third International Workshop, FACS 2006, Prague, Czech Republic, Proceedings, Electr. Notes Theor. Comput. Sci., 182:107122, 2007
[bib  pdf  doi  slides  tool]In this paper, we present an abstraction refinement approach for model checking safety properties of realtime systems using SATsolving. We present a faithful embedding of bounded model checking for systems of timed automata into propositional logic with linear arithmetic and prove correctness. With this logical representation, we achieve a linearsize representation of parallel composition and introduce a quick abstraction technique that works uniformly for clocks, events, and states. When necessary, abstractions are refined by analysing spurious counterexamples using a promising extension of counterexampleguided abstraction refinement with syntactic information about Craig interpolants. To support generalisations, our overall approach identifies the algebraic and logical principles required for logicbased abstraction refinement.
Keywords: abstraction refinement • model checking • realtime systems • SAT • Craig interpolation

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

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

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

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

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

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

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

André Platzer.
A differential operator approach to equational differential invariants.
In Lennart Beringer and Amy Felty, editors, Interactive Theorem Proving, International Conference, ITP 2012, August 1315, Princeton, USA, Proceedings, volume 7406 of LNCS, pp. 2848. Springer, 2012. © SpringerVerlag
Invited paper.
[bib  pdf  doi  slides]Hybrid systems, i.e., dynamical systems combining discrete and continuous dynamics, have a complete axiomatization in differential dynamic logic relative to differential equations. Differential invariants are a natural induction principle for proving properties of the remaining differential equations. We study the equational case of differential invariants using a differential operator view. We relate differential invariants to Lie's seminal work and explain important structural properties resulting from this view. Finally, we study the connection of differential invariants with partial differential equations in the context of the inverse characteristic method for computing differential invariants.
Keywords: differential dynamic logic • differential invariants • differential equations • hybrid systems

André Platzer.
Logics of dynamical systems.
ACM/IEEE Symposium on Logic in Computer Science, LICS 2012, June 25–28, 2012, Dubrovnik, Croatia, pp. 1324. IEEE 2012. © IEEE
Invited paper.
[bib  pdf  doi  slides]We study the logic of dynamical systems, that is, logics and proof principles for properties of dynamical systems. Dynamical systems are mathematical models describing how the state of a system evolves over time. They are important in modeling and understanding many applications, including embedded systems and cyberphysical systems. In discrete dynamical systems, the state evolves in discrete steps, one step at a time, as described by a difference equation or discrete state transition relation. In continuous dynamical systems, the state evolves continuously along a function, typically described by a differential equation. Hybrid dynamical systems or hybrid systems combine both discrete and continuous dynamics.
This is a brief survey of differential dynamic logic for specifying and verifying properties of hybrid systems. We explain hybrid system models, differential dynamic logic, its semantics, and its axiomatization for proving logical formulas about hybrid systems. We study differential invariants, i.e., induction principles for differential equations. We briefly survey theoretical results, including soundness and completeness and deductive power. Differential dynamic logic has been implemented in automatic and interactive theorem provers and has been used successfully to verify safetycritical applications in automotive, aviation, railway, robotics, and analogue electrical circuits.
Keywords: logic of dynamical systems • dynamic logic • differential dynamic logic • hybrid systems • axiomatization • deduction

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

Sarah M. Loos and André Platzer.
Safe intersections: At the crossing of hybrid systems and verification.
In Kyongsu Yi, editor, 14th International IEEE Conference on Intelligent Transportation Systems, ITSC'11, Washington, DC, USA, Proceedings, pp. 11811186. 2011. © IEEE
[bib  pdf  doi  slides  study]Intelligent vehicle systems have interesting prospects for solving inefficiencies and risks in ground transportation, e.g., by making cars aware of their environment and regulating speed intelligently. If the computer control technology reacts fast enough, intelligent control can be used to increase the density of cars on the streets. The technology may also help prevent crashes at intersections, which cost the US $97 Billion in the year 2000. The crucial prerequisite for intelligent vehicle control, however, is that it must be correct, for it may otherwise do more harm than good. Formal verification techniques provide the best reliability guarantees but have had difficulties in the past with scaling to such complex systems. We report our successes with a logical approach to hybrid systems verification, which can capture discrete control decisions and continuous driving dynamics. We present a model for the interaction of two cars and a traffic light at a two lane intersection and verify with a formal proof that our system always ensures collision freedom and that our controller always prevents cars from running red lights.

André Platzer.
Logic and compositional verification of hybrid systems.
In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification, CAV 2011, Snowbird, UT, USA, Proceedings, volume 6806 of LNCS, pp. 2843. Springer, 2011. © SpringerVerlag
Invited tutorial.
[bib  pdf  doi  slides]Hybrid systems are models for complex physical systems and have become a widely used concept for understanding their behavior. Many applications are safetycritical, including car, railway, and air traffic control, robotics, physicalchemical process control, and biomedical devices. Hybrid systems analysis studies how we can build computerised controllers for physical systems which are guaranteed to meet their design goals. The continuous dynamics of hybrid systems can be modeled by differential equations, the discrete dynamics by a combination of discrete statetransitions and conditional execution. The discrete and continuous dynamics interact to form hybrid systems, which makes them quite challenging for verification.
In this tutorial, we survey stateoftheart verification techniques for hybrid systems. In particular, we focus on a coherent logical approach for systematic hybrid systems analysis. We survey theory, practice, and applications, and show how hybrid systems can be verified in the hybrid systems verification tool KeYmaera. KeYmaera has been used successfully to verify safety, reactivity, controllability, and liveness properties, including collision freedom in air traffic, car, and railway control systems. It has also been used to verify properties of electrical circuits.

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

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

Werner Damm, Alfred Mikschl, Jens Oehlerking, ErnstRüdiger Olderog, Jun Pang, André Platzer, Marc Segelken and Boris Wirtz.
Automating verification of cooperation, control, and design in traffic applications.
In Cliff Jones, Zhiming Liu and Jim Woodcock, editors, Formal Methods and Hybrid RealTime Systems, volume 4700 of LNCS, pp. 115169. Springer, 2007. © SpringerVerlag
Invited paper.
[bib  pdf  doi]We present a verification methodology for cooperating traffic agents covering analysis of cooperation strategies, realization of strategies through control, and implementation of control. For each layer, we provide dedicated approaches to formal verification of safety and stability properties of the design. The range of employed verification techniques invoked to span this verification space includes application of preverified design patterns, automatic synthesis of Lyapunov functions, constraint generation for parameterized designs, modelchecking in rich theories, and abstraction refinement. We illustrate this approach with a variant of the European Train Control System (ETCS), employing layer specific verification techniques to layer specific views of an ETCS design.
Reports

André Platzer and Yong Kiam Tan.
How to Prove "All" Differential Equation Properties.
School of Computer Science, Carnegie Mellon University, CMUCS17117, 2017.
[bib  pdf]

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

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

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

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

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

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

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

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

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

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

André Platzer.
The Complete Proof Theory of Hybrid Systems.
School of Computer Science, Carnegie Mellon University, CMUCS11144, November 2011.
[bib  pdf  LICS'12]Hybrid systems are a fusion of continuous dynamical systems and discrete dynamical systems. They freely combine dynamical features from both worlds. For that reason, it has often been claimed that hybrid systems are more challenging than continuous dynamical systems and than discrete systems. We now show that, prooftheoretically, this is not the case. We present a complete prooftheoretical alignment that interreduces the discrete dynamics and the continuous dynamics of hybrid systems. We give a sound and complete axiomatization of hybrid systems relative to continuous dynamical systems and a sound and complete axiomatization of hybrid systems relative to discrete dynamical systems. Thanks to our axiomatization, proving properties of hybrid systems is exactly the same as proving properties of continuous dynamical systems and again, exactly the same as proving properties of discrete dynamical systems. This fundamental cornerstone sheds light on the nature of hybridness and enables flexible and provably perfect combinations of discrete reasoning with continuous reasoning that lift to all aspects of hybrid systems and their fragments.
Keywords: proof theory • hybrid dynamical systems • differential dynamic logic • axiomatization • completeness

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

André Platzer.
The Structure of Differential Invariants and Differential Cut Elimination.
School of Computer Science, Carnegie Mellon University, CMUCS11112, April 2011.
[bib  pdf  arXiv  LMCS'12]The biggest challenge in hybrid systems verification is the handling of differential equations. Because computable closedform solutions only exist for very simple differential equations, proof certificates have been proposed for more scalable verification. Search procedures for these proof certificates are still rather adhoc, though, because the problem structure is only understood poorly. We investigate differential invariants, which define an induction principle for differential equations and which can be checked for invariance along a differential equation just by using their differential structure, without having to solve them. We study the structural properties of differential invariants. To analyze tradeoffs for proof search complexity, we identify more than a dozen relations between several classes of differential invariants and compare their deductive power. As our main results, we analyze the deductive power of differential cuts and the deductive power of differential invariants with auxiliary differential variables. We refute the differential cut elimination hypothesis and show that, unlike standard cuts, differential cuts are fundamental proof principles that strictly increase the deductive power. We also prove that the deductive power increases further when adding auxiliary differential variables to the dynamics.
Keywords: proof theory • differential equations • differential invariants • differential cut elimination • differential dynamic logic • hybrid systems • logics of programs • real differential semialgebraic geometry

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

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

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

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

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

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

Sumit Kumar Jha, Edmund Clarke, Christopher Langmead, Axel Legay, André Platzer and Paolo Zuliani.
A Bayesian Approach to Model Checking Biological Systems.
School of Computer Science, Carnegie Mellon University, CMUCS09110, 2009.
[bib  pdf  CMSB'09]Recently, there has been considerable interest in the use of Model Checking for Systems Biology. Unfortunately, the state space of stochastic biological models is often too large for classical Model Checking techniques. For these models, a statistical approach to Model Checking has been shown to be an effective alternative. Extending our earlier work, we present the first algorithm for performing statistical Model Checking using Bayesian Sequential Hypothesis Testing. We show that our Bayesian approach outperforms current statistical Model Checking techniques, which rely on tests from Classical (aka Frequentist) statistics, by requiring fewer system simulations. Another advantage of our approach is the ability to incorporate prior Biological knowledge about the model being verified. We demonstrate our algorithm on a variety of models from the Systems Biology literature and show that it enables faster verification than stateoftheart techniques, even when no prior knowledge is available.

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

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

André Platzer and Edmund M. Clarke.
Computing Differential Invariants of Hybrid Systems as Fixedpoints.
School of Computer Science, Carnegie Mellon University, CMUCS08103, Feb, 2008.
[bib  pdf  CAV'08]We introduce a fixedpoint algorithm for verifying safety properties of hybrid systems with differential equations whose righthand sides are polynomials in the state variables. In order to verify nontrivial systems without solving their differential equations and without numerical errors, we use a continuous generalization of induction, for which our algorithm computes the required differential invariants. As a means for combining local differential invariants into global system invariants in a sound way, our fixedpoint algorithm works with a compositional verification logic for hybrid systems. To improve the verification power, we further introduce a saturation procedure that refines the system dynamics successively with differential invariants until safety becomes provable. By complementing our symbolic verification algorithm with a robust version of numerical falsification, we obtain a fast and sound verification procedure. We verify roundabout maneuvers in air traffic management and collision avoidance in train control.
Keywords: verification of hybrid systems • differential invariants • verification logic • fixedpoint engine

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

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

André Platzer.
Foundations of CyberPhysical Systems.
Lecture Notes, Computer Science Department, Carnegie Mellon University. 2017.
[bib  course]Cyberphysical systems (CPSs) combine cyber effects (computation and/or communication) with physical effects (motion or other physical processes). Designing algorithms to control CPSs, such as those in cars, aircraft and robots, is challenging due to their tight coupling with physical behavior. At the same time, it is vital that these algorithms be correct, since we rely on CPSs for safetycritical tasks like keeping aircraft from colliding. Students in this course will understand the core principles behind CPSs, develop models and controls, identify safety specifications and critical properties of CPSs, understand abstraction and system architectures, learn how to design by invariant, reason rigorously about CPS models, verify CPS models of appropriate scale, understand the semantics of a CPS model and develop an intuition for operational effects. Students will write hybrid programs (HPs), which capture relevant dynamical aspects of CPSs in a simple programming language with a simple semantics, allowing the programmer to refer to realvalued variables representing real quantities and specify their dynamics as part of the HP.

André Platzer.
Foundations of CyberPhysical Systems.
Lecture Notes, Computer Science Department, Carnegie Mellon University. 2016.
[bib  pdf  course]Cyberphysical systems (CPSs) combine cyber effects (computation and/or communication) with physical effects (motion or other physical processes). Designing algorithms to control CPSs, such as those in cars, aircraft and robots, is challenging due to their tight coupling with physical behavior. At the same time, it is vital that these algorithms be correct, since we rely on CPSs for safetycritical tasks like keeping aircraft from colliding. Students in this course will understand the core principles behind CPSs, develop models and controls, identify safety specifications and critical properties of CPSs, understand abstraction and system architectures, learn how to design by invariant, reason rigorously about CPS models, verify CPS models of appropriate scale, understand the semantics of a CPS model and develop an intuition for operational effects. Students will write hybrid programs (HPs), which capture relevant dynamical aspects of CPSs in a simple programming language with a simple semantics, allowing the programmer to refer to realvalued variables representing real quantities and specify their dynamics as part of the HP.

André Platzer.
Foundations of CyberPhysical Systems.
Lecture Videos, Computer Science Department, Carnegie Mellon University. 2016.
[bib  slides  videos]Cyberphysical systems (CPSs) combine cyber effects (computation and/or communication) with physical effects (motion or other physical processes). Designing algorithms to control CPSs, such as those in cars, aircraft and robots, is challenging due to their tight coupling with physical behavior. At the same time, it is vital that these algorithms be correct, since we rely on CPSs for safetycritical tasks like keeping aircraft from colliding. Students in this course will understand the core principles behind CPSs, develop models and controls, identify safety specifications and critical properties of CPSs, understand abstraction and system architectures, learn how to design by invariant, reason rigorously about CPS models, verify CPS models of appropriate scale, understand the semantics of a CPS model and develop an intuition for operational effects. Students will write hybrid programs (HPs), which capture relevant dynamical aspects of CPSs in a simple programming language with a simple semantics, allowing the programmer to refer to realvalued variables representing real quantities and specify their dynamics as part of the HP.

André Platzer.
Foundations of CyberPhysical Systems.
Lecture Notes, Computer Science Department, Carnegie Mellon University. 2014.
[bib  pdf  course]Cyberphysical systems (CPSs) combine cyber effects (computation and/or communication) with physical effects (motion or other physical processes). Designing algorithms to control CPSs, such as those in cars, aircraft and robots, is challenging due to their tight coupling with physical behavior. At the same time, it is vital that these algorithms be correct, since we rely on CPSs for safetycritical tasks like keeping aircraft from colliding. Students in this course will understand the core principles behind CPSs, develop models and controls, identify safety specifications and critical properties of CPSs, understand abstraction and system architectures, learn how to design by invariant, reason rigorously about CPS models, verify CPS models of appropriate scale, understand the semantics of a CPS model and develop an intuition for operational effects. Students will write hybrid programs (HPs), which capture relevant dynamical aspects of CPSs in a simple programming language with a simple semantics, allowing the programmer to refer to realvalued variables representing real quantities and specify their dynamics as part of the HP.

André Platzer.
Foundations of CyberPhysical Systems.
Lecture Notes, Computer Science Department, Carnegie Mellon University. 2013.
[bib  pdf  course]Cyberphysical systems (CPSs) combine cyber effects (computation and/or communication) with physical effects (motion or other physical processes). Designing algorithms to control CPSs, such as those in cars, aircraft and robots, is challenging due to their tight coupling with physical behavior. At the same time, it is vital that these algorithms be correct, since we rely on CPSs for safetycritical tasks like keeping aircraft from colliding. Students in this course will understand the core principles behind CPSs, develop models and controls, identify safety specifications and critical properties of CPSs, understand abstraction and system architectures, learn how to design by invariant, reason rigorously about CPS models, verify CPS models of appropriate scale, understand the semantics of a CPS model and develop an intuition for operational effects. Students will write hybrid programs (HPs), which capture relevant dynamical aspects of CPSs in a simple programming language with a simple semantics, allowing the programmer to refer to realvalued variables representing real quantities and specify their dynamics as part of the HP.
Drafts

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

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

Annika Peterson.
Formal Verification of a Controlled Flight Between Two Robots: A Case Study.
Senior Thesis, Carnegie Mellon University, Department of Computer Science. May 2015.
Allen Newell Award for Excellence in Undergraduate Research and 2nd place in the Boeing Blue Skies Competition with special mention for ``Most Creative'' project.
[bib  pdf  study]Robots moving within controlled flight paths are complex systems that require formal verification of collision avoidance. A flight path dependent upon a coded program requires confidence of its ability to avoid crashing, which we show with a formal proof. Inspired by the controlled flight of two robots within the DisneyPixar film WALL·E, we have designed a controller for a robot flying within a complex controlled flight path, a helix with another robot. We have formally proven collision avoidance within the proof rules of differential dynamic logic, a logic for hybrid systems consisting of discrete controlled steps and continuous physics, using a deductive verification tool, KeYmaera, when this flight path is viewed in two dimensions as well as three dimensions. We formally prove safety as well as an additional property that the two robots are within some delta of each other. This case study also applies to aircraft collision avoidance and unmanned aerial vehicles where unsafe operation is potentially fatal and similar 3D motion is relevant.

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

André Platzer.
An Objectoriented Dynamic Logic with Updates.
Master's Thesis, University of Karlsruhe, Department of Computer Science. Institute for Logic, Complexity and Deduction Systems, September 2004.
Short version appeared as Dynamic logic with nonrigid functions: A basis for objectoriented program verification at IJCAR 2006.
[bib  pdf  slides]With the goal of this thesis being to create a dynamic logic for objectoriented languages, ODL is developed along with a sound and relatively complete calculus. The dynamic logic contains only the absolute logical essentials of objectorientation, yet still allows a ``natural'' representation of all other features of common objectoriented programming languages. ODL is an extension of a dynamic logic for imperative While programs by function modification and dynamic type checks. A generalisation of substitutions, called updates, constitute the central technical device for dealing with object aliasing arising from function modification and for retaining a manageable calculus in practical application scenarios. Further, object enumerators realise object creation in a natural yet powerful way. Finally, completeness is proven relative to firstorder arithmetic. Along with the soundness result, this proof constitutes the central part of this thesis and even copes with states containing uncomputable functions.

André Platzer.
Using a Program Verification Calculus for Constructing Specifications from Implementations.
Minor Thesis (Studienarbeit), University of Karlsruhe, Department of Computer Science. Institute for Logic, Complexity and Deduction Systems, February 2004.
[bib  pdf  slides]In this thesis we examine the possibility of automatically constructing the program specification from an implementation, both from a theoretical perspective and as a practical approach with a sequent calculus. As a setting for program specifications we choose dynamic logic for the Java programming language. We show thatdespite the undecidable nature of program analysisthe strongest specification of any program can always be constructed algorithmically. Further we outline a practical approach embedded into a sequent calculus for dynamic logic and with a higher focus on readability. Therefor, the central aspect of describing unbounded state changes incorporates the concept of modifies lists for expressing the modifiable portion of the state space. The underlying deductions are carried out by the theorem prover of the KeY System.