Skip to Main content Skip to Navigation
New interface
Reports (Research report)

Modular termination of C programs

Guillaume Andrieu 1 Christophe Alias 2 Laure Gonnord 1, 3, 4 
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 paper we describe 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 [compsys-termination-sas10] and preliminary results shows the feasibility of the method.
Document type :
Reports (Research report)
Complete list of metadata

Cited literature [12 references]  Display  Hide  Download
Contributor : Laure Gonnord Connect in order to contact the contributor
Submitted on : Wednesday, December 19, 2012 - 11:47:07 AM
Last modification on : Wednesday, October 26, 2022 - 8:16:24 AM
Long-term archiving on: : Wednesday, March 20, 2013 - 11:34:06 AM


Files produced by the author(s)


  • HAL Id : hal-00760917, version 2


Guillaume Andrieu, Christophe Alias, Laure Gonnord. Modular termination of C programs. [Research Report] RR-8166, INRIA. 2012. ⟨hal-00760917v2⟩



Record views


Files downloads