KeYmaera X

KeYmaera X

Description: Self-driving cars, autonomous robots, modern airplanes, or robotic surgery: we increasingly entrust our lives to computers and therefore should strive for nothing but the highest safety standards - mathematical correctness proof. Proofs for such cyber-physical systems can be constructed with the KeYmaera X prover. As a hybrid systems theorem prover, KeYmaera X analyzes the control program and the physical behavior of the controlled system together.

KeYmaera X features a minimal core of just 1700 lines of code that isolates all soundness-critical reasoning. Such a small and simple prover core makes it much easier to trust verification results. Pre-defined and custom tactics built on top of the core drive automated proof search. KeYmaera X comes with a web-based front-end that provides a clean interface for both interactive and automated proving, highlighting the most crucial parts of a verification activity.

VO Integration: No

Active: Yes

Available Benchmarks: Case studies can be found here and in some of these publications.

Website: http://www.ls.cs.cmu.edu/KeYmaeraX/

Download: Instructions here.

Documentation: Link

Contact: List of contributors.

Excerpt and graphics from: http://www.ls.cs.cmu.edu/KeYmaeraX/