Hoare semigroups

DOI10.1017/S096012951700007XMaRDI QIDQ4640310zbMATH OpenOpenAlexFDO

Authors Georg Struth

Publication date 17 May 2018

Published in Mathematical Structures in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1017/s096012951700007x

Mathematics Subject Classification ID

Logic in computer science (03B70) General structure theory for semigroups (20M10) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• Towards reasoning about Hoare relations
• Hoare Logic in the Abstract
• scientific article; zbMATH DE number 2110621
• scientific article; zbMATH DE number 3986619
• On Hoare logic and Kleene algebra with tests

Cites work

• Building program construction and verification tools from algebraic principles
• Concurrent dynamic algebra
• Concurrent dynamic logic
• scientific article; zbMATH DE number 605806 (Why is no real title available?)
• Internal axioms for domain semirings
• Isabelle/HOL. A proof assistant for higher-order logic
• Kleene algebra with tests and Coq tools for while programs
• On Hoare logic and Kleene algebra with tests
• Program analysis and verification based on Kleene algebra in Isabelle/HOL
• Reasoning about imperative quantum programs
• Towards a refinement algebra
• VERIFYING PROBABILISTIC PROGRAMS USING A HOARE LIKE LOGIC

Cited in

(5)

• Takahasi semigroups
• scientific article; zbMATH DE number 1405499 (Why is no real title available?)
• Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL
• Modal algebra of multirelations
• Predicate transformer semantics for hybrid systems. Verification components for Isabelle/HOL

Describes a project that uses

Uses Software

• Coq
• Archive Formal Proofs
• Isabelle/HOL
• Kleene Algebra

This page was built for publication: Hoare semigroups

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