Sciweavers

Share
CADE
2015
Springer

KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems

3 years 10 months ago
KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
KeYmaera X is a theorem prover for differential dynamic logic (dL), 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 dL 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 th...
Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Ma
Added 17 Apr 2016
Updated 17 Apr 2016
Type Journal
Year 2015
Where CADE
Authors Nathan Fulton, Stefan Mitsch, Jan-David Quesel, Marcus Völp, André Platzer
Comments (0)
books