Differential Ghosts

Jump to bottom Edit New page

André Platzer edited this page Oct 15, 2018 · 3 revisions

This page contains a list of resources for using differential ghosts in KeYmaera X.

Chapter 12 of the textbook Logical Foundations of Cyber-Physical Systems.
Lecture notes and recitation notes from older FCPS course
Reasoning about Exponential Decay and Growth in KeYmaera X.
Another tutorial-style example of differential cuts & ghosts.
The extended example from the Bellerophon paper contains an example of differential ghosts.

The KeYmaera X Theorem Prover for Hybrid Systems