Visible to the public The KeYmaera X Theorem Prover for Hybrid Systems

Submitted by krogh on Mon, 12/21/2015 - 4:47pm. Contributor:

Abstract:

KeYmaera X is a theorem prover for specifying and verifying correctness properties of hybrid systems (systems that mix discrete and continuous dynamics). KeYmaera X implements differential dynamic logic (dL) and provides a high degree of control over automated proof search.

License: 
Creative Commons 2.5

Other available formats:

The KeYmaera X Theorem Prover for Hybrid Systems
Switch to experimental viewer