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

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

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)

Cites Work

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

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
• IsaVODEs: Interactive verification of cyber-physical systems at scale
• Title not available (Why is that?)
• UTP, \textsf{\textit{Circus}}, and Isabelle
• Programming Languages and Systems

Uses Software

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

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)