On Hoare logic and Kleene algebra with tests
From MaRDI portal
Publication:5738898
DOI10.1145/343369.343378zbMath1365.68326MaRDI 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
03B70: Logic in computer science
68Q60: Specification and verification (program logics, model checking, etc.)
68Q17: Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
Related Items
Hoare Semigroups, Unnamed Item, Extended Static Checking by Calculation Using the Pointfree Transform, The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion Schemes, Domain Axioms for a Family of Near-Semirings, SEMIGROUPS WITH if–then–else AND HALTING PROGRAMS, Canonical finite models of Kleene algebra with tests, Boolean-like algebras, Hopscotch -- reaching the target hop by hop, A relation-algebraic approach to the ``Hoare logic of functional dependencies, Algebraic separation logic, Axiomatizability of representable domain algebras, On the expressiveness of single-pass instruction sequences, Synchronous Kleene algebra, Algebras for iteration and infinite computations, Building program construction and verification tools from algebraic principles, Algebras of modal operators and partial correctness, On the expressive power of Kleene algebra with domain, Local variable scoping and Kleene algebra with tests, Monoids with tests and the algebra of possibly non-halting programs, Fifty years of Hoare's logic, Infinite executions of lazy and strict computations, Deciding Kleene algebra terms equivalence in Coq, The Laws of Programming Unify Process Calculi, Deciding Regular Expressions (In-)Equivalence in Coq, Laws of Programming for References, A Program Construction and Verification Tool for Separation Logic, Deciding Synchronous Kleene Algebra with Derivatives, Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism, MODAL RESTRICTION SEMIGROUPS: TOWARDS AN ALGEBRA OF FUNCTIONS, On the Coalgebraic Theory of Kleene Algebra with Tests, Partial Maps with Domain and Range: Extending Schein's Representation, Automatic Proof Generation in Kleene Algebra, KAT-ML: an interactive theorem prover for Kleene algebra with tests
