The Complete Proof Theory of Hybrid Systems

DOI10.1109/LICS.2012.64MaRDI QIDQ2986831zbMATH OpenWikidataFDO

Authors André Platzer

Publication date 16 May 2017

Published in 2012 27th Annual IEEE Symposium on Logic in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1109/LICS.2012.64

zbMATH Keywords

proof theorycompletenessaxiomatizationhybrid dynamical systemsdifferential dynamic logic

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Specification and verification (program logics, model checking, etc.) (68Q60) Hybrid systems of ordinary differential equations (34A38) Other applications of logic (03B80)

Recommendations

• Theorem proving with built-in hybrid theories
• Hybrid logic and its proof-theory
• Hybrid Systems: From Verification to Falsification
• A compositional approach to the verification of hybrid systems
• Hybrid Logics with Infinitary Proof Systems
• Verifying hybrid systems with modal Kleene algebra
• Hybrid diagrams: a deductive-algorithmic approach to hybrid system verification

Cited in

(26)

• A deductive approach towards reasoning about algebraic transition systems
• Logical analysis of hybrid systems: a complete answer to a complexity challenge
• Implicit definitions with differential equations for KeYmaera X (system description)
• Skill-based verification of cyber-physical systems
• \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic
• Relational differential dynamic logic
• Generating semi-algebraic invariants for non-autonomous polynomial hybrid systems
• scientific article; zbMATH DE number 2000403 (Why is no real title available?)
• Formally-verified round-off error analysis of Runge-Kutta methods
• A Survey on Analog Models of Computation
• Deductive stability proofs for ordinary differential equations
• A uniform substitution calculus for differential dynamic logic
• A complete uniform substitution calculus for differential dynamic logic
• KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description)
• Proof-Based Approach to Hybrid Systems Development: Dynamic Logic and Event-B
• Logical analysis of hybrid systems. A complete answer to a complexity challenge
• Generating invariants for non-linear hybrid systems
• Pegasus: sound continuous invariant generation
• Modular analysis of distributed hybrid systems using post-regions
• Verification of Hybrid Systems
• From post-conditions to post-region invariants
• Axiomatization of compact initial value problems: open properties
• Pegasus: a framework for sound continuous invariant generation
• Parallel composition and modular verification of computer controlled systems in differential dynamic logic
• ModelPlex: verified runtime validation of verified cyber-physical system models
• Differential game logic

This page was built for publication: The Complete Proof Theory of Hybrid Systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2986831)