From Idea to Provably Safe Implementation
Modeling, Proving, Simulation, and Synthesis in KeYmaera X
The verification tool KeYmaera has been used in the verification of several cyberphysical system (CPS) applications, including the Airborne Collision Avoidance System ACAS X, the European Train Control System ETCS, several automotive systems, mobile robot navigation with the dynamic window algorithm, and a surgical robotic system for skullbase surgery . Its successor, KeYmaera X, expands upon functionality by providing easier ways of augmenting the automatic proof capabilities and by providing proofbased code synthesis. KeYmaera X is also based on a significantly smaller soundnesscritical core than all other hybrid systems verification tools, which makes it easier to ensure correct verification results. 
KeYmaera X
or CPSWEEK tutorial or Slides 
Objectives
This tutorial will explain how hybrid system theorem proving in KeYmaera X can be used as a powerful technique to analyze and design safe cyberphysical systems. We will illustrate how developers can benefit from KeYmaera X by demonstrating on a series of examples how it can be used to:
 model cyberphysical systems
 express safety/correctness properties
 find bugs in a system design
 identify safety constraints
 identify system invariants
 fully verify the final system design
 write automated tactics for (sub)systems that serve as "unit proofs", in analogy to unit tests
 derive new products from a verified system design and refine a system design while retaining correctness proofs
 automatically synthesize correct monitors from the system design, which can be used as test cases or as runtime monitors to check compliance of observed behavior with the verified model
Topics
The tutorial will introduce the modeling language, proof techniques, and synthesis tools of KeYmaera X . We will present techniques for analyzing both discrete and continuous parts of a model, such as differential invariants for differential equations Along the way, we will convey the intuition behind proof techniques for differential equations such as Lyapunov functions or differential invariants.
Throughout the tutorial, we will use a ground robot as a running example. The tutorial will start with simple tasks that KeYmaera X can prove fully automatically (e.g., drive a robot in a straight line to a charging station and stop there) and progress to more complicated models where manual interaction or advanced proof techniques become necessary (e.g., proving properties about a trajectory generator).
Participants will learn how to model hybrid systems using hybrid programs, how to avoid modeling pitfalls, and how to prove safety properties (e.g., that the robot never collides with walls or never runs past the charging station). To explore safety verification concepts we will interact with KeYmaera X through its pointandclick web interface. We will then demonstrate how these manual pointandclick proofs can be automated using the tactics programming language. Tactics provide a powerful way of automating either generic or domainspecific proof search procedures for cases that are out of reach for the proof strategies that already ship with KeYmaera X.
Synthesis
Once a hybrid system is proved correct, the remaining question is whether or not the model used for verification adequately represents the real system and its environment. We will show participants how to use the ModelPlex proof tactic implemented in KeYmaera X to synthesize provably correct monitor expressions, which test the running system for deviation from the verified model. When run alongside controllers on the real system as watchdogs, these monitors initiate emergency actions on deviation to keep the system safe in a provably correct way.
The tutorial will feature practical handson tutoring and exercises done online using the web interface of KeYmaera X. Participants are invited to also bring their own computers with a web browser if they are seeking to gain handson experience in hybrid systems proving.
Content and Objectives
In an exampledriven style, the tutorial will introduce the background, modeling, and proof techniques of KeYmaera X for formally verifying safety properties of hybrid systems. The emphasis in the tutorial is put on intuition grounded in insightful examples with generalizable takeaway messages. The tutorial is accompanied by a companion tutorial article for easy reference after the conference, a book and indepth course material from an undergraduate course held at Carnegie Mellon University.
Outcomes
Participants will: learn how to model systems with hybrid programs and how to simulate models in KeYmaera X
 learn how to prove models with KeYmaera X both automatically and manually
 learn how to interpret counterexamples and find bugs in models
 learn how to use proof techniques, such as differential invariants, to prove properties of nonlinear differential equations
 learn how to use KeYmaera X to find correct switching conditions for a controller
 learn how to write tactics for steering the proof search of KeYmaera X
 learn how to turn a model into a safetyensuring runtime monitor.
Lecturer Short Biographies




