Accelerated Invariant Generation for C Programs with Aspic and C2fsm
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.
Domains
Symbolic Computation [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
Origin : Files produced by the author(s)
Format : Other