Automated verification of termination certificates

Frédéric Blanqui; Kim Quyen Ly

hal-00763495, version 1

Automated verification of termination certificates

Frédéric Blanqui ( Auteur à contacter de préférence , )^a^, 1, 2, Kim Quyen Ly (, )^a^, 1, 2

15th National Symposium of Selected ICT Problems (2012)

Résumé : In order to increase user confidence, many automated theorem provers provide certificates that can be independently verified. In this paper, we report on our progress in developing a standalone tool for checking the correctness of certificates for the termination of term rewrite systems, and formally proving its correctness in the proof assistant Coq. To this end, we use the extraction mechanism of Coq and the library on rewriting theory and termination called CoLoR.

a – INRIA
1 : FORMES (LIAMA)
INRIA – Tsinghua University / Beijing – LIAMA
2 : ISCAS - State Key Laboratory of Computer Science (LCS)
Institute of Software of the Chinese Academy of Sciences

hal-00763495, version 1
http://hal.inria.fr/hal-00763495
oai:hal.inria.fr:hal-00763495
Contributeur : Frédéric Blanqui <>
Soumis le : Mardi 11 Décembre 2012, 04:39:30
Dernière modification le : Mardi 11 Décembre 2012, 10:24:50

Voir la fiche détaillée

Documents associés

PDF :

PS :

arXiv : 1212.2350

Voir aussi

Exporter

Bibtex EndNote TEI RefWorks

<?xml version="1.0" encoding="UTF-8"?>
<listBibl xmlns="http://www.tei-c.org/ns/1.0" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:mml="http://www.w3.org/1998/Math/MathML">
<listBibl type="article"><head>Communications sans actes</head>
<biblStruct type="article" xml:id="hal-00763495"><analytic>
<author><persName><forename>Frédéric</forename><surname>Blanqui</surname></persName>
<affiliation>
<orgName type="laboratory">LIAMA</orgName>
<orgName type="team">FORMES</orgName>
<country>CN</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Tsinghua University / Beijing</orgName>
<orgName type="institution">LIAMA</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">LCS</orgName>
<orgName type="team">ISCAS - State Key Laboratory of Computer Science</orgName>
<country>CN</country>
<orgName type="institution">Institute of Software of the Chinese Academy of Sciences</orgName>
</affiliation>
</author>
<author><persName><forename>Kim Quyen</forename><surname>Ly</surname></persName>
<affiliation>
<orgName type="laboratory">LIAMA</orgName>
<orgName type="team">FORMES</orgName>
<country>CN</country>
<orgName type="institution">INRIA</orgName>
<orgName type="institution">Tsinghua University / Beijing</orgName>
<orgName type="institution">LIAMA</orgName>
</affiliation>
<affiliation>
<orgName type="laboratory">LCS</orgName>
<orgName type="team">ISCAS - State Key Laboratory of Computer Science</orgName>
<country>CN</country>
<orgName type="institution">Institute of Software of the Chinese Academy of Sciences</orgName>
</affiliation>
</author>
<title type="main" level="a">Automated verification of termination certificates</title></analytic><monogr><meeting>15th National Symposium of Selected ICT Problems</meeting><imprint><pubPlace><settlement>Hanoi</settlement><country>Viet Nam</country></pubPlace><biblScope type="publicationDate">2012-11-17</biblScope></imprint></monogr><idno type="HALid">http://hal.inria.fr/hal-00763495</idno><idno type="HALFile">http://hal.inria.fr/hal-00763495/PDF/main.pdf</idno></biblStruct>
</listBibl>
</listBibl>