Aspic tool implementation

Aspic is implemented over a fixpoint generic analyzer called Analyseur ([ANA]), developped by B. Jeannet at Inria. This tool performs a fixpoint analysis, provided an encoding of the control flow graph and an implementation of the abstract lattice of properties. We chose the polyhedral library NewPolka ([New]).

Aspic takes as input the textual automata input format of the tool Fast ([BFLP03]). A Fast file is composed of two parts : A “model”, which contains a textual description of a unique counter automaton: numerical vars, control points and transition functions consisting of a source, a destination, a numerical guard (possibly non convex) and an affine action over the numerical variables.

A “strategy”, which defines “regions”, and computation objectives. In contrast with the tool Fast itself, our tool only needs an initial region; an “error region” is only optionnal, and no additional information is required.

The Aspic tool makes a forward accessibility analysis, which aims at discovering some polyhedral invariants at each program control point. If an error region is defined (a formula over numerical variables and control points), the goal is transformed into a non accessibility problem by creating new bad states and new transitions; if, after convergence, all the bad states are associated an empty polyhedron, the goal is proved, otherwise the result is unconclusive.

The method used in aspic, called “Accelerated Linear Relation Analysis” is described in [Gon07] and [GH06].


The simplest way to use Aspic on the input.fst file is to use the command line :

./aspic input.fst [options]


Toy examples

For the toy examples, we compared our method (comumn “Aspic”) with the following ones :

Classic Linear Relation Analysis, without widening upto, without the new path algorithm, with two widenings : the standard one ([Hal79]) and the one proposed in  [BHRZ03]. The first analysis is implemented in Aspic and the StInG tool ([StI]) can deal with both two. The results can be found in column Hal79/BHRZ03. On the toy examples, the invariants are indeed the same.

The algorithm [SSM04], which is implemented in StInG (column named “STING”). Aspic provides a translator from Fast language to the input grammar of StInG.

The classical LRA with or without widening upto, with the new path algorithm. It has been done with the Aspic tool (column Ch79-v2)

The LRA with “lookahead widening” ([GR06]) that we also implemented in Aspic. The results can be found in column called “lookahead”.

The Fast tool([FAS]), that implement the acceleration techniques we described in [Ler03]. The used Fast version does not give the fixpoint, it gives only some informaton on the accerated loops. The benchmarks give only an estimation of the computing time.

The description of the automata can be found in Aspic homepage. We present only the results obtained by the different methods on a relevant control point in Fig 1 and 2. No computation time is given because all these analysis are instantaneous, at the exception of the gas burner and the car analysis with the Fast tool (we stopped these two analysis after 15 min because the Presburger automata were too big at this time (more than 8000 states in each case).

Name/MethodCh79/BHRZ03STINGCH79 v2

0≤ j
2j≤ i

idem BHRZ03

0≤ j
2ji≤ 104

Hal79b{0≤ y≤ x}idem BHRZ03{0≤ y ≤ x≤ 102} 
SP {x2+x3+x4+x7=p2,x1+x2+x4+x5+x6=p1, …}
GB{0≤ x≤ ℓ≤ t}idem ch79idem Aspic 

20≤ b
b≤ s+20


11≤ b
1≤ bs≤ 20

idem BHRZ03 

0≤ s ≤ d
0≤ t

idem BHRZ03idem Aspic 

0≤ s ≤ d
0≤ t

idem BHRZ03idem Aspic 
Apache1idem Aspic idem Aspicidem Aspic 
Goubault1bidem Aspic idem Aspicidem Aspic
Goubault2b{ji<=25,j≤ 175}{… i>150}idem Aspic 

j≥ k ,k≤ 10 
2k≤ a,0≤ a≤ 2k+5

BJRZ03 + 

j≥ 10

 idem BHRZ03 
wcet2idem Aspicidem Aspicidem Aspic 
dummy1{0≤ t0≤ t}idem CH79idem CH79 
dummy4{3t=3t0+zz≥ 0}idem Aspicidem Aspic
dummy6{t+2a≥ 4}

a≤ 6
0≤ t+a−2


0≤ t 
4≤ t+2a


t0=j, 1≤ t0, 1 ≤ i 
n−1 <t0  
n−1 <i 

idem BHRZ03idem BHRZ03 

t0=j,1≤ t0 1 ≤ i

idem BHRZ03idem BHRZ03
Figure 1: The toy examples with different methods (1)

Hal79aidem AspicOK

i+2j≤ 204
i≤ 104,0≤ j
2j≤ i

Hal79bidem AspicOK

0≤ y ≤ x≤ 102

SP {x2+x3+x4+x7=p2,x1+x2+x4+x5+x6=p1, …}
GB{0≤ x≤ ℓ≤ t}>15min

6ℓ ≤ t+5x
0≤ x≤ 10
x≤ ℓ
0≤ ℓ

Train1idem BHRZ03OKidem BHRZ03

0≤ s≤ d
s≤ 4
0≤ t

> 15min

0≤ s≤ 4
s≤ d
d≤ 4t+s


0≤ s≤ d
s≤ 2
0≤ t


0≤ s≤ 2
s≤ d
d≤ 2t+s
t≤ 3

Apache1idem AspicOK

c<tk_sz,0≤ c

Goubault1bidem AspicOK

j≤ 8,6≤ j

Goubault2bidem CH79V2OK (4s)

j≤ 175,i<177,98≤ j

wcet1idem CH79V2OK (4s)

0 ≤ 2k ≤ a≤ 2k+5 
3k<10i+10,k≤ 5i


20 ≤ 3k1


2k1≤  a 
0 ≤ k
a≤ 2k1+5

dummy1idem AspicOK

0≤ t0≤ t≤ t0+10

dummy4idem AspicOK

0≤ z≤ 56

dummy6idem CH79V2OK

4≤ t+2a≤ 16
−2≤ ta≤ 1

ax0idem CH79V2>3min

t0=j,1≤ t0≤ i 
n−1 <t0

t4x0idem CH79V2>3min

t0=j,1≤ i
i<=n+1,1≤ t0

Figure 2: The toy examples with different methods (2)

On these examples, we can remark that Aspic manages to infer more complex invariants than the other tools. When the classic LRA (column CH79-v2) gives the same result, it needs the new path heuristic and the widening upto, and converge in more steps, as can be shown in Figure 3. In this last table, we used proof goals and compare the behaviour of classical LRA, Lookahead widening and LRA with acceleration. We indicate the minimum of delay used for prooving the goal, and the number of global iterations. This table shows the effectivity of aspic in terms of iteration number.

ExampleProof GoalCH79_v2LookaheadAspic 
swapda≤ db+1delay = 4/6 itdelay = 4/7itdelay = 1/1 it
subwayb≤ s ⇒ sb ≤ 29delay = 1/ 5itdelay = 20/23 itdelay =1 / 4it 
GB6ℓ≤ t+50delay = 63/65 itdelay = 63/66 itdelay = 1/5 it 
wcet13k ≤ 10i+10delay=11/12 itdelay=10/12 itdelay = 1/4 it 
wcet220 ≤ k1delay=37/39 itdelay=37/40 itdelay = 5/8 it 
Figure 3: Some examples with proof goals



We would like to thank Paul Feautrier for his precious comments on polyhedra generation and for his benchmarks.


S. Bardin, A. Finkel, J. Leroux, and L. Petrucci. Fast: Fast acceleration of symbolic transition systems. In CAV’03, pages 118–121, Boulder (Colorado), July 2003. LNCS 2725, Springer-Verlag.
R. Bagnara, P. M. Hill, E. Ricci, and E. Zaffanella. Precise widening operators for convex polyhedra. In R. Cousot, editor, Static Analysis: Proceedings of the 10th International Symposium, volume 2694 of Lecture Notes in Computer Science, pages 337–354, San Diego, California, USA, 2003. Springer-Verlag, Berlin.
L. Gonnord and N. Halbwachs. Combining widening and acceleration in linear relation analysis. In 13th International Static Analysis Symposium, SAS’06, Seoul, Korea, August 2006.
Laure Gonnord. Accélération abstraite pour l’amélioration de la précision en Analyse des Relations Linéaires. Thèse de doctorat, Université Joseph Fourier, Grenoble, October 2007.
D. Gopan and T. Reps. Lookahead widening. In CAV’06, Seattle, 2006.
N. Halbwachs. Détermination automatique de relations linéaires vérifiées par les variables d’un programme. Thèse de troisième cycle, University of Grenoble, March 1979.
J. Leroux. Algorithmique de la vérification des systèmes à compteurs – approximation et accélération – implémentation dans l’outil Fast. Phd thesis, Ecole Normale Supérieure de Cachan, December 2003.
S. Sankaranarayanan, H. Sipma, and Z. Manna. Constraint-based linear relations analysis. In International Symposium on Static Analysis, SAS’2004, pages 53–68. LNCS 3148, Springer Verlag, 2004.

Ce document a été traduit de LATEX par HEVEA