KeYmaera X

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.


References in zbMATH (referenced in 13 articles )

Showing results 1 to 13 of 13.
Sorted by year (citations)

  1. Huerta y Munive, Jonathan Julián; Struth, Georg: Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL (2022)
  2. Preoteasa, Viorel; Dragomir, Iulia; Tripakis, Stavros: The refinement calculus of reactive systems (2022)
  3. Kastenbaum, Stéphane; Boyer, Benoît; Talpin, Jean-Pierre: A mechanically verified theory of contracts (2021)
  4. Sogokon, Andrew; Mitsch, Stefan; Tan, Yong Kiam; Cordwell, Katherine; Platzer, André: Pegasus: sound continuous invariant generation (2021)
  5. Tan, Yong Kiam; Platzer, André: An axiomatic approach to existence and liveness for differential equations (2021)
  6. Tan, Yong Kiam; Platzer, André: Deductive stability proofs for ordinary differential equations (2021)
  7. Xu, Runqing; Li, Liming; Zhan, Bohua: Verified interactive computation of definite integrals (2021)
  8. Sogokon, Andrew; Jackson, Paul B.; Johnson, Taylor T.: Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants (2019)
  9. Doyen, Laurent; Frehse, Goran; Pappas, George J.; Platzer, André: Verification of hybrid systems (2018)
  10. Bak, Stanley; Duggirala, Parasara Sridhar: Rigorous simulation-based analysis of linear hybrid systems (2017)
  11. Platzer, André: A complete uniform substitution calculus for differential dynamic logic (2017)
  12. Mitsch, Stefan; Platzer, André: ModelPlex: verified runtime validation of verified cyber-physical system models (2016)
  13. Fulton, Nathan; Mitsch, Stefan; Quesel, Jan-David; Völp, Marcus; Platzer, André: KeYmaera X: an axiomatic tactical theorem prover for hybrid systems (2015)