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.