Accelerated Invariant Generation for C Programs with Aspic and C2fsm
Résumé
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.
Domaines
Calcul formel [cs.SC]
Fichier principal
tapas10_FeautrierGonnord.authorversion.pdf (248.94 Ko)
Télécharger le fichier
tapas2010_aspic.pdf (323.48 Ko)
Télécharger le fichier
Origine : Fichiers produits par l'(les) auteur(s)
Format : Autre