UDC 004.421

KAT and PHL in Coq

David Pereira1 and Nelma Moreira1

  1. DCC-FC & LIACC - University of Porto
    Rua do Campo Alegre 1021, 4169-007
    {dpereira,nam}@ncc.up.pt

Abstract

In this article we describe an implementation of Kleene algebra with tests (KAT) in the Coq theorem prover. KAT is an equational system that has been successfully applied in program verification and, in particular, it subsumes the propositional Hoare logic (PHL). We also present an PHL encoding in KAT, by deriving its deduction rules as theorems of KAT. Some examples of simple program’s formal correctness are given. This work is part of a study of the feasibility of using KAT in the automatic production of certificates in the context of (source-level) Proof-Carrying-Code (PCC).

Key words

Kleene algebra with tests, Hoare logics, interactive theorem proving, and formal verification of software

Publication information

Volume 5, Issue 2 (December 2008)
Compilers, Related Technologies and Applications
Year of Publication: 2008
ISSN: 1820-0214 (Print) 2406-1018 (Online)
Publisher: ComSIS Consortium

Full text

DownloadAvailable in PDF
Portable Document Format

How to cite

Pereira, D., Moreira, N.: KAT and PHL in Coq. Computer Science and Information Systems, Vol. 5, No. 2, 137-160. (2008)