A Uniform Substitution Calculus for Differential Dynamic Logic

DOI10.1007/978-3-319-21401-6_32zbMath1465.03056arXiv1503.01981OpenAlexW1941921537MaRDI QIDQ3454116

André Platzer

Publication date: 2 December 2015

Published in: Automated Deduction - CADE-25 (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1503.01981

Mathematics Subject Classification ID

Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Mechanization of proofs and logical operations (03B35) Hybrid systems of ordinary differential equations (34A38)

Related Items (7)

Differential Game Logic ⋮ A Uniform Substitution Calculus for Differential Dynamic Logic ⋮ KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems ⋮ Verifiably safe exploration for end-to-end reinforcement learning ⋮ A complete uniform substitution calculus for differential dynamic logic ⋮ ModelPlex: verified runtime validation of verified cyber-physical system models ⋮ A Survey on Analog Models of Computation

Uses Software

• KeYmaera

Cites Work

• Unnamed Item
• Unnamed Item
• An error analysis of least-squares finite element method of velocity- pressure-vorticity formulation for Stokes problem
• The Complete Proof Theory of Hybrid Systems
• Differential-algebraic Dynamic Logic for Differential-algebraic Programs
• A Uniform Substitution Calculus for Differential Dynamic Logic
• 50 Years of Integer Programming 1958-2008
• Differential Game Logic
• Banishing the rule of substitution for functional variables

This page was built for publication: A Uniform Substitution Calculus for Differential Dynamic Logic