KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems

DOI10.1007/978-3-319-21401-6_36zbMath1465.68281OpenAlexW1590463358MaRDI QIDQ3454120

Marcus Völp, André Platzer, Jan-David Quesel, Nathan Fulton, Stefan Mitsch

Publication date: 2 December 2015

Published in: Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL: https://figshare.com/articles/journal_contribution/KeYmaera_X_An_Axiomatic_Tactical_Theorem_Prover_for_Hybrid_Systems/6606683

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Hybrid systems of ordinary differential equations (34A38) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (26)

A mechanically verified theory of contracts ⋮ Skill-Based Verification of Cyber-Physical Systems ⋮ Implicit semi-algebraic abstraction for polynomial dynamical systems ⋮ Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL ⋮ Verification of Hybrid Systems ⋮ Pegasus: sound continuous invariant generation ⋮ The refinement calculus of reactive systems ⋮ Bellerophon: tactical theorem proving for hybrid systems ⋮ Reusable contracts for safe integration of reinforcement learning in hybrid systems ⋮ Verifying Switched System Stability With Logic ⋮ On proving that an unsafe controller is not proven safe ⋮ \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic ⋮ From post-conditions to post-region invariants ⋮ A program logic to verify signal temporal logic specifications of hybrid systems ⋮ Verifiably safe exploration for end-to-end reinforcement learning ⋮ Quantitative Robustness Analysis of Sensor Attacks on Cyber-Physical Systems ⋮ A complete uniform substitution calculus for differential dynamic logic ⋮ Deductive stability proofs for ordinary differential equations ⋮ Rigorous Simulation-Based Analysis of Linear Hybrid Systems ⋮ An axiomatic approach to existence and liveness for differential equations ⋮ ModelPlex: verified runtime validation of verified cyber-physical system models ⋮ Verified interactive computation of definite integrals ⋮ \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic ⋮ Uniform substitution at one Fell swoop ⋮ Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants ⋮ Implicit definitions with differential equations for KeYmaera X (system description)

Uses Software

• Coq
• Isabelle/HOL
• KeYmaera
• KeY
• KeYmaera X

Cites Work

• Differential dynamic logic for hybrid systems
• Isabelle/HOL. A proof assistant for higher-order logic
• Logics of Dynamical Systems
• A Uniform Substitution Calculus for Differential Dynamic Logic
• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
• Logical Analysis of Hybrid Systems
• Tactic theorem proving with refinement-tree proofs and metavariables
• Differential Game Logic

This page was built for publication: KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems