Differential Ghosts - LS-Lab/KeYmaeraX-release GitHub Wiki

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.