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

DOI10.1007/978-3-030-43520-2_11MaRDI QIDQ5098720zbMATH OpenOpenAlexFDO

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

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, https://eprints.whiterose.ac.uk/155734/1/hybrid_kat.pdf

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Recommendations

• Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
• Differential Refinement Logic
• Differential dynamic logic for hybrid systems
• Verifying hybrid systems with modal Kleene algebra
• Differential Logic for Reasoning About Hybrid Systems

Cites work

• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• scientific article; zbMATH DE number 1086671 (Why is no real title available?)
• Algebras of modal operators and partial correctness
• Building program construction and verification tools from algebraic principles
• Differential Refinement Logic
• Hoare semigroups
• Hybrid relations in Isabelle/UTP
• Logical foundations of cyber-physical systems
• Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
• On Hoare logic and Kleene algebra with tests
• Ordinary differential equations and dynamical systems
• Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
• Refinement Calculus
• Taming multirelations
• The flow of ODEs: formalization of variational equation and Poincaré map
• Type classes and filters for mathematical analysis in Isabelle/HOL
• Unifying heterogeneous state-spaces with lenses
• Verification of Hybrid Systems

Cited in

(10)

• An axiomatic approach to existence and liveness for differential equations
• 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
• Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
• Integration of formal proof into unified assurance cases with Isabelle/SACM
• scientific article; zbMATH DE number 2110621 (Why is no real title available?)
• IsaVODEs: Interactive verification of cyber-physical systems at scale
• UTP, \textsf{\textit{Circus}}, and Isabelle
• Programming Languages and Systems

Describes a project that uses

Uses Software

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

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

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