Paper Info
Title
Automatic verification of recursive procedures with one integer parameter
Abstract
Context-free processes (BPA) have been used for dataflow analysis in recursive procedures with applications in optimizing compilers (Proceedings of FOSSaCS¿99, Lecture Notes in Computer Science, Vol. 1578, Springer, Berlin, 1999, pp. 14¿30). We introduce a more refined model called BPA(Z) that can model not only recursive dependencies, but also the passing of an integer parameter to a subroutine. Moreover, this parameter 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 1-counter machines (cm) 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 (i.e. machines which use counters such that the change between increasing and decreasing mode of each counter is bounded (J. Assoc. Comput. Mach. 25 (1978) 116) that can be used to describe properties of BPA(Z) and show that the model-checking problem is decidable.
Year
DOI
Venue
2003
10.1016/S0304-3975(02)00397-3
Theoretical Computer Science - Mathematical foundations of computer science
Keywords
DocType
Volume
recursive dependency,new temporal logic,automatic verification,recursive procedure,integer parameter,Model checking,Z-input 1-CM,Context-free processes,Verification,integer number,new class,regular set,model-checking problem,refined model,expressive model
Journal
295
Issue
ISSN
ISBN
1-3
Theoretical Computer Science
3-540-42496-2
Citations 
PageRank 
References 
21
1.14
14
Authors
3
Name
Order
Citations
PageRank
Ahmed Bouajjani12663184.84
Peter Habermehl250230.39
Richard Mayr31356.64