Program analysis and verification based on Kleene algebra in Isabelle/HOL

DOI10.1007/978-3-642-39634-2_16MaRDI QIDQ5327345zbMATH OpenOpenAlexFDO

Authors Alasdair Armstrong, Georg Struth, Tjark Weber

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

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Algebraic theory of languages and automata (68Q70)

Recommendations

• Algebras for program correctness in Isabelle/HOL
• Building program construction and verification tools from algebraic principles
• Kleene algebra with tests and Coq tools for while programs
• On Hoare logic and Kleene algebra with tests
• Deciding KAT and Hoare logic with derivatives

Cited in

(13)

• Calculational verification of reactive programs with reactive relations and Kleene algebra
• Modal Kleene algebra applied to program correctness
• Solving quantifier-free first-order constraints over finite sets and binary relations
• A verified compiler from Isabelle/HOL to CakeML
• Unifying heterogeneous state-spaces with lenses
• Hoare semigroups
• Stone relation algebras
• Mathematics of Program Construction
• Algebras for program correctness in Isabelle/HOL
• An Axiomatization of Arrays for Kleene Algebra with Tests
• Logic for Programming, Artificial Intelligence, and Reasoning
• Building program construction and verification tools from algebraic principles
• Describing data flow analysis techniques with Kleene algebra

Describes a project that uses

Uses Software

• Isabelle/HOL
• Coq
• Ynot
• KAT-ML

This page was built for publication: Program analysis and verification based on Kleene algebra in Isabelle/HOL

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5327345)