Algebras for iteration and infinite computations

DOI10.1007/s00236-012-0162-2zbMath1279.68078OpenAlexW2149537518MaRDI QIDQ715050

Walter Guttmann

Publication date: 15 October 2012

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00236-012-0162-2

zbMATH Keywords

iterationprogram transformationrefinementseparationIsabellerelational models of computations

Mathematics Subject Classification ID

Related Items (8)

Stone Relation Algebras ⋮ An algebraic approach to computations with progress ⋮ Unifying Lazy and Strict Computations ⋮ A Hierarchy of Algebras for Boolean Subsets ⋮ Multirelations with infinite computations ⋮ Kleene star, subexponentials without contraction, and infinite computations ⋮ Verifying minimum spanning tree algorithms with Stone relation algebras ⋮ Infinite executions of lazy and strict computations

Uses Software

• Nitpick
• Mace4
• Sledgehammer

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Fixpoints for general correctness
• Internal axioms for domain semirings
• Fixed-point calculus
• Kleene under a modal demonic star
• Algebras of modal operators and partial correctness
• Verification of sequential and concurrent programs
• Normal design algebra
• Kleene getting lazy
• Relational algebraic semantics of deterministic and nondeterministic programs
• Reasoning algebraically about loops
• A completeness theorem for Kleene algebras and the algebra of regular events
• Towards a refinement algebra
• General correctness: A unification of partial and total correctness
• Unifying Correctness Statements
• Unifying Lazy and Strict Computations
• Algebraic Notions of Termination
• Unifying Recursion in Partial, Total and General Correctness
• Partial, Total and General Correctness
• Unifying Theories of Programming That Distinguish Nontermination and Abort
• The Linear Algebra of UTP
• General Correctness Algebra
• A generalized control structure and its formal definition
• Extending Sledgehammer with SMT Solvers
• Modal Design Algebra
• Demonic Algebra with Domain
• Omega Algebra, Demonic Refinement Algebra and Commands
• On Hoare logic and Kleene algebra with tests
• Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder

This page was built for publication: Algebras for iteration and infinite computations