Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL
From MaRDI portal
Publication:5327345
DOI10.1007/978-3-642-39634-2_16zbMath1317.68201OpenAlexW1797941296MaRDI QIDQ5327345
Tjark Weber, Alasdair Armstrong, Georg Struth
Publication date: 7 August 2013
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-207378
Logic in computer science (03B70) Algebraic theory of languages and automata (68Q70) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (5)
Stone Relation Algebras ⋮ Unifying Heterogeneous State-Spaces with Lenses ⋮ Hoare Semigroups ⋮ Building program construction and verification tools from algebraic principles ⋮ Solving quantifier-free first-order constraints over finite sets and binary relations
Uses Software
This page was built for publication: Program Analysis and Verification Based on Kleene Algebra in Isabelle/HOL
