SToP : Scalable Termination analysis of (C) Programs (tool presentation)

Guillaume Andrieu 1 Christophe Alias 2, * Laure Gonnord 1, 3, 4
* Auteur correspondant
2 COMPSYS - Compilation and embedded computing systems
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
3 LIFL - DART/Émeraude
LIFL - Laboratoire d'Informatique Fondamentale de Lille
4 DART - Contributions of the Data parallelism to real time
LIFL - Laboratoire d'Informatique Fondamentale de Lille, Inria Lille - Nord Europe
Abstract : In this talk, we present Stop, which implements a general method to prove termination of C programs in a scalable and modular way. The program to analyse is reduced to the smallest relevant subset through a termination-specific slicing technique. Then, the program is divided into pieces of code that are analysed separately, thanks to an external engine for termination. The result is implemented in the prototype \stoptool over our previous toolsuite WTC (\cite{compsys-termination-sas10}) and preliminary results shows the feasibility of the method.
Type de document :
Communication dans un congrès
Tapas 2012, Sep 2012, Deauville, France. 2012
Liste complète des métadonnées

https://hal.inria.fr/hal-00760926
Contributeur : Laure Gonnord <>
Soumis le : mardi 4 décembre 2012 - 15:38:53
Dernière modification le : jeudi 8 février 2018 - 11:08:20

Identifiants

  • HAL Id : hal-00760926, version 1

Collections

Citation

Guillaume Andrieu, Christophe Alias, Laure Gonnord. SToP : Scalable Termination analysis of (C) Programs (tool presentation). Tapas 2012, Sep 2012, Deauville, France. 2012. 〈hal-00760926〉

Partager

Métriques

Consultations de la notice

310