Automatic verification of recursive procedures with one integer parameter.

*(English)*Zbl 1005.68096
Sgall, Jiří (ed.) et al., Mathematical foundations of computer science 2001. 26th international symposium, MFCS 2001, Mariánské Lázně, Czech Republic, August 27-31, 2001. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 2136, 198-211 (2001).

Summary: Context-free processes (BPA) have been used for dataflow-analysis in recursive procedures with applications in optimizing compilers by J. Esparza and J. Knoop (1999). We introduce a more refined model called BPA\((\mathbb{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 \(\mathbb{Z}\)-input 1-CM, a new class of one-counter machines that take integer numbers as input, to describe sets of configurations of BPA\((\mathbb{Z})\). We show that the \(\text{Post}^*\) (the set of successors) of a set of BPA\((\mathbb{Z})\)-configurations described by a \(\mathbb{Z}\)-input 1-CM can be effectively constructed. The \(\text{Pre}^*\) (set of predecessors) of a regular set can be effectively constructed as well. However, the \(\text{Pre}^*\) of a set described by a \(\mathbb{Z}\)-input 1-CM cannot be represented by a \(\mathbb{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\((\mathbb{Z})\) and show that the model-checking problem is decidable.

For the entire collection see [Zbl 0969.00078].

For the entire collection see [Zbl 0969.00078].