Abstract
Higher-order model checking has been recently applied to automated verification of higher-order functional programs, but there have been difficulties in dealing with algebraic data types such as lists and trees. To remedy the problem, we propose an automata-based abstraction of tree data, and a counterexample-guided refinement of the abstraction. By combining them with higher-order model checking, we can construct a fully-automated verification tool for higher-order, tree-processing functional programs. We formalize the verification method, prove its correctness, and report experimental results.
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
References
Asada, K., Sato, R., Kobayashi, N.: Verifying relational properties of functional programs by first-order refinement. In: Proceedings of PEPM 2015, pp. 61–72 (2015)
Blumensath, A., Grädel, E.: Automatic structures. In: Proceedings of LICS 2000, pp. 51–62 (2000)
Broadbent, C.H., Kobayashi, N.: Saturation-based model checking of higher-order recursion schemes. In: Proceedings of CSL 2013. LIPIcs, vol. 23, pp. 129–148 (2013)
Comon, H., et al.: Tree automata techniques and applications (2007). http://www.grappa.univ-lille3.fr/tata
de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Genet, T.: Towards static analysis of functional programs using tree automata completion. In: Escobar, S. (ed.) WRLA 2014. LNCS, vol. 8663, pp. 147–161. Springer, Heidelberg (2014)
Kawaguchi, M., Rondon, P., Jhala, R.: Type-based data structure verification. In: Proceedings of PLDI 2009, pp. 304–315. ACM (2009)
Kobayashi, N.: Model-checking higher-order functions. In: Proceedings of PPDP 2009. pp. 25–36 (2009)
Kobayashi, N.: Model checking higher-order programs. J. ACM 60(3), 20:1–20:62 (2013)
Kobayashi, N., Li, X.: Automata-based abstraction refinement for \(\mu \)HORS model checking. In: Proceedings of LICS 2015 (2015)
Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and cegar for higher-order model checking. In: Proceedings of PLDI 2011, pp. 222–233 (2011)
Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. In: Proceedings of POPL 2010, pp. 495–508. ACM (2010)
Matsumoto, Y., Kobayashi, N., Unno, H.: Automata-based abstraction for automated verification of higher-order tree-processing programs (2015). an extended version, available from the second author’s web page
Matsumoto, Y., Kobayashi, N., Unno, H.: Counterexample finding and abstraction refinement for automated verification of higher-order transducers. Comput. Softw. 31(1), 161–178 (2015). (in Japanese)
Ong, C.-H.L.: On model-checking trees generated by higher-order recursion schemes. In: Proceedings of LICS 2006, pp. 81–90. IEEE Computer Society (2006)
Ong, C.-H.L., Ramsay, S.J.: Verifying higher-order functional programs with pattern-matching algebraic data types. In: Proceedings of POPL 2011, pp. 587–598. ACM (2011)
Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: PLDI 2008, pp. 159–169 (2008)
Sato, R., Unno, H., Kobayashi, N.: Towards a scalable software model checker for higher-order programs. In: Proceedings of PEPM 2013, pp. 53–62. ACM (2013)
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)
Vazou, N., Rondon, P.M., Jhala, R.: Abstract refinement types. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 209–228. Springer, Heidelberg (2013)
Acknowledgments
We thank anonymous reviewers for useful comments. This work was partially supported by JSPS Kakenhi 15H05706, 23220001, and 25730035.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Matsumoto, Y., Kobayashi, N., Unno, H. (2015). Automata-Based Abstraction for Automated Verification of Higher-Order Tree-Processing Programs. In: Feng, X., Park, S. (eds) Programming Languages and Systems. APLAS 2015. Lecture Notes in Computer Science(), vol 9458. Springer, Cham. https://doi.org/10.1007/978-3-319-26529-2_16
Download citation
DOI: https://doi.org/10.1007/978-3-319-26529-2_16
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-26528-5
Online ISBN: 978-3-319-26529-2
eBook Packages: Computer ScienceComputer Science (R0)