Differential-algebraic Dynamic Logic for Differential-algebraic Programs

DOI10.1093/logcom/exn070zbMath1191.03024OpenAlexW2130705439MaRDI QIDQ3406693

André Platzer

Publication date: 19 February 2010

Published in: Journal of Logic and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1093/logcom/exn070

zbMATH Keywords

theorem provingsequent calculusdynamic logicair traffic controlverification of hybrid systemsdifferential constraintsdifferential induction

Mathematics Subject Classification ID

Logic in computer science (03B70) Traffic problems in operations research (90B20) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Differential Game Logic ⋮ Verification of Hybrid Systems ⋮ A Uniform Substitution Calculus for Differential Dynamic Logic ⋮ Quantified Differential Temporal Dynamic Logic for Verifying Properties of Distributed Hybrid Systems ⋮ A compositional modelling and verification framework for stochastic hybrid systems ⋮ Formal Modelling, Analysis and Verification of Hybrid Systems ⋮ Exact safety verification of hybrid systems using sums-of-squares representation ⋮ Change-of-bases abstractions for non-linear hybrid systems ⋮ From post-conditions to post-region invariants ⋮ A program logic to verify signal temporal logic specifications of hybrid systems ⋮ A Two-Way Path Between Formal and Informal Design of Embedded Systems ⋮ A complete uniform substitution calculus for differential dynamic logic ⋮ KeYmaera: A Hybrid Theorem Prover for Hybrid Systems (System Description) ⋮ An axiomatic approach to existence and liveness for differential equations ⋮ Programming with Infinitesimals: A While-Language for Hybrid System Modeling ⋮ A hierarchy of proof rules for checking positive invariance of algebraic and semi-algebraic sets ⋮ ModelPlex: verified runtime validation of verified cyber-physical system models ⋮ Loop invariants ⋮ Stochastic Differential Dynamic Logic for Stochastic Hybrid Programs ⋮ Direct Formal Verification of Liveness Properties in Continuous and Hybrid Dynamical Systems ⋮ Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application ⋮ A formal framework for Hybrid Event B ⋮ \(\mathsf{dL}_{\iota}\): definite descriptions in differential dynamic logic ⋮ Synthesizing Switching Controllers for Hybrid Systems by Generating Invariants ⋮ Constructive hybrid games ⋮ A Roadmap to Decidability

Uses Software

• QEPCAD
• KeYmaera