Abstract
While temporal verification of programs is a topic with a long history, its traditional basis—semantics based on word languages—is ill-suited for modular reasoning about procedural programs. We address this issue by defining the semantics of procedural (potentially recursive) programs using languages of nested words and developing a framework for temporal reasoning around it. This generalization has two benefits. First, this style of reasoning naturally unifies Manna-Pnueli-style temporal reasoning with Hoare-style reasoning about structured programs. Second, it allows verification of “non-regular” properties of specific procedural contexts—e.g., “If a lock is acquired in a context, then it is released in the same context.” We present proof rules for a variety of properties such as local safety, local response, and staircase reactivity; our rules are sufficient to prove all temporal properties over nested words. We show that our rules are sound and relatively complete.
This research was partially supported by NSF award CCF-0905464.
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.
Similar content being viewed by others
References
Alur, R., Arenas, M., Barceló, P., Etessami, K., Immerman, N., Libkin, L.: First-order and temporal logics for nested words. In: Proceedings of LICS, pp. 151–160 (2007)
Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 467–481. Springer, Heidelberg (2004)
Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM (2009)
Apt, K.R.: Ten years of Hoare’s logic: A survey—part I. ACM Transactions on Programming Languages and Systems 3(4), 431–483 (1981)
Arenas, M., Barceló, P., Libkin, L.: Regular languages of nested words: Fixed points, automata, and synchronization. In: Arge, L., Cachin, C., Jurdziński, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 888–900. Springer, Heidelberg (2007)
Ball, T., Rajamani, S.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 260–264. Springer, Heidelberg (2001)
Bradley, A., Manna, Z.: The Calculus of Computation. Springer, Heidelberg (2007)
Cook, B., Podelski, A., Rybalchenko, A.: Summarization for termination: no return! Formal Methods for System Design (2009)
Dillig, I., Dillig, T., Aiken, A.: Sound, complete and scalable path-sensitive analysis. In: PLDI, pp. 270–280 (2008)
Heizmann, M., Hoenicke, J., Podelski, A.: Nested interpolants. In: Proceedings of POPL (2010)
Henzinger, T.A., Jhala, R., Majumdar, R., Necula, G.C., Sutre, G., Weimer, W.: Temporal-safety proofs for systems code. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 526–538. Springer, Heidelberg (2002)
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580 (1969)
Löding, C., Madhusudan, P., Serre, O.: Visibly pushdown games. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 408–420. Springer, Heidelberg (2004)
Manna, Z., Pnueli, A.: Completing the temporal picture. Theoretical Computer Science 83(1), 91–130 (1991)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Safety. Springer, New York (1995)
Manna, Z., Pnueli, A.: The Temporal Logic of Reactive and Concurrent Systems: Progress (1996)
Pnueli, A.: The temporal logic of programs. In: Proceedings of FOCS, pp. 46–77 (1977)
Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 239–251. Springer, Heidelberg (2004)
Podelski, A., Schaefer, I., Wagner, S.: Summaries for while programs with recursion. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 94–107. Springer, Heidelberg (2005)
Reps, T., Horwitz, S., Sagiv, S.: Precise interprocedural dataflow analysis via graph reachability. In: Proc. of POPL, pp. 49–61 (1995)
Reps, T.W., Schwoon, S., Jha, S.: Weighted pushdown systems and their application to interprocedural dataflow analysis. In: Proceedings of SAS, pp. 189–213 (2003)
Sharir, M., Pnueli, A.: Two approaches to interprocedural dataflow analysis. Program Flow Analysis: Theory and Applications, 189–234 (1981)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Alur, R., Chaudhuri, S. (2010). Temporal Reasoning for Procedural Programs. In: Barthe, G., Hermenegildo, M. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2010. Lecture Notes in Computer Science, vol 5944. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11319-2_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-11319-2_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11318-5
Online ISBN: 978-3-642-11319-2
eBook Packages: Computer ScienceComputer Science (R0)