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; SpaceEx; Isabelle/HOL; Bellerophon; MetiTarski; Coq; dReal; ModelPlex; dReach; z3; PVS; Simulink; Flow*; LySHA; CAPD; HyTech; PHAVer; QEPCAD; Zenon; VeriPhy Cited in: 15 Publications Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year Implicit definitions with differential equations for KeYmaera X (system description). Zbl 07628218Gallicchio, James; Tan, Yong Kiam; Mitsch, Stefan; Platzer, André 2022 all top 5 Cited by 32 Authors 8 Platzer, André 4 Mitsch, Stefan 4 Tan, Yong Kiam 2 Sogokon, Andrew 1 Bak, Stanley 1 Boyer, Benoît 1 Cimatti, Alessandro 1 Cordwell, Katherine 1 Doyen, Laurent 1 Dragomir, Iulia 1 Duggirala, Parasara Sridhar 1 Frehse, Goran 1 Fulton, Nathan 1 Gallicchio, James 1 Griggio, Alberto 1 Huerta y Munive, Jonathan Julián 1 Irfan, Ahmed 1 Jackson, Paul B. 1 Johnson, Taylor T. 1 Kastenbaum, Stéphane 1 Li, Liming 1 Mover, Sergio 1 Pappas, George J. 1 Preoteasa, Viorel 1 Quesel, Jan-David 1 Struth, Georg 1 Talpin, Jean-Pierre 1 Tonetta, Stefano 1 Tripakis, Stavros 1 Völp, Marcus 1 Xu, Runqing 1 Zhan, Bohua Cited in 4 Serials 3 Journal of Automated Reasoning 2 Formal Methods in System Design 1 Information and Computation 1 Formal Aspects of Computing Cited in 4 Fields 15 Computer science (68-XX) 6 Mathematical logic and foundations (03-XX) 4 Ordinary differential equations (34-XX) 4 Systems theory; control (93-XX) Citations by Year