Journal's Facebook pageUDC 004.421
KAT and PHL in Coq
- 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: 2406-1018 (Online)
Publisher: ComSIS Consortium
Full text
Available 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)
