Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL

DOI10.1007/978-3-030-43520-2_11OpenAlexW3014009067MaRDI QIDQ5098720

Simon Foster, Georg Struth, Jonathan Julián Huerta y Munive

Publication date: 30 August 2022

Published in: Relational and Algebraic Methods in Computer Science (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Related Items (8)

Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL ⋮ Formally verified animation for RoboChart using interaction trees ⋮ \textsf{HHLPy}: practical verification of hybrid systems using Hoare logic ⋮ An axiomatic approach to existence and liveness for differential equations ⋮ UTP, \textsf{\textit{Circus}}, and Isabelle ⋮ Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving ⋮ IsaVODEs: Interactive verification of cyber-physical systems at scale ⋮ Integration of formal proof into unified assurance cases with Isabelle/SACM

Uses Software

• Unnamed Item
• Isabelle/UTP
• Archive Formal Proofs
• Ordinary Differential Equations
• Kleene Algebra
• Binary Multirelations
• Algebraic_VCs

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Building program construction and verification tools from algebraic principles
• Algebras of modal operators and partial correctness
• Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
• The flow of ODEs: formalization of variational equation and Poincaré map
• Hybrid relations in Isabelle/UTP
• Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
• Verification of Hybrid Systems
• Unifying Heterogeneous State-Spaces with Lenses
• Refinement Calculus
• Differential Refinement Logic
• Hoare Semigroups
• Logical Foundations of Cyber-Physical Systems
• Taming Multirelations
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
• On Hoare logic and Kleene algebra with tests

This page was built for publication: Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL