Abstract
Pushdown systems (PDS) naturally model sequential recursive programs. Numeric data types also often arise in real-world programs. We study the extension of PDS with unbounded counters, which naturally model numeric data types. Although this extension is Turing-powerful, reachability is known to be decidable when the number of reversals between incrementing and decrementing modes is bounded. In this paper, we (1) pinpoint the decidability/complexity of reachability and linear/branching time model checking over PDS with reversal-bounded counters (PCo), and (2) experimentally demonstrate the effectiveness of our approach in analysing software. We show reachability over PCo is NP-complete, while LTL is coNEXP-complete (coNP-complete for fixed formulas). In contrast, we prove that EF-logic over PCo is undecidable. Our NP upper bounds are by a direct poly-time reduction to satisfaction over existential Presburger formulas, allowing us to tap into highly optimized solvers like Z3. Although reversal-bounded analysis is incomplete for PDS with unbounded counters in general, our experiments suggest that some intricate bugs (e.g. from Linux device drivers) can be discovered with a small number of reversals. We also pinpoint the decidability/complexity of various extensions of PCo, e.g., with discrete clocks.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Dill, D.L.: A Theory of Timed Automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
Ball, T., Cook, B., Levin, V., Rajamani, S.K.: SLAM and Static Driver Verifier: Technology Transfer of Formal Methods inside Microsoft. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 1–20. Springer, Heidelberg (2004)
Ball, T., Rajamani, S.K.: Bebop: A Symbolic Model Checker for Boolean Programs. In: SPIN 2000, pp. 113–130 (2000)
Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)
Bouyer, P.: Model-checking timed temporal logics. Electr. Notes Theor. Comput. Sci. 231, 323–341 (2009)
Cachat, T.: Uniform Solution of Parity Games on Prefix-Recognizable Graphs. Electr. Notes Theor. Comput. Sci. 68(6) (2002)
Chadha, R., Legay, A., Prabhakar, P., Viswanathan, M.: Complexity Bounds for the Verification of Real-Time Software. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 95–111. Springer, Heidelberg (2010)
Courcoubetis, C., Yannakakis, M.: Minimum and Maximum Delay Problems in Real-Time Systems. FMSD 1(4), 385–415 (1992)
Dang, Z.: Binary reachability analysis of pushdown timed automata with dense clocks. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, p. 506. Springer, Heidelberg (2001)
de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
D’Silva, V., Kroening, D., Weissenbacher, G.: A Survey of Automated Techniques for Formal Software Verification. IEEE Trans. on CAD of Integrated Circuits and Systems 27(7), 1165–1178 (2008)
Esparza, J., Kucera, A., Schwoon Model, S.: Model checking LTL with regular valuations for pushdown systems. Inf. Comput. 186(2), 355–376 (2003)
Filiot, E., Raskin, J.-F., Reynier, P.-A., Servais, F., Talbot, J.-M.: Properties of visibly pushdown transducers. In: Hliněný, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 355–367. Springer, Heidelberg (2010)
Finkel, A., Sangnier, A.: Reversal-bounded counter machines revisited. In: Ochmański, E., Tyszkiewicz, J. (eds.) MFCS 2008. LNCS, vol. 5162, pp. 323–334. Springer, Heidelberg (2008)
Gries, D.: The Science of Programming. Springer, Heidelberg (1981)
Gurari, E.M., Ibarra, O.H.: The Complexity of Decision Problems for Finite-Turn Multicounter Machines. J. Comput. Syst. Sci. 22(2), 220–229 (1981)
Hague, M.: Saturation Methods for Global Model-Checking Pushdown Systems. PhD thesis, Oxford University Computing Laboratory (2009)
Howell, R., Rosier, L.: An Analysis of the Nonemptiness Problem for Classes of Reversal-Bounded Multicounter Machines. J. Comput. Syst. Sci. 34(1), 55–74
Ibarra, O.H.: Reversal-Bounded Multicounter Machines and Their Decision Problems. J. ACM 25(1), 116–133 (1978)
Ibarra, O., Su, J., Dang, Z., Bultan, T., Kemmerer, R.: Counter machines and verification problems. Theor. Comput. Sci. 289, 165–189 (2002)
Jhala, R., McMillan, K.L.: A practical and complete approach to predicate refinement. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol. 3920, pp. 459–473. Springer, Heidelberg (2006)
Laroussinie, F., Meyer, A., Petonnet, E.: Counting CTL. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 206–220. Springer, Heidelberg (2010)
Papadimitriou, C.H., Steiglitz, K.: Combinatorial Optimization: Algorithms and Complexity. Dover Publications, Mineola (1998)
Parikh, R.: On context-free languages. J. ACM 13(4), 570–581 (1966)
Patterson, A.: PCI: fix memory leak in aer_inject (2003), https://patchwork.kernel.org/patch/53058/
Scarpellini, B.: Complexity of Subcases of Presburger Arithmetic. Trans. of AMS 284(1), 203–218 (1984)
Sipser, M.: Introduction to the Theory of Computation. PWS Publishing Co. (1997)
Sistla, A.P., Clarke, E.M.: The Complexity of Propositional Linear Temporal Logics. J. ACM 32(3), 733–749 (1985)
Suwimonteerabuth, D., Schwoon, S., Esparza, J.: jMoped: A Java Bytecode Checker Based on Moped. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 541–545. Springer, Heidelberg (2005)
Thornbur, J.: dm: Fix memory leak in dm_register_target() (2003), http://lkml.org/lkml/2003/6/9/70
To, A.W.: Model Checking Infinite-State Systems: Generic and Specific Approaches. PhD thesis, School of Informatics, University of Edinburgh (2010)
Vardi, M.Y., Wolper, P.: An Automata-Theoretic Approach to Automatic Program Verification. In: LICS 1986, pp. 332–344 (1986)
Veith, H.: Languages Represented by Boolean Formulas. Inf. Process. Lett. 63(5), 251–256 (1997)
Verma, K.N., Seidl, H., Schwentick, T.: On the Complexity of Equational Horn Clauses. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 337–352. Springer, Heidelberg (2005)
Walukiewicz, I.: Model Checking CTL Properties of Pushdown Systems. In: FSTTCS 2000, pp. 127–138 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Hague, M., Lin, A.W. (2011). Model Checking Recursive Programs with Numeric Data Types. In: Gopalakrishnan, G., Qadeer, S. (eds) Computer Aided Verification. CAV 2011. Lecture Notes in Computer Science, vol 6806. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22110-1_60
Download citation
DOI: https://doi.org/10.1007/978-3-642-22110-1_60
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22109-5
Online ISBN: 978-3-642-22110-1
eBook Packages: Computer ScienceComputer Science (R0)