×

zbMATH — the first resource for mathematics

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].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
03B25 Decidability of theories and sets of sentences
03B44 Temporal logic
68Q45 Formal languages and automata
PDF BibTeX XML Cite