Certification of program termination
4 pages
English

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Certification of program termination

-

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus
4 pages
English
Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

Description

Niveau: Supérieur, Doctorat, Bac+8
Internship proposals Certification of program termination Frederic Blanqui (INRIA) Place: The internship will take place at Tsinghua University1 (Beijing, China) within the INRIA2 project-team FORMES3 which is part of the LIAMA4 Con- sortium, the Sino-French Laboratory for Computer Science, Automation and Applied Mathematics. The members of the FORMES project-team also in- clude Pr Ming Gu, Dr Fei He, Dr Claude Helmstetter, Pr Vania Joloboff, Pr Jean-Pierre Jouannaud, Pr Jean-Franc¸ois Monin, Dr Pierre-Yves Strub and Dr Bow-Yaw Wang. Introduction: Termination is an important property of programs. For a given program, it may even be necessary to establish its termination in order to prove its correct- ness. For this undecidable problem, many criteria and tools have been developed over the last years. But these become more and more complex and difficult to verify. To recover the confidence one can expect from such tools, it is nec- essary to certify their results. For stimulating the research in this area, the steering committee of the international competition on termination5 organizes a competition for certified termination provers since 2007. The CoLoR project6 aims at providing tools for certifying the results of automated provers. The tools developed in this project, CoLoR and Rainbow, are currently used by four different termination provers: AProVE (best 2007 termination tool for TRSs), Matchbox (best 2007 termination tool for SRSs), TPA and TTT2.

  • automated termination analysis

  • termination certificate

  • computational logic

  • programs based

  • can expect

  • them can

  • program termination

  • rewriting

  • common programming


Sujets

Informations

Publié par
Nombre de lectures 22
Langue English

Extrait

Internship proposals
Certicationofprogramtermination
Frédéric Blanqui (INRIA)
http://wwwrocq.inria.fr/ blanqui ~
Place: 1 The internship will take place at Tsinghua University (Beijing, China) 2 3 4 within the INRIA projectteam FORMES which is part of the LIAMA Con sortium, the SinoFrench Laboratory for Computer Science, Automation and Applied Mathematics. The members of the FORMES projectteam also in clude Pr Ming Gu, Dr Fei He, Dr Claude Helmstetter, Pr Vania Joloboff, Pr JeanPierreJouannaud,PrJeanFranc¸oisMonin,DrPierreYvesStrubandDr BowYaw Wang.
Introduction: Termination is an important property of programs. For a given program, it may even be necessary to establish its termination in order to prove its correct ness. For this undecidable problem, many criteria and tools have been developed over the last years. But these become more and more complex and difficult to verify. To recover the confidence one can expect from such tools, it is nec essary to certify their results. For stimulating the research in this area, the 5 steering committee of the international competition on termination organizes a competition for certified termination provers since 2007. 6 The CoLoR project aims at providing tools for certifying the results of automated provers. The tools developed in this project, CoLoR and Rainbow, are currently used by four different termination provers: AProVE (best 2007 termination tool for TRSs), Matchbox (best 2007 termination tool for SRSs), TPA and TTT2. And CoLoR+Rainbow was the best certification backend for 7 the last two years in the international competition on termination . The approach taken in CoLoR is as follows. It is based on two impor tant elements. First, a grammar for termination certificates (TCG) (currently implemented as an XML Schema). Second, a Coq library of the termination 8 techniques used in the grammar. Coq is a highly secure proof checker and proof development tool which allows one to reach the highest security standards
1 http://www.thss.tsinghua.edu.cn/index_en.asp 2 http://www.inria.fr 3 http://formes.asia 4 http://liama.ia.ac.cn 5 http://terminationportal.org 6 http://color.inria.fr 7 http://terminationportal.org/wiki/Termination_Competition 8 http://coq.inria.fr
1
  • Univers Univers
  • Ebooks Ebooks
  • Livres audio Livres audio
  • Presse Presse
  • Podcasts Podcasts
  • BD BD
  • Documents Documents