Modular termination of C programs

Andrieu Guillaume 1 Christophe Alias 2 Laure Gonnord 1, 3
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
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
Complete list of metadatas

https://hal.inria.fr/hal-00760917
Contributor : Laure Gonnord <>
Submitted on : Tuesday, December 4, 2012 - 3:30:04 PM
Last modification on : Sunday, March 17, 2019 - 8:58:02 AM
Long-term archiving on : Tuesday, March 5, 2013 - 3:52:55 AM

File

RR-8166.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00760917, version 1

Collections

Citation

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

Share

Metrics

Record views

31

Files downloads

13