On Hoare logic and Kleene algebra with tests
From MaRDI portal
Publication:5738898
DOI10.1145/343369.343378zbMath1365.68326OpenAlexW2010626618MaRDI QIDQ5738898
Publication date: 13 June 2017
Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/343369.343378
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)
Related Items (44)
Algebras of modal operators and partial correctness ⋮ The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion Schemes ⋮ Canonical finite models of Kleene algebra with tests ⋮ The Laws of Programming Unify Process Calculi ⋮ Deciding Regular Expressions (In-)Equivalence in Coq ⋮ Boolean-like algebras ⋮ Laws of Programming for References ⋮ A Program Construction and Verification Tool for Separation Logic ⋮ Deciding Synchronous Kleene Algebra with Derivatives ⋮ Differential Hoare Logics and Refinement Calculi for Hybrid Systems with Isabelle/HOL ⋮ Automatic Proof Generation in Kleene Algebra ⋮ Hopscotch -- reaching the target hop by hop ⋮ A relation-algebraic approach to the ``Hoare logic of functional dependencies ⋮ Axiomatizability of representable domain algebras ⋮ Embedding Kozen-Tiuryn logic into residuated one-sorted Kleene algebra with tests ⋮ Local completeness logic on Kleene algebra with tests ⋮ Unnamed Item ⋮ A fine-grained semantics for arrays and pointers under weak memory models ⋮ On the expressive power of Kleene algebra with domain ⋮ An algebraic glimpse at bunched implications and separation logic ⋮ On algebra of program correctness and incorrectness ⋮ On tools for completeness of Kleene algebra with hypotheses ⋮ Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism ⋮ Local variable scoping and Kleene algebra with tests ⋮ On the Coalgebraic Theory of Kleene Algebra with Tests ⋮ Completeness for Identity-free Kleene Lattices ⋮ Hoare Semigroups ⋮ On the expressiveness of single-pass instruction sequences ⋮ Monoids with tests and the algebra of possibly non-halting programs ⋮ Algebraic separation logic ⋮ Unnamed Item ⋮ Synchronous Kleene algebra ⋮ Algebras for iteration and infinite computations ⋮ Extended Static Checking by Calculation Using the Pointfree Transform ⋮ Fifty years of Hoare's logic ⋮ Building program construction and verification tools from algebraic principles ⋮ Partial Maps with Domain and Range: Extending Schein's Representation ⋮ KAT-ML: an interactive theorem prover for Kleene algebra with tests ⋮ MODAL RESTRICTION SEMIGROUPS: TOWARDS AN ALGEBRA OF FUNCTIONS ⋮ SEMIGROUPS WITH if–then–else AND HALTING PROGRAMS ⋮ Domain Axioms for a Family of Near-Semirings ⋮ A semantics and a logic for \textit{Fuzzy Arden Syntax} ⋮ Infinite executions of lazy and strict computations ⋮ Deciding Kleene algebra terms equivalence in Coq
This page was built for publication: On Hoare logic and Kleene algebra with tests
