Bellerophon: tactical theorem proving for hybrid systems
type: Item
instance of: scholarly article
title: Bellerophon: tactical theorem proving for hybrid systems
zbMATH Open document ID: 1483.68191
DOI: 10.1007/978-3-319-66107-0_14
author: Nathan Fulton
author: Stefan Mitsch
author: Brandon Bohrer
author: André Platzer
publication date: 2018-01-04T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68V15
Mathematics Subject Classification ID: 93C30
zbMATH DE Number: 6821853
describes a project that uses: Coq
describes a project that uses: MetaPRL
describes a project that uses: dReach
describes a project that uses: Coquelicot
describes a project that uses: Lean
describes a project that uses: Isabelle/HOL
describes a project that uses: ModelPlex
describes a project that uses: KeYmaera
describes a project that uses: PHAVer
describes a project that uses: SpaceEx
MaRDI profile type: Publication
full work available at URL: 978-3-319-66107-0 14
OpenAlex ID: W2747477340
cites work: The Lean Theorem Prover (System Description)
cites work: Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems
cites work: Coquelicot: a user-friendly library of real analysis for Coq
cites work: Q5417200
cites work: Partial cylindrical algebraic decomposition for quantifier elimination
cites work: Real quantifier elimination is doubly exponential
cites work: KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
cites work: Hybrid systems
cites work: Theorem Proving in Higher Order Logics
cites work: Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
cites work: The Flow of ODEs
cites work: Computer Certified Efficient Exact Reals in Coq
cites work: ModelPlex: verified runtime validation of verified cyber-physical system models
cites work: Isabelle/HOL. A proof assistant for higher-order logic
cites work: Differential dynamic logic for hybrid systems
cites work: Logical Analysis of Hybrid Systems
cites work: Logics of Dynamical Systems
cites work: A complete uniform substitution calculus for differential dynamic logic
cites work: Computing differential invariants of hybrid systems as fixed points
cites work: KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
cites work: Real World Verification
description: scientific article; zbMATH DE number 6821853