Abstract
Model checking of higher-order recursion schemes (HORS, for short) has been recently studied as a new promising technique for automated verification of higher-order programs. The previous HORS model checking could however deal with only simply-typed programs, so that its application was limited to functional programs. To deal with a broader range of programs such as object-oriented programs and multi-threaded programs, we extend HORS model checking to check properties of programs with recursive types. Although the extended model checking problem is undecidable, we develop a sound model-checking algorithm that is relatively complete with respect to a recursive intersection type system and prove its correctness. Preliminary results on the implementation and applications to verification of object-oriented programs and multi-threaded programs are also reported.
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.
Download to read the full chapter text
Chapter PDF
References
Barnett, M., DeLine, R., Fähndrich, M., Jacobs, B., Leino, K.R.M., Schulte, W., Venter, H.: The Spec# Programming System: Challenges and Directions. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 144–152. Springer, Heidelberg (2008)
Cardelli, L.: A semantics of multiple inheritance. Info. Comput. 76(2/3), 138–164 (1988)
Corbett, J.C., Dwyer, M.B., Hatcliff, J., Laubach, S., Pasareanu, C.S., Robby, Zheng, H.: Bandera: extracting finite-state models from Java source code. In: ICSE, pp. 439–448 (2000)
Havelund, K., Pressburger, T.: Model checking JAVA programs using JAVA pathfinder. STTT 2(4), 366–381 (2000)
Igarashi, A., Pierce, B.C., Wadler, P.: Featherweight Java: a minimal core calculus for Java and GJ. ACM Trans. Prog. Lang. Syst. 23(3), 396–450 (2001)
Kahlon, V.: Reasoning about Threads with Bounded Lock Chains. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 450–465. Springer, Heidelberg (2011)
Kamin, S.N., Reddy, U.S.: Two semantic models of object-oriented languages. In: Gunter, C.A., Mitchell, J.C. (eds.) Theoretical Aspects of Object-Oriented Programming, ch. 13, pp. 463–496. The MIT Press (1993)
Kobayashi, N.: Model-checking higher-order functions. In: Proceedings of PPDP 2009, pp. 25–36. ACM Press (2009)
Kobayashi, N.: Types and higher-order recursion schemes for verification of higher-order programs. In: Proc. of POPL, pp. 416–428 (2009)
Kobayashi, N., Igarashi, A.: Model-checking higher-order programs with recursive types (2012), An extended version available from http://www-kb.is.s.u-tokyo.ac.jp/~koba/fjmc/
Kobayashi, N., Ong, C.-H.L.: A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes. In: Proceedings of LICS 2009, pp. 179–188 (2009)
Kobayashi, N., Ong, C.-H.L.: Complexity of model checking recursion schemes for fragments of the modal mu-calculus. Logical Methods in Computer Science 7(4) (2011)
Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and cegar for higher-order model checking. In: Proc. of PLDI (2011)
Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. In: Proc. of POPL, pp. 495–508 (2010)
Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: LICS 2006, pp. 81–90 (2006)
Ong, C.-H.L., Ramsay, S.: Verifying higher-order programs with pattern-matching algebraic data types. In: Proc. of POPL, pp. 587–598 (2011)
Palsberg, J.: Equality-based flow analysis versus recursive types. ACM Trans. Prog. Lang. Syst. 20(6), 1251–1264 (1998)
Parkinson, M.J., Bierman, G.M.: Separation logic, abstraction and inheritance. In: Proc. of POPL, pp. 75–86 (2008)
Qadeer, S., Rehof, J.: Context-Bounded Model Checking of Concurrent Software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005)
Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Prog. Lang. Syst. 22(2), 416–430 (2000)
Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: PLDI 2008, pp. 159–169 (2008)
Rowe, R., Van Bakel, S.: Approximation Semantics and Expressive Predicate Assignment for Object-Oriented Programming (Extended Abstract). In: Ong, L. (ed.) TLCA 2011. LNCS, vol. 6690, pp. 229–244. Springer, Heidelberg (2011)
Skalka, C.: Types and trace effects for object orientation. Higher-Order and Symbolic Computation 21(3), 239–282 (2008)
Tsukada, T., Kobayashi, N.: Untyped Recursion Schemes and Infinite Intersection Types. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 343–357. Springer, Heidelberg (2010)
Unno, H., Tabuchi, N., Kobayashi, N.: Verification of Tree-Processing Programs via Higher-Order Model Checking. In: Ueda, K. (ed.) APLAS 2010. LNCS, vol. 6461, pp. 312–327. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kobayashi, N., Igarashi, A. (2013). Model-Checking Higher-Order Programs with Recursive Types. In: Felleisen, M., Gardner, P. (eds) Programming Languages and Systems. ESOP 2013. Lecture Notes in Computer Science, vol 7792. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-37036-6_24
Download citation
DOI: https://doi.org/10.1007/978-3-642-37036-6_24
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-37035-9
Online ISBN: 978-3-642-37036-6
eBook Packages: Computer ScienceComputer Science (R0)