KeYmaera X FM 2016 Tutorial

Tactics and Proofs
for Cyber-Physical Systems

 

Table of Contents
  1. Modeling: What Kinds of Systems?
  2. Automated Proofs and Proof Inspection
  3. Interactive Proofs and Proof Programming
  4. Proof Search
  5. Lecturer Short Biographies

Cyber-physical systems that combine discrete and continuous dynamics are everywhere including automatic or semi-automatic controllers in modern (self-driving) cars, trains, airplanes, ground robots, robotic household appliances, or surgical robots. This tutorial will introduce the new theorem prover KeYmaera X to establish safety properties that reason about the interaction between software and the physical real world encountered in modern cyber-physical systems. You will learn how to model software together with physics and how to verify safety properties formally (e.g., a robot will not collide with obstacles).

KeYmaera X or
FM tutorial or
Slides

Modeling: What Kinds of Systems?

Differential dynamic logic has been used successfully for verification in railway, automotive, and aviation transportation systems, as well as for autonomous robotics, surgical robotics, and other systems.

Learn how to write hybrid programs that describe the interaction between software and physics as a program.

Automated Proofs and Proof Inspection

Use KeYmaera X tactics to find formal safety proofs for your models automatically. Inspect proofs and learn about differential dynamic logic from the interactive proving features of KeYmaera X. Combine proof automation and interactive proof-by-pointing to come up with elegant and concise proofs.

Interactive Proofs and Proof Programming

Watch KeYmaera X script your interactive proofs while you are clicking on how you want to decompose your system. Write your own proof scripts and experience how they interact with the graphical sequent proof view.

Initial conjecture is loaded
Extract assumptions
Split compound assumptions into single facts
Prove loops with induction
Get proof suggestions
Work on subproblems in context
Proved!

Proof Search

Learn techniques to turn the proof scripts from your interactive sessions into more general proof search procedures.

Lecturer Short Biographies

Nathan Fulton
Nathan is a Ph.D. student at Carnegie Mellon University. His research focuses on verification technology for cyber-physical systems and is a major developer of KeYmaera X.
Nathan Fulton
Stefan Mitsch
Stefan is a System Scientist at Carnegie Mellon University. His current research focuses on modeling, refactoring, verification, and monitoring methods for cyber-physical systems, and he contributed to ModelPlex and is a major developer of KeYmaera X.
Stefan Mitsch
André Platzer
André is an Associate Professor of Computer Science at Carnegie Mellon University. His interests include logic in computer science, cyber-physical systems, programming languages, formal methods, and automated theorem proving. He introduced differential dynamic logic and led the development of the KeYmaera and KeYmaera X provers for hybrid systems.
Andre Platzer