Types and higher-order recursion schemes for verification of higher-order programs

ABSTRACT

We propose a new verification method for temporal properties of higher-order functional programs, which takes advantage of Ong's recent result on the decidability of the model-checking problem for higher-order recursion schemes (HORS's). A program is transformed to an HORS that generates a tree representing all the possible event sequences of the program, and then the HORS is model-checked. Unlike most of the previous methods for verification of higher-order programs, our verification method is sound and complete. Moreover, this new verification framework allows a smooth integration of abstract model checking techniques into verification of higher-order programs. We also present a type-based verification algorithm for HORS's. The algorithm can deal with only a fragment of the properties expressed by modal mu-calculus, but the algorithm and its correctness proof are (arguably) much simpler than those of Ong's game-semantics-based algorithm. Moreover, while the HORS model checking problem is n-EXPTIME in general, our algorithm is linear in the size of HORS, under the assumption that the sizes of types and specification formulas are bounded by a constant.

REFERENCES

• 1: K. Aehlig. A finite semantics of simply-typed lambda terms for infinite runs of automata. Logical Methods in Computer Science, 3(3), 2007.
• 2: K. Aehlig, J. G. de Miranda, and C.-H. L. Ong. The monadic second order theory of trees given by arbitrary level--tworecursion schemes is decidable. In TLCA 2005, volume 3461 of LNCS, pages 39--54.Springer-Verlag, 2005.
• 3: Thomas Ball , Rupak Majumdar , Todd Millstein , Sriram K. Rajamani, Automatic predicate abstraction of C programs, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.203-213, June 2001, Snowbird, Utah, United States
• 4: 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
• 5: 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]
• 6: Sagar Chaki , Sriram K. Rajamani , Jakob Rehof, Types as models: model checking message-passing programs, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.45-57, January 16-18, 2002, Portland, Oregon
• 7: Byron Cook , Alexey Gotsman , Andreas Podelski , Andrey Rybalchenko , Moshe Y. Vardi, Proving that programs eventually do something good, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 8: Manuel Fahndrich , Robert DeLine, Adoption and focus: practical linear types for imperative programming, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 9: 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, October 01-04, 1991, San Juan, Puerto Rico [doi>10.1109/SFCS.1991.185392]
• 10: J. Field , D. Goyal , G. Ramalingam , E. Yahav, Typestate verification: abstraction techniques and complexity results, Science of Computer Programming, v.58 n.1-2, p.57-82, October 2005 [doi>10.1016/j.scico.2005.02.004]
• 11: Stephen J. Fink , Eran Yahav , Nurit Dor , G. Ramalingam , Emmanuel Geay, Effective typestate verification in the presence of aliasing, ACM Transactions on Software Engineering and Methodology (TOSEM), v.17 n.2, p.1-34, April 2008 [doi>10.1145/1348250.1348255]
• 12: Jeffrey S. Foster , Tachio Terauchi , Alex Aiken, Flow-sensitive type qualifiers, Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, June 17-19, 2002, Berlin, Germany
• 13: Christian Haack , J. B. Wells, Type error slicing in implicitly typed higher-order languages, Science of Computer Programming, v.50 n.1-3, p.189-224, March 2004 [doi>10.1016/j.scico.2004.01.004]
• 14: M. Hague and C.-H. L. Ong. Symbolic backwards-reachability analysis for higher-order pushdown In FoSSaCS 2007, volume 4423 of LNCS, pages 213--227. Springer-Verlag, 2007.
• 15: Nevin Heintze , David McAllester, Linear-time subtransitive control flow analysis, Proceedings of the ACM SIGPLAN 1997 conference on Programming language design and implementation, p.261-272, June 16-18, 1997, Las Vegas, Nevada, United States
• 16: Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar , Grégoire Sutre, Lazy abstraction, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.58-70, January 16-18, 2002, Portland, Oregon
• 17: Haruo Hosoya , Jérôme Vouillon , Benjamin C. Pierce, Regular expression types for XML, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.1, p.46-90, January 2005 [doi>10.1145/1053468.1053470]
• 18: Atsushi Igarashi , Naoki Kobayashi, A generic type system for the Pi-calculus, Theoretical Computer Science, v.311 n.1-3, p.121-163, 23 January 2004 [doi>10.1016/S0304-3975(03)00325-6]
• 19: Atsushi Igarashi , Naoki Kobayashi, Resource usage analysis, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.2, p.264-313, March 2005 [doi>10.1145/1057387.1057390]
• 20: Futoshi Iwama , Atsushi Igarashi , Naoki Kobayashi, Resource usage analysis for a functional language with exceptions, Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 09-10, 2006, Charleston, South Carolina [doi>10.1145/1111542.1111550]
• 21: D. Kikuchi and N. Kobayashi. Type-based verification of correspondence assertions for communication protocols. In Proceedings of APLAS 2007, volume 4807 of LNCS, pages 191--205. Springer-Verlag, 2007.
• 22: T. Knapik, D. Niwinski, and P. Urzyczyn. Deciding monadic theories of hyperalgebraic trees. Deciding monadic theories of hyperalgebraic trees. Springer-Verlag, 2001.
• 23: Teodor Knapik , Damian Niwinski , Pawel Urzyczyn, Higher-Order Pushdown Trees Are Easy, Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures, p.205-222, April 08-12, 2002
• 24: T. Knapik, D. Niwinski, P. Urzyczyn, and I. Walukiewicz. Unsafe grammars and panic automata. Unsafe grammars and panic automata. Springer-Verlag, 2005.
• 25: N. Kobayashi. Types and higher-order recursion schemes for verification of higher-order programs. An extended version, available from http://www.kb.ecei.tohoku.ac.jp/ koba/papers/hors.pdf, 2008.
• 26: P. Lam, V. Kuncak, and M. C. Rinard. Generalized typestate checking for data structure consistency. In VMCAI 2005, volume 3385 of LNCS, pages 430--447.Springer-Verlag, 2005.
• 27: M. Naik. A type system equivalent to a model checker. Master Thesis, Purdue University.
• 28: M. Naik and J. Palsberg. A type system equivalent to a model checker. In ESOP 2005, volume 3444 of LNCS, pages 374--388. Springer-Verlag, 2005.
• 29: C.-H. L. Ong, On Model-Checking Trees Generated by Higher-Order Recursion Schemes, Proceedings of the 21st Annual IEEE Symposium on Logic in Computer Science, p.81-90, August 12-15, 2006 [doi>10.1109/LICS.2006.38]
• 30: Jakob Rehof , Torben Ægidius Mogensen, Tractable constraints in finite semilattices, Science of Computer Programming, v.35 n.2-3, p.191-221, Nov.1.1999 [doi>10.1016/S0167-6423(99)00011-8]
• 31: Patrick M. Rondon , Ming Kawaguci , Ranjit Jhala, Liquid types, Proceedings of the 2008 ACM SIGPLAN conference on Programming language design and implementation, June 07-13, 2008, Tucson, AZ, USA
• 32: R E Strom , S Yemini, Typestate: A programming language concept for enhancing software reliability, IEEE Transactions on Software Engineering, v.12 n.1, p.157-171, Jan. 1986
• 33: Wolfgang Thomas, Languages, automata, and logic, Handbook of formal languages, vol. 3: beyond words, Springer-Verlag New York, Inc., New York, NY, 1997
• 34: H. Unno and N. Kobayashi. On-demand refinement of dependent types. In Proceedings of FLOPS 2008, volume 4989 of LNCS, pages 81--96. Springer-Verlag, 2008.

INDEX TERMS

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

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs

General Terms:
Languages, Verification

Keywords:
higher-order recursion scheme, model checking, type system