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
Tools for Automatic Program AnalysiS, Sep 2010, Perpignan, France. 2010, <10.1016/j.entcs.2010.09.014>
Liste complète des métadonnées

https://hal.inria.fr/inria-00523320
Contributor : Laure Gonnord <>
Submitted on : Monday, October 4, 2010 - 5:52:08 PM
Last modification on : Wednesday, October 7, 2015 - 1:14:00 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. 2010, <10.1016/j.entcs.2010.09.014>. <inria-00523320>

Share

Metrics

Record views

350

Document downloads

482