swMATH ID: 
40558

Software Authors: 
Fulton, N., Mitsch, S., Quesel, J., Völp, M., Platzer, A.

Description: 
KeYmaera X: an axiomatic tactical theorem prover for hybrid systems. KeYmaera X is a theorem prover for differential dynamic logic ( ), a logic for specifying and verifying properties of hybrid systems. Reasoning about complicated hybrid systems models requires support for sophisticated proof techniques, efficient computation, and a user interface that crystallizes salient properties of the system. KeYmaera X allows users to specify custom proof search techniques as tactics, execute these tactics in parallel, and interface with partial proofs via an extensible user interface. Advanced proof search features—and userdefined tactics in particular—are difficult to check for soundness. To admit extension and experimentation in proof search without reducing trust in the prover, KeYmaera X is built up from a small trusted kernel. The prover kernel contains a list of sound axioms that are instantiated using a uniform substitution proof rule. Isolating all soundnesscritical reasoning to this prover kernel obviates the intractable task of ensuring that each new proof search algorithm is implemented correctly. Preliminary experiments suggest that a single layer of tactics on top of the prover kernel provides a rich language for implementing novel and sophisticated proof search techniques. 
Homepage: 
https://keymaerax.org

Related Software: 
KeYmaera;
SpaceEx;
Isabelle/HOL;
Bellerophon;
MetiTarski;
Coq;
dReal;
ModelPlex;
dReach;
z3;
PVS;
Simulink;
Flow*;
LySHA;
CAPD;
HyTech;
PHAVer;
QEPCAD;
Zenon;
VeriPhy

Cited in: 
15 Publications
