The KeYmaera X Theorem Prover for Hybrid Systems

Download
pdf

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.

Tags:
License: CC-2.5
Submitted by Bruce Krogh on
Feedback
Feedback
If you experience a bug or would like to see an addition or change on the current page, feel free to leave us a message.
Image CAPTCHA
Enter the characters shown in the image.
This question is for testing whether or not you are a human visitor and to prevent automated spam submissions.