Automatic Verification of Recursive Procedures with one Integer Parameter

       Ahmed Bouajjani, Richard Mayr and Peter Habermehl


R‚sum‚:

Context-free processes (BPA) have been used for dataflow-analysis in
recursive procedures with applications in optimizing compilers. 
We introduce a more refined model called BPA(Z) that can model not
only recursive dependencies, but also the passing of integer
parameters to subroutines. Moreover, these parameters can be tested 
against conditions expressible in Presburger-arithmetic. This new 
and more expressive model can still be analyzed automatically. We 
define Z-input 1-CM, a new class of one-counter machines that take 
integer numbers as input, to describe sets of configurations of
BPA(Z). 
We show that the Post* (the set of successors) of a set of
BPA(Z)-configurations described by a Z-input 1-CM can be effectively
constructed. The Pre* (set of predecessors) of a regular set can be
effectively constructed as well. However, the Pre* of a set described
by a Z-input 1-CM cannot be represented by a Z-input 1-CM in general
and has an undecidable membership problem. Then we develop a new
temporal logic based on reversal-bounded counter machines that can be 
used to describe properties of BPA(Z) and show that the model-checking 
problem is decidable.

Abstract:

Les processus hors-contextes (BPA) sont utilis‚s pour l'analyse de
flot de donn‚es dans des proc‚dures r‚cursives avec des
applications dans l'optimisation de compilateur. Nous introduisons un
modŠle plus raffin‚ appel‚ BPA(Z) qui peut mod‚lis‚ non
seulement des d‚pendances r‚cursives mais aussi le passage de
paramŠtres entiers vers les proc‚dures. En plus, ces
paramŠtres peuvent ˆtre test‚s par rapport … des
conditions exprim‚es en arithm‚tique de Presburger. Ce nouveau
modŠle plus expressif peut toujours ˆtre analys‚
automatiquement. Pour d‚crire des ensembles de configurations de
BPA(Z) nous d‚finissons les Z-entr‚e 1-CM, une nouvelle classe
de machines … un compteur qui prend des entiers comme entr‚es. 
Nous montrons que le Post* (l'ensemble des successeurs) d'un ensemble 
de configurations de BPA(Z) d‚crit par une Z-entr‚e 1-CM est
constructible. Le Pre* (l'ensemble des pr‚d‚cesseurs) d'un
ensemble r‚gulier de configuration est aussi
constructible. N‚anmoins, le Pre* d'un ensemble d‚crit par une
Z-entr‚e 1-CM ne peut en g‚n‚ral pas ˆtre d‚crit par
une Z-entr‚e 1-CM et son problŠme d'appartenance est
ind‚cidable. Ensuite nous introduisons une nouvelle logique
temporelle bas‚e sur les machines … compteurs avec renversement
fini. Cette logique peut ˆtre utilis‚e pour d‚crire des
propri‚t‚s des BPA(Z) et nous montrons que le problŠme du 
model-checking est d‚cidable.