KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)

DOI10.1007/978-3-540-71070-7_15zbMath1165.68469OpenAlexW1535116423MaRDI QIDQ3541700

Jan-David Quesel, André Platzer

Publication date: 27 November 2008

Published in: Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-71070-7_15

zbMATH Keywords

computer algebradynamic logicautomated theorem provingdecision proceduresverification of hybrid systems

Mathematics Subject Classification ID

Related Items (32)

Verifying safety properties of a nonlinear control by interactive theorem proving with the prototype verification system ⋮ Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B ⋮ A heuristic prover for real inequalities ⋮ Deadness and how to disprove liveness in hybrid dynamical systems ⋮ Crossing the Bridge between Similar Games ⋮ Verification of Hybrid Systems ⋮ KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems ⋮ Pegasus: sound continuous invariant generation ⋮ Reachability analysis and simulation for hybridised Event-B models ⋮ ROSCoq: Robots Powered by Constructive Reals ⋮ Efficient choice of parameters on delta-reachability bounded hybrid systems ⋮ Bellerophon: tactical theorem proving for hybrid systems ⋮ \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic ⋮ A program logic to verify signal temporal logic specifications of hybrid systems ⋮ A system for compositional verification of asynchronous objects ⋮ A complete uniform substitution calculus for differential dynamic logic ⋮ Unnamed Item ⋮ An axiomatic approach to existence and liveness for differential equations ⋮ Programming with Infinitesimals: A While-Language for Hybrid System Modeling ⋮ ModelPlex: verified runtime validation of verified cyber-physical system models ⋮ Assume–guarantee verification of nonlinear hybrid systems with <scp>Ariadne</scp> ⋮ Reachability computation for polynomial dynamical systems ⋮ Using machine learning to improve cylindrical algebraic decomposition ⋮ Fixing Zeno gaps ⋮ Real World Verification ⋮ Theorem-proving analysis of digital control logic interacting with continuous dynamics ⋮ KeYmaera ⋮ Computing differential invariants of hybrid systems as fixed points ⋮ Verifying safety and persistence in hybrid systems using flowpipes and continuous invariants ⋮ Recent developments in theory and tool support for hybrid systems verification with \textsc{HyPro} ⋮ Enclosing the behavior of a hybrid automaton up to and beyond a Zeno point ⋮ Generating invariants for non-linear hybrid systems

Uses Software

• QEPCAD
• PHAVer
• HyTech
• Orbital library

Cites Work

• Unnamed Item
• Differential dynamic logic for hybrid systems
• Partial cylindrical algebraic decomposition for quantifier elimination
• Differential-algebraic Dynamic Logic for Differential-algebraic Programs
• Conflict resolution for air traffic management: a study in multiagent hybrid systems
• Differential Dynamic Logic for Verifying Parametric Hybrid Systems
• Hybrid Systems: Computation and Control

This page was built for publication: KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)