Abstract
Context-free processes (BPA) have been used for dataflow-analysis in recursive procedures with applications in optimizing compilers [6]. We introduce a more refined model called BPA(ℤ) 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 ℤ-input 1-CM, a new class of one-counter machines that take integer numbers as input, to describe sets of configurations of BPA(ℤ). We show that the Post* (the set of successors) of a set of BPA(ℤ)-configurations described by a ℤ-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 ℤ-input 1-CM cannot be represented by a ℤ-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(ℤ) and show that the model-checking problem is decidable.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: application to model checking. In International Conference on Concurrency Theory (CONCUR’97), volume 1243 of LNCS. Springer Verlag, 1997.
A. Bouajjani, P. Habermehl, and R. Mayr. Automatic Verification of Recursive Procedures with one Integer Parameter. Technical Report LIAFA, 2001. available at http://www.informatik.uni-freiburg.de/~mayrri/index.html
O. Burkart and B. Steffen. Pushdown processes: Parallel composition and model checking. In CONCUR’94, volume 836 of LNCS, pages 98–113. Springer Verlag, 1994.
O. Burkart and B. Steffen. Model checking the full modal mu-calculus for infinite sequential processes. In Proceedings of ICALP’97, volume 1256 of LNCS. Springer Verlag, 1997.
J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. In Proc. of CAV 2000, volume 1855 of LNCS. Springer, 2000.
J. Esparza and J. Knoop. An automata-theoretic approach to interprocedural data-flow analysis. In Proc. of FoSSaCS’99, volume 1578 of LNCS, pages 14–30. Springer Verlag, 1999.
O. Ibarra. Reversal-bounded multicounter machines and their decision problems. Journal of the ACM, 25:116–133, 1978.
O. Ibarra, T. Bultan, and J. Su. Reachability analysis for some models of infinite-state transition systems. In Proc. of CONCUR 2000, volume 1877 of LNCS. Springer, 2000.
R. Mayr. Undecidable problems in unreliable computations. In Proc. of LATIN 2000, volume 1776 of LNCS. Springer Verlag, 2000.
J. van Leeuwen, editor. Handbook of Theoretical Computer Science: Volume A, Algorithms and Complexity. Elsevier, 1990.
I. Walukiewicz. Pushdown processes: games and model checking. In International Conference on Computer Aided Verification (CAV’96), volume 1102 of LNCS. Springer, 1996.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bouajjani, A., Habermehl, P., Mayr, R. (2001). Automatic Verification of Recursive Procedures with One Integer Parameter. In: Sgall, J., Pultr, A., Kolman, P. (eds) Mathematical Foundations of Computer Science 2001. MFCS 2001. Lecture Notes in Computer Science, vol 2136. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44683-4_18
Download citation
DOI: https://doi.org/10.1007/3-540-44683-4_18
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42496-3
Online ISBN: 978-3-540-44683-5
eBook Packages: Springer Book Archive