Towards a refinement algebra
From MaRDI portal
Publication:1881265
DOI10.1016/j.scico.2003.09.002zbMath1091.68030OpenAlexW4212873283WikidataQ114850304 ScholiaQ114850304MaRDI QIDQ1881265
Publication date: 4 October 2004
Published in: Science of Computer Programming (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.scico.2003.09.002
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items
Finite representability of semigroups with demonic refinement ⋮ An algebraic approach to computations with progress ⋮ Normal design algebra ⋮ Unifying Lazy and Strict Computations ⋮ On Completeness of Omega-Regular Algebras ⋮ Generalised rely-guarantee concurrency: an algebraic foundation ⋮ Abstract representation theorems for demonic refinement algebras ⋮ Algebraic notions of nontermination: Omega and divergence in idempotent semirings ⋮ A synchronous program algebra: a basis for reasoning about shared-memory and event-based concurrency ⋮ Designing a semantic model for a wide-spectrum language with concurrency ⋮ Latest News about Demonic Algebra with Domain ⋮ On the Structure of Demonic Refinement Algebras with Enabledness and Termination ⋮ Non-termination in Idempotent Semirings ⋮ Reactive Probabilistic Programs and Refinement Algebra ⋮ Balancing expressiveness in formal approaches to concurrency ⋮ Hopscotch -- reaching the target hop by hop ⋮ Internal axioms for domain semirings ⋮ Probabilistic Choice in Refinement Algebra ⋮ Modal Semirings Revisited ⋮ Relational characterisations of paths ⋮ Enabledness and termination in refinement algebra ⋮ Algebraic reasoning for probabilistic action systems and while-loops ⋮ Modelling higher-order dual nondeterminacy ⋮ Hoare Semigroups ⋮ Modal Tools for Separation and Refinement ⋮ An algebraic approach to multirelations and their properties ⋮ A sketch of a dynamic epistemic semiring ⋮ Dual choice and iteration in an abstract algebra of action ⋮ Monoids with tests and the algebra of possibly non-halting programs ⋮ Normal forms in total correctness for while programs and action systems ⋮ Refinement algebra for probabilistic programs ⋮ Algebras for iteration and infinite computations ⋮ Algebra of Monotonic Boolean Transformers ⋮ Automated verification of refinement laws ⋮ Domain Axioms for a Family of Near-Semirings ⋮ Infinite executions of lazy and strict computations ⋮ Completeness results for omega-regular algebras