Kleene algebra with tests and Coq tools for while programs

DOI10.1007/978-3-642-39634-2_15MaRDI QIDQ5327344zbMATH OpenOpenAlexFDO

Authors Damien Pous

Publication date 7 August 2013

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1302.1737

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)

Abstract: We present a Coq library about Kleene algebra with tests, including a proof of their completeness over the appropriate notion of languages, a decision procedure for their equational theory, and tools for exploiting hypotheses of a particular shape in such a theory. Kleene algebra with tests make it possible to represent if-then-else statements and while loops in most imperative programming languages. They were actually introduced by Kozen as an alternative to propositional Hoare logic. We show how to exploit the corresponding Coq tools in the context of program verification by proving equivalences of while programs, correctness of some standard compiler optimisations, Hoare rules for partial correctness, and a particularly challenging equivalence of flowchart schemes.

Recommendations

• Deciding Kleene algebras in \texttt{Coq}
• An efficient Coq tactic for deciding Kleene algebras
• On Hoare logic and Kleene algebra with tests
• Algebras for program correctness in Isabelle/HOL
• Building program construction and verification tools from algebraic principles

Cited in

(30)

• Regular language representations in the constructive type theory of Coq
• Using relation-algebraic means and tool support for investigating and computing bipartitions
• On tools for completeness of Kleene algebra with hypotheses
• scientific article; zbMATH DE number 1696821 (Why is no real title available?)
• Cardinalities of Finite Relations in Coq
• A coalgebraic approach to Kleene algebra with tests
• Deciding Kleene algebras in \texttt{Coq}
• Algorithms for Kleene algebra with converse
• KAT-ML: an interactive theorem prover for Kleene algebra with tests
• Hoare semigroups
• Completeness for identity-free Kleene lattices
• Non-wellfounded proof theory for (Kleene+action)(algebras+lattices)
• Reasoning about cardinalities of relations with applications supported by proof assistants
• Program analysis and verification based on Kleene algebra in Isabelle/HOL
• Verification of the correctness of compiler optimization using co-induction
• An efficient Coq tactic for deciding Kleene algebras
• Coinduction: automata, formal proof, companions (invited paper)
• Embedding Kozen-Tiuryn logic into residuated one-sorted Kleene algebra with tests
• A Coq implementation of the program algebra in Jifeng He's new roadmap for linking theories of programming
• On tools for completeness of Kleene algebra with hypotheses
• Completeness theorems for Kleene algebra with tests and top
• BiGKAT: an algebraic framework for relational verification of probabilistic programs
• Diagrammatic algebra of first order logic
• A coalgebraic approach to Kleene algebra with tests
• When Lawvere meets Peirce: an equational presentation of Boolean hyperdoctrines
• A Kleene algebra with tests for union bound reasoning about probabilistic programs
• The calculus of neo-Peircean relations
• Building program construction and verification tools from algebraic principles
• Cardinality of relations with applications
• Local variable scoping and Kleene algebra with tests

Describes a project that uses

Uses Software

• Coq

This page was built for publication: Kleene algebra with tests and Coq tools for while programs

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