Bellerophon: tactical theorem proving for hybrid systems

DOI10.1007/978-3-319-66107-0_14zbMath1483.68191OpenAlexW2747477340MaRDI QIDQ1687737

Stefan Mitsch, Nathan Fulton, Brandon Bohrer, André Platzer

Publication date: 4 January 2018

Full work available at URL: https://doi.org/10.1007/978-3-319-66107-0_14

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (8)

Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL ⋮ Pegasus: sound continuous invariant generation ⋮ Verifying Switched System Stability With Logic ⋮ \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic ⋮ Verifiably safe exploration for end-to-end reinforcement learning ⋮ Deductive stability proofs for ordinary differential equations ⋮ An axiomatic approach to existence and liveness for differential equations ⋮ Bellerophon

Uses Software

• Coq
• Isabelle/HOL
• KeYmaera
• PHAVer
• MetaPRL
• SpaceEx
• Coquelicot
• Lean
• dReach
• ModelPlex

Cites Work

• Unnamed Item
• ModelPlex: verified runtime validation of verified cyber-physical system models
• Hybrid systems
• Computing differential invariants of hybrid systems as fixed points
• Differential dynamic logic for hybrid systems
• Real quantifier elimination is doubly exponential
• Partial cylindrical algebraic decomposition for quantifier elimination
• Isabelle/HOL. A proof assistant for higher-order logic
• A complete uniform substitution calculus for differential dynamic logic
• Coquelicot: a user-friendly library of real analysis for Coq
• The Flow of ODEs
• Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems
• Logics of Dynamical Systems
• The Lean Theorem Prover (System Description)
• KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
• Logical Analysis of Hybrid Systems
• Real World Verification
• Computer Certified Efficient Exact Reals in Coq
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• Theorem Proving in Higher Order Logics

This page was built for publication: Bellerophon: tactical theorem proving for hybrid systems