Skip to Main content Skip to Navigation
New interface
Conference papers

Accelerated Invariant Generation for C Programs with Aspic and C2fsm

Paul Feautrier 1 Laure Gonnord 2, 3 
1 COMPSYS - Compilation and embedded computing systems
Inria Grenoble - Rhône-Alpes, LIP - Laboratoire de l'Informatique du Parallélisme
3 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 present Aspic, an automatic polyhedral invariant generation tool for flowcharts programs. Aspic implements an improved Linear Relation Analysis on numeric counter automata. The "accelerated" method improves precision by computing locally a precise overapproximation of a loop without using the widening operator. C2Fsm is a C preprocessor that generates automata in the format required by Aspic. The experimental results show the performance and precision of the tools.
Document type :
Conference papers
Complete list of metadata
Contributor : Laure Gonnord Connect in order to contact the contributor
Submitted on : Monday, October 4, 2010 - 5:52:08 PM
Last modification on : Tuesday, October 25, 2022 - 4:19:08 PM
Long-term archiving on: : Thursday, October 25, 2012 - 4:30:16 PM




Paul Feautrier, Laure Gonnord. Accelerated Invariant Generation for C Programs with Aspic and C2fsm. Tools for Automatic Program AnalysiS, Sep 2010, Perpignan, France. ⟨10.1016/j.entcs.2010.09.014⟩. ⟨inria-00523320⟩



Record views


Files downloads