Modular termination of C programs

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.

Data and Resources

Additional Info

Field Value
Source https://inria.hal.science/hal-00760917
Author Andrieu, Guillaume, Alias, Christophe, Gonnord, Laure
Maintainer CCSD
Last Updated May 30, 2026, 06:43 (UTC)
Created May 30, 2026, 06:43 (UTC)
Identifier Report N°: RR-8166
Language en
Rights https://about.hal.science/hal-authorisation-v1/
contributor Laboratoire d'Informatique Fondamentale de Lille (LIFL) ; Université de Lille, Sciences et Technologies-Institut National de Recherche en Informatique et en Automatique (Inria)-Université de Lille, Sciences Humaines et Sociales-Centre National de la Recherche Scientifique (CNRS)
creator Andrieu, Guillaume
date 2012-12-04T00:00:00
harvest_object_id 56819d56-2b96-4ef5-a106-3d545f9cd947
harvest_source_id 3374d638-d20b-4672-ba96-a23232d55657
harvest_source_title test moissonnage SELUNE
metadata_modified 2025-10-13T00:00:00
set_spec type:REPORT