KAT and PHL in Coq

• Tipo: Artigo em Revista Científica Internacional
• Data: 2008

Autores

David Pereira (Autor) Outra; Nelma Moreira (Autor) FCUP

Revista

Título: Computer Science and Information Systems

Vol. 5

Páginas: 137-160

ISSN: 1820-0214

Editora: ComSIS Consortium

Indexação

ISI Web of Knowledge - 2 Citações

Scopus - 5 Citações

Classificação Científica

FOS: Ciências exactas e naturais > Ciências da computação e da informação

Outras Informações

ID Authenticus: P-003-TD0

DOI: 10.2298/csis0802137p

Abstract (EN): 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).

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Nº de páginas: 24