A fixpoint calculus for local and global program flows

ABSTRACT

We define a new fixpoint modal logic, the visibly pushdown μ-calculus (VP-μ), as an extension of the modal μ-calculus. The models of this logic are execution trees of structured programs where the procedure calls and returns are made visible. This new logic can express pushdown specifications on the model that its classical counterpart cannot, and is motivated by recent work on visibly pushdown languages [4]. We show that our logic naturally captures several interesting program specifications in program verification and dataflow analysis. This includes a variety of program specifications such as computing combinations of local and global program flows, pre/post conditions of procedures, security properties involving the context stack, and interprocedural dataflow analysis properties. The logic can capture flow-sensitive and inter-procedural analysis, and it has constructs that allow skipping procedure calls so that local flows in a procedure can also be tracked. The logic generalizes the semantics of the modal μ-calculus by considering summaries instead of nodes as first-class objects, with appropriate constructs for concatenating summaries, and naturally captures the way in which pushdown models are model-checked. The main result of the paper is that the model-checking problem for VP-μ is effectively solvable against pushdown models with no more effort than that required for weaker logics such as CTL. We also investigate the expressive power of the logic VP-μ: we show that it encompasses all properties expressed by a corresponding pushdown temporal logic on linear structures (caret [2]) as well as by the classical μ-calculus. This makes VP-μ the most expressive known program logic for which algorithmic software model checking is feasible. In fact, the decidability of most known program logics (μ-calculus, temporal logics LTL and CTL, caret, etc.) can be understood by their interpretation in the monadic second-order logic over trees. This is not true for the logic VP-μ, making it a new powerful tractable program logic.

REFERENCES

• 1: R. Alur, S. Chaudhuri, and P. Madhusudan. Visibly pushdown tree languages. http://www.cis.upenn.edu/~swarat/pubs/vptl.ps+.
• 2: R. Alur, K. Etessami, and P. Madhusudan. A temporal logic of nested calls and returns. In 10th Int. Conf. on Tools and Algorithms for the Const. and Analysis of Software, LNCS 2988, pages 467--481, 2004.
• 3: Rajeev Alur , Kousha Etessami , Mihalis Yannakakis, Analysis of Recursive State Machines, Proceedings of the 13th International Conference on Computer Aided Verification, p.207-220, July 18-22, 2001
• 4: Rajeev Alur , P. Madhusudan, Visibly pushdown languages, Proceedings of the thirty-sixth annual ACM symposium on Theory of computing, June 13-16, 2004, Chicago, IL, USA [doi>10.1145/1007352.1007390]
• 5: Thomas Ball , Sriram K. Rajamani, Bebop: A Symbolic Model Checker for Boolean Programs, Proceedings of the 7th International SPIN Workshop on SPIN Model Checking and Software Verification, p.113-130, August 30-September 01, 2000
• 6: Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
• 7: Michael Benedikt , Patrice Godefroid , Thomas W. Reps, Model Checking of Unrestricted Hierarchical State Machines, Proceedings of the 28th International Colloquium on Automata, Languages and Programming,, p.652-666, July 08-12, 2001
• 8: J. R. Burch , E. M. Clarke , K. L. McMillan , D. L. Dill , L. J. Hwang, Symbolic model checking: 1020 states and beyond, Information and Computation, v.98 n.2, p.142-170, June 1992 [doi>10.1016/0890-5401(92)90017-A]
• 9: L. Burdy, Y. Cheon, D. Cok, M. Ernst, J. Kiniry, G.T. Leavens, R. Leino, and E. Poll. An overview of JML tools and applications. In Proceedings of the 8th International Workshop on Formal Methods for Industrial Critical Systems, pages 75--89, 2003.
• 10: Olaf Burkart , Bernhard Steffen, Model checking the full modal mu-calculus for infinite sequential processes, Theoretical Computer Science, v.221 n.1-2, p.251-270, June 28, 1999 [doi>10.1016/S0304-3975(99)00034-1]
• 11: K. Chatterjee, D. Ma, R. Majumdar, T. Zhao, T.A. Henzinger, and J. Palsberg. Stack size analysis for interrupt driven programs. In Proceedings of the 10th International Symposium on Static Analysis, volume LNCS 2694, pages 109--126, 2003.
• 12: Hao Chen , David Wagner, MOPS: an infrastructure for examining security properties of software, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA [doi>10.1145/586110.586142]
• 13: E. Allen Emerson, Temporal and modal logic, Handbook of theoretical computer science (vol. B): formal models and semantics, MIT Press, Cambridge, MA, 1991
• 14: E. A. Emerson , C. S. Jutla, Tree automata, Mu-Calculus and determinacy, Proceedings of the 32nd annual symposium on Foundations of computer science, p.368-377, September 1991, San Juan, Puerto Rico [doi>10.1109/SFCS.1991.185392]
• 15: Javier Esparza , Antonín Kucera , Stefan Schwoon, Model checking LTL with regular valuations for pushdown systems, Information and Computation, v.186 n.2, p.355-376, 01 November 2003 [doi>10.1016/S0890-5401(03)00139-1]
• 16: E. Grädel, W. Thomas, and T. Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research {outcome of a Dagstuhl seminar, February 2001}, volume 2500 of Lecture Notes in Computer Science. Springer, 2002.
• 17: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , George C. Necula , Grégoire Sutre , Westley Weimer, Temporal-Safety Proofs for Systems Code, Proceedings of the 14th International Conference on Computer Aided Verification, p.526-538, July 27-31, 2002
• 18: David Janin , Igor Walukiewicz, On the Expressive Completeness of the Propositional mu-Calculus with Respect to Monadic Second Order Logic, Proceedings of the 7th International Conference on Concurrency Theory, p.263-277, August 26-29, 1996
• 19: T. Jensen, D. Le Metayer, and T. Thorn. Verification of control flow based security properties. In Proceedings of the IEEE Symposium on Security and Privacy, pages 89--103, 1999.
• 20: D. Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27:333--354, 1983.
• 21: Kenneth L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, Norwell, MA, 1993
• 22: Thomas Reps , Susan Horwitz , Mooly Sagiv, Precise interprocedural dataflow analysis via graph reachability, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.49-61, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199462]
• 23: David A. Schmidt, Data flow analysis is model checking of abstract interpretations, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.38-48, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268950]
• 24: Bernhard Steffen, Data Flow Analysis as Model Checking, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.346-365, September 24-27, 1991
• 25: Colin Stirling, Modal and temporal logics, Handbook of logic in computer science (vol. 2): background: computational structures, Oxford University Press, Inc., New York, NY, 1993
• 26: Igor Walukiewicz, Pushdown processes: games and model-checking, Information and Computation, v.164 n.2, p.234-263, Jan. 29, 2001 [doi>10.1006/inco.2000.2894]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Model checking

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic
          Subjects: Temporal logic

General Terms:
Algorithms, Theory, Verification

Keywords:
μ-calculus, games, infinite-state, logic, model-checking, pushdown systems, specification, verification