Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
type: Item
instance of: scholarly article
title: Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL
author: Jonathan Julián Huerta y Munive
author: Georg Struth
published in: Journal of Automated Reasoning
publication date: 2022-03-25T00:00:00Z
Mathematics Subject Classification ID: 68V15
zbMATH DE Number: 7498609
zbMATH Keywords: hybrid systems
zbMATH Keywords: predicate transformers
zbMATH Keywords: modal Kleene algebra
zbMATH Keywords: hybrid program verification
zbMATH Keywords: interactive theorem proving
describes a project that uses: Quantales
describes a project that uses: Transformer semantics
describes a project that uses: Bellerophon
describes a project that uses: Isabelle/HOL
describes a project that uses: KeYmaera
describes a project that uses: Coquelicot
describes a project that uses: Ordinary Differential Equations
describes a project that uses: KeYmaera X
describes a project that uses: C-CoRN
describes a project that uses: Algebraic_VCs
describes a project that uses: KAD
describes a project that uses: Differential_Game_Logic
describes a project that uses: RODAS
describes a project that uses: Archive Formal Proofs
describes a project that uses: Kleene Algebra
MaRDI profile type: Publication
full work available at URL: s10817-021-09607-x
OpenAlex ID: W3210385152
cites work: Q4433933
cites work: Building program construction and verification tools from algebraic principles
cites work: Q4003604
cites work: Refinement Calculus
cites work: Coquelicot: a user-friendly library of real analysis for Coq
cites work: Mathematical Knowledge Management
cites work: Internal axioms for domain semirings
cites work: Verification of Hybrid Systems
cites work: Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
cites work: Bellerophon: tactical theorem proving for hybrid systems
cites work: KeYmaera X: An Axiomatic Tactical Theorem Prover for Hybrid Systems
cites work: Q3898534
cites work: Modal Kleene algebra applied to program correctness
cites work: Solving Ordinary Differential Equations II
cites work: Q4525781
cites work: Q4067388
cites work: Type Classes and Filters for Mathematical Analysis in Isabelle/HOL
cites work: Affine systems of ODEs in Isabelle/HOL for hybrid-program verification
cites work: Verifying hybrid systems with modal Kleene algebra
cites work: Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL
cites work: The flow of ODEs: formalization of variational equation and Poincaré map
cites work: Q5270088
cites work: Boolean Algebras with Operators. Part I
cites work: Q4693151
cites work: The Picard Algorithm for Ordinary Differential Equations in Coq
cites work: Predicate Transformer Semantics
cites work: The Structure of Differential Invariants and Differential Cut Elimination
cites work: Logical Analysis of Hybrid Systems
cites work: A complete uniform substitution calculus for differential dynamic logic
cites work: Logical Foundations of Cyber-Physical Systems
cites work: Differential Equation Axiomatization
cites work: Algebra of Monotonic Boolean Transformers
cites work: Generating invariants for non-linear hybrid systems
cites work: Q4884543
cites work: Q3996704
cites work: On the expressive power of Kleene algebra with domain
cites work: Hoare Semigroups
cites work: Ordinary differential equations and dynamical systems
DOI: 10.1007/S10817-021-09607-X
description: scientific article; zbMATH DE number 7498609