|
|
⇓ Download ⇓
or get Source and read Book and watch Videos and follow Tutorial |
Quickly
Announcements
- KeYmaera X 5.1 quality release with usability, system compatibility and simplicity advances.
- KeYmaera X 5 major release with definition package for user-defined functions, major parser rewrite, keyboard shortcuts during proofs, tactic performance improvements, and tool improvements. (release notes)
- Tool paper KeYmaera X implicit function definitions at IJCAR 2022
- KeYmaera X 4.9 major release with restructured tactic framework and module separation. Model organization, shortcut notation in user definitions, improved support for starting and checking lemmas. (release notes)
- KeYmaera X 4.8 major release with more speed, more automation, restructured and reviewed microkernel, user definitions and more.
- New KeYmaera X Tutorial for learning KeYmaera X
- Best Tool Paper Award at FM 2019 was awarded for Pegasus, the continuous invariant generator for KeYmaera X
- FM 2019 Tutorial on KeYmaera X: Modular Formal Verification of Cyber-Physical Systems with KeYmaera X
- Video lectures: Logical Foundations of Cyber-Physical Systems
- Textbook: Logical Foundations of Cyber-Physical Systems, Springer, 2018
Overview
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 and hybrid games theorem prover, KeYmaera X analyzes the control program and the physical behavior of the controlled system together.
KeYmaera X features a minimal microkernel of just 2000 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.
- ⇓ Download KeYmaera X to your computer (installation instructions)
- Get KeYmaera X Source to contribute
Summary
KeYmaera X is a theorem prover for
KeYmaera X is built up from a small trusted core. The core contains a finite list of locally sound dL axioms that are instantiated using a uniform substitution proof rule. Isolating all soundness-critical reasoning in this axiomatic core obviates the otherwise intractable task of ensuring that proof search algorithms are implemented correctly. This enables advanced proof search features---such as aggressive, speculative proof search and user-defined tactics built using a flexible tactic language---without correctness concerns that could undermine the usefulness of automated analysis. KeYmaera X demonstrates that tactics on top of the axiomatic core provide a rich language for implementing novel and highly sophisticated automatic proof procedures.
Case Studies
These are a few of the many other case studies that have been verified in KeYmaera X: |
 |
Other case studies are reported in the corresponding publications.
Quick Usage
Also get quick usage help any time with the ? menu button in KeYmaera X.
Also see: KeYmaera X Usage Overview Video
 |
Any opinions, findings, and conclusions or recommendations expressed are those of the author(s) and do not necessarily reflect the views of any sponsoring institution.