Skip to Main content Skip to Navigation
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
LIP - Laboratoire de l'Informatique du Parallélisme, Inria Grenoble - Rhône-Alpes
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 metadatas

https://hal.inria.fr/inria-00523320
Contributor : Laure Gonnord <>
Submitted on : Monday, October 4, 2010 - 5:52:08 PM
Last modification on : Tuesday, December 24, 2019 - 9:16:07 AM
Document(s) archivé(s) le : Thursday, October 25, 2012 - 4:30:16 PM

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

548

Files downloads

794