Algebras of modal operators and partial correctness

DOI10.1016/j.tcs.2005.09.069zbMath1086.68082OpenAlexW2016732604MaRDI QIDQ820135

Georg Struth, Bernhard Möller

Publication date: 6 April 2006

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://opus.bibliothek.uni-augsburg.de/opus4/frontdoor/index/index/docId/39151

zbMATH Keywords

semiringsHoare logicpartial correctnessKleene algebramodal operators

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items

D-semigroups and constellations ⋮ Domain and Range Operations in Semigroups and Rings ⋮ Unifying Operational Weak Memory Verification: An Axiomatic Approach ⋮ Algebraic notions of nontermination: Omega and divergence in idempotent semirings ⋮ A Program Construction and Verification Tool for Separation Logic ⋮ A Hierarchy of Algebras for Boolean Subsets ⋮ Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL ⋮ Non-termination in Idempotent Semirings ⋮ The Structure of the One-Generated Free Domain Semiring ⋮ Knowledge and Games in Modal Semirings ⋮ Exploring modal worlds ⋮ Axiomatizability of representable domain algebras ⋮ Semigroup actions on posets and preimage quasi-orders ⋮ Internal axioms for domain semirings ⋮ Local completeness logic on Kleene algebra with tests ⋮ On the complexity of Kleene algebra with domain ⋮ On the expressive power of Kleene algebra with domain ⋮ On algebra of program correctness and incorrectness ⋮ Modal Semirings Revisited ⋮ How to generalise demonic composition ⋮ Domain and range for angelic and demonic compositions ⋮ Undecidability of representability as binary relations ⋮ Monoids with tests and the algebra of possibly non-halting programs ⋮ Algebraic separation logic ⋮ Algebras for iteration and infinite computations ⋮ Building program construction and verification tools from algebraic principles ⋮ MODAL RESTRICTION SEMIGROUPS: TOWARDS AN ALGEBRA OF FUNCTIONS ⋮ SEMIGROUPS WITH if–then–else AND HALTING PROGRAMS ⋮ Modal algebra and Petri nets ⋮ Infinite executions of lazy and strict computations

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• ``A la Burstall intermittent assertions induction principles for proving inevitability properties of programs
• Dynamic algebras: Examples, constructions, applications
• A completeness theorem for Kleene algebras and the algebra of regular events
• Characterizing determinacy in Kleene algebras
• Some results in dynamic model theory
• Relational and Kleene-algebraic methods in computer science. 7th international seminar on relational methods in computer science (RelMiCS 7) and 2nd international workshop on applications of Kleene algebra, Bad Malente, Germany, May 12-17, 2003. Revised selected papers
• Temporal algebra
• Demonic operators and monotype factors
• Kleene algebra with domain
• Algebraic Methodology and Software Technology
• Mathematics of Program Construction
• On Hoare logic and Kleene algebra with tests
• Boolean Algebras with Operators. Part I

This page was built for publication: Algebras of modal operators and partial correctness