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.
Type de document :
Communication dans un congrès
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
Contributeur : Laure Gonnord <>
Soumis le : lundi 4 octobre 2010 - 17:52:08
Dernière modification le : jeudi 22 novembre 2018 - 12:50:03
Document(s) archivé(s) le : jeudi 25 octobre 2012 - 16:30:16

Identifiants

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〉

Partager

Métriques

Consultations de la notice

436

Téléchargements de fichiers

572