Analyzing recursive programs using a fixed-point calculus

ABSTRACT

We show that recursive programs where variables range over finite domains can be effectively and efficiently analyzed by describing the analysis algorithm using a formula in a fixed-point calculus. In contrast with programming in traditional languages, a fixed-point calculus serves as a high-level programming language to easily, correctly, and succinctly describe model-checking algorithms While there have been declarative high-level formalisms that have been proposed earlier for analysis problems (e.g., Datalog the fixed-point calculus we propose has the salient feature that it also allows algorithmic aspects to be specified.

We exhibit two classes of algorithms of symbolic (BDD-based) algorithms written using this framework-- one for checking for errors in sequential recursive Boolean programs, and the other to check for errors reachable within a bounded number of context-switches in a concurrent recursive Boolean program. Our formalization of these otherwise complex algorithms is extremely simple, and spans just a page of fixed-point formulae. Moreover, we implement these algorithms in a tool called Getafix which expresses algorithms as fixed-point formulae and evaluates them efficiently using a symbolic fixed-point solver called Mucke. The resulting model-checking tools are surprisingly efficient and are competitive in performance with mature existing tools that have been fine-tuned for these problems.

REFERENCES

• 1: Rajeev Alur , Michael Benedikt , Kousha Etessami , Patrice Godefroid , Thomas Reps , Mihalis Yannakakis, Analysis of recursive state machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.4, p.786-818, July 2005 [doi>10.1145/1075382.1075387]
• 2: Rajeev Alur , Michael McDougall , Zijiang Yang, Exploiting Behavioral Hierarchy for Efficient Model Checking, Proceedings of the 14th International Conference on Computer Aided Verification, p.338-342, July 27-31, 2002
• 3: T. Ball, B. Cook, V. Levin, and S. K. Rajamani. SLAM and Static Driver Verifier: Technology transfer of formal methods inside Microsoft. In E. A. Boiten, J. Derrick, and G. Smith, editors, IFM, volume 2999 of Lecture Notes in Computer Science, pages 1--20. Springer, 2004.
• 4: 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
• 5: 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
• 6: Dirk Beyer , Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar, The software model checker Blast: Applications to software engineering, International Journal on Software Tools for Technology Transfer (STTT), v.9 n.5, p.505-525, October 2007 [doi>10.1007/s10009-007-0044-z]
• 7: Armin Biere, µcke - Efficient µ-Calculus Model Checking, Proceedings of the 9th International Conference on Computer Aided Verification, p.468-471, June 22-25, 1997
• 8: J. R. Buchi. Regular canonical systems. Arch. Math. Logik Grundlagenforschung, 6:91--111, 1964.
• 9: Swarat Chaudhuri, Subcubic algorithms for recursive state machines, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 10: B. Cook, A. Podelski, and A. Rybalchenko. Terminator: Beyond safety. In T. Ball and R. B. Jones, editors, CAV, volume 4144 of Lecture Notes in Computer Science, pages 415--418. Springer, 2006.
• 11: Javier Esparza , Stefan Schwoon, A BDD-Based Model Checker for Recursive Programs, Proceedings of the 13th International Conference on Computer Aided Verification, p.324-336, July 18-22, 2001
• 12: Akash Lal , Thomas Reps, Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis, Proceedings of the 20th international conference on Computer Aided Verification, July 07-14, 2008, Princeton, NJ, USA [doi>10.1007/978-3-540-70545-1_7]
• 13: Monica S. Lam , John Whaley , V. Benjamin Livshits , Michael C. Martin , Dzintars Avots , Michael Carbin , Christopher Unkel, Context-sensitive program analysis as database queries, Proceedings of the twenty-fourth ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, June 13-15, 2005, Baltimore, Maryland [doi>10.1145/1065167.1065169]
• 14: Ondřej Lhoták , Laurie Hendren, Jedd: a BDD-based relational extension of Java, Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 09-11, 2004, Washington DC, USA
• 15: Madanlal Musuvathi , Shaz Qadeer, Iterative context bounding for systematic testing of multithreaded programs, Proceedings of the 2007 ACM SIGPLAN conference on Programming language design and implementation, June 10-13, 2007, San Diego, California, USA
• 16: Proceedings of the ACM SIGPLAN 2004 conference on Programming language design and implementation, June 2004
• 17: S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In N. Halbwachs and L. D. Zuck, editors, TACAS, volume 3440 of Lecture Notes in Computer Science, pages 93--107. Springer, 2005.
• 18: S. Qadeer and D. Wu. Kiss: keep it simple and sequential. In Pugh and Chambers {16}, pages 14--24.
• 19: 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]
• 20: T.W. Reps, S. Schwoon, and S. Jha. Weighted pushdown systems and their application to interprocedural dataflow analysis. In R. Cousot, editor, SAS, volume 2694 of Lecture Notes in Computer Science, pages 189--213. Springer, 2003.
• 21: S. Schwoon. Model-Checking Pushdown Systems. PhD thesis, Technische Universitat Munchen, 2002.
• 22: M. Sharir and A. Pnueli. Two approaches to inter-procedural data-flow analysis. In Program Flow Analysis: Theory and Applications, 1981.
• 23: Dejvuth Suwimonteerabuth , Javier Esparza , Stefan Schwoon, Symbolic Context-Bounded Analysis of Multithreaded Java Programs, Proceedings of the 15th international workshop on Model Checking Software, August 10-12, 2008, Los Angeles, CA, USA [doi>10.1007/978-3-540-85114-1_19]
• 24: 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]
• 26: J. Whaley and M. S. Lam. Cloning-based context-sensitive pointer alias analysis using binary decision diagrams. In Pugh and Chambers {16}, pages 131--144.

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, Experimentation, Verification

Keywords:
abstraction, logic, model-checking, mu-calculus, recursive systems, software verification