Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs

DOI10.1007/978-3-031-38499-8_6MaRDI QIDQ6492733zbMATH OpenFDO

Authors Stefan Mitsch, André Platzer

Publication date 26 April 2024

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-031-38499-8_6

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic
• A complete uniform substitution calculus for differential dynamic logic
• A Proof System for Communicating Sequential Processes
• A proof technique for communicating sequential processes
• A UTP semantics for communicating processes with shared variables and its formal encoding in PVS
• Algebras for program correctness in Isabelle/HOL
• An assume/guarantee based compositional calculus for hybrid CSP
• An axiomatic proof technique for parallel programs
• Communicating sequential processes
• Compositional Hoare-style reasoning about hybrid CSP in the duration calculus
• Concurrency verification. Introduction to compositional and noncompositional methods
• Differential dynamic logic for hybrid systems
• Differential equation invariance axiomatization
• Differential game logic
• FDR3 -- a modern refinement checker for CSP
• First-order dynamic logic
• scientific article; zbMATH DE number 3122413 (Why is no real title available?)
• scientific article; zbMATH DE number 3890715 (Why is no real title available?)
• scientific article; zbMATH DE number 3903940 (Why is no real title available?)
• scientific article; zbMATH DE number 3068536 (Why is no real title available?)
• KeYmaera X: an axiomatic tactical theorem prover for hybrid systems
• Proofs of Networks of Processes
• SPHIN: a model checker for reconfigurable hybrid systems based on SPIN
• The Rely-Guarantee method for verifying shared variable concurrent programs
• Uniform substitution at one Fell swoop
• Uniform substitution for differential game logic
• Verification of sequential and concurrent programs

Cited in

(2)

• Modular analysis of distributed hybrid systems using post-regions
• Uniform substitution for differential refinement logic

This page was built for publication: Uniform Substitution for Dynamic Logic with Communicating Hybrid Programs

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