KeYmaera X

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 user-defined 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 soundness-critical 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; Isabelle/HOL; Bellerophon; SpaceEx; z3; ModelPlex; dReal; Coq; PVS; Simulink; MetiTarski; Flow*; LySHA; HSolver; Benchmarks; RSOLVER; HyTech; PHAVer; QEPCAD; VeriFast
Cited in: 28 Documents

Citations by Year