Tactics and Proofs
for Cyber-Physical Systems
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.
Proof Search
Learn techniques to turn the proof scripts from your interactive sessions into more general proof search procedures.
Lecturer Short Biographies
|
|
|
|
|
|