KeYmaera X Tutorial

KeYmaera X Tutorial

An ultra short synopsis of what you'll need to keep handy about the KeYmaera X Prover for Hybrid Systems is on the KeYmaera X Cheat Sheet.

A great practical way to learn how to use the KeYmaera X Prover for Hybrid Systems is via the KeYmaera X Tutorial:

  1. Differential Dynamic Logic in KeYmaera X
  2. Hybrid Programs in KeYmaera X
  3. Proofs in KeYmaera X
  4. Differential Equation Proofs in KeYmaera X
  5. User Tutorial Videos for KeYmaera X
PDF Version of KeYmaera X Tutorial for download

Cheat Sheet or
X Tutorial or
Videos

Books

The most comprehensive and readable background on the differential dynamic logic that the KeYmaera X Prover for Hybrid Systems provides can be found in the Textbook: Logical Foundations of Cyber-Physical Systems. Additional theory can be found in the Book: Logical Analysis of Hybrid Systems. Those books do not cover KeYmaera X specifically, though.

Textbook or
Book or
Videos