Certification of automated termination proofs Export

@inproceedings{citeulike:6067070, abstract = {2 C\'{E}DRIC – Conservatoire national des arts et m\'{e}tiers Abstract. Nowadays, formal methods rely on tools of different kinds: proof assistants with which the user interacts to discover a proof step by step; and fully automated tools which make use of (intricate) decision procedures. But while some proof assistants can check the soundness of a proof, they lack automation. Regarding automated tools, one still has to be satisfied with their answers Yes/No/Donotknow, the validity of which can be subject to question, in particular because of the increasing size and complexity of these tools. In the context of rewriting techniques, we aim at bridging the gap between proof assistants that yield formal guarantees of reliability and highly automated tools one has to trust. We present an approach making use of both shallow and deep embeddings. We illustrate this approach with a prototype based on the CiME rewriting toolbox, which can discover involved termination proofs that can be certified by the COQ proof assistant, using the COCCINELLE library for rewriting. 1}, author = {Contejean, Evelyne and Courtieu, Pierre and Forest, Julien and Pons, Olivier and Urbain, Xavier}, booktitle = {In Proc. 6th FroCoS}, citeulike-article-id = {6067070}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.81.5500}, keywords = {cime, coccinelle, coq, rewriting}, pages = {148--162}, posted-at = {2009-11-04 09:13:57}, priority = {2}, title = {Certification of automated termination proofs}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.81.5500}, year = {2007} }

TY - CONF ID - citeulike:6067070 L3 - citeulike-article-id:6067070 N2 - 2 CÉDRIC – Conservatoire national des arts et métiers Abstract. Nowadays, formal methods rely on tools of different kinds: proof assistants with which the user interacts to discover a proof step by step; and fully automated tools which make use of (intricate) decision procedures. But while some proof assistants can check the soundness of a proof, they lack automation. Regarding automated tools, one still has to be satisfied with their answers Yes/No/Donotknow, the validity of which can be subject to question, in particular because of the increasing size and complexity of these tools. In the context of rewriting techniques, we aim at bridging the gap between proof assistants that yield formal guarantees of reliability and highly automated tools one has to trust. We present an approach making use of both shallow and deep embeddings. We illustrate this approach with a prototype based on the CiME rewriting toolbox, which can discover involved termination proofs that can be certified by the COQ proof assistant, using the COCCINELLE library for rewriting. 1 EP - 162 TI - Certification of automated termination proofs T2 - In Proc. 6th FroCoS SP - 148 KW - cime KW - coccinelle KW - coq KW - rewriting AU - Contejean, Evelyne AU - Courtieu, Pierre AU - Forest, Julien AU - Pons, Olivier AU - Urbain, Xavier PY - 2007/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.81.5500 ER -