Abstract
Refinement types have recently been applied to program verification, where program verification problems are reduced to type checking or inference problems. For fully automated verification of programs with recursive data structures, however, previous refinement type systems have not been satisfactory: they were not expressive enough to state complex properties of data, such as the length and monotonicity of a list, or required explicit declarations of precise types by users. To address the problem above, we introduce parameterized recursive refinement types (PRRT), which are recursive datatypes parameterized by integer parameters and refinement predicates; those parameters can be used to express various properties of data structures such as the length/sortedness of a list and the depth/size of a tree. We propose an automated type inference algorithm for PRRT, by a reduction to the satisfiability problem for CHCs (Constrained Horn Clauses). We have implemented a prototype verification tool and evaluated the effectiveness of the proposed method through experiments.
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
Similar content being viewed by others
Notes
- 1.
The restriction to first-order programs is just for the sake of simplicity; our refinement type system can be easily extended for higher-order functions in a standard manner.
- 2.
Actually, \(\mathtt {gen\_tree}(n)\) will not terminate if \(n<0\), but that does not concern us here since we are interested in only the safety property.
- 3.
Since the CHC satisfiability problem is undecidable in general, there is no complete CHC solver.
- 4.
The work of Tondwalkar et al. [17] does not suffer from this problem, since the existential CHCs obtained in their work is acyclic, while the existential CHCs generated from our inference problem would be cyclic.
References
Bjørner, N., Gurfinkel, A., McMillan, K., Rybalchenko, A.: Horn clause solvers for program verification. In: Beklemishev, L.D., Blass, A., Dershowitz, N., Finkbeiner, B., Schulte, W. (eds.) Fields of Logic and Computation II. LNCS, vol. 9300, pp. 24–51. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23534-9_2
Champion, A., Chiba, T., Kobayashi, N., Sato, R.: ICE-based refinement type discovery for higher-order functional programs. J. Autom. Reason. 64(7), 1393–1418 (2020). https://doi.org/10.1007/s10817-020-09571-y
Hashimoto, K., Unno, H.: Refinement type inference via horn constraint optimization. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 199–216. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48288-9_12
Hojjat, H., Rümmer, P.: The ELDARICA horn solver. In: 2018 Formal Methods in Computer Aided Design (FMCAD), pp. 1–7 (2018)
Kawaguchi, M., Rondon, P.M., Jhala, R.: Type-based data structure verification. In: Hind, M., Diwan, A. (eds.) Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009, Dublin, Ireland, June 15–21, 2009, pp. 304–315. ACM (2009). https://doi.org/10.1145/1542476.1542510
Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: PLDI 2011, pp. 222–233. ACM Press (2011)
Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Formal Methods Syst. Design 48(3), 175–205 (2016). https://doi.org/10.1007/s10703-016-0249-4
Kuwahara, T., Terauchi, T., Unno, H., Kobayashi, N.: Automatic termination verification for higher-order functional programs. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 392–411. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54833-8_21
Lee, C.S., Jones, N.D., Ben-Amram, A.M.: The size-change principle for program termination. In: Hankin, C., Schmidt, D. (eds.) Conference Record of POPL 2001: The 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, London, UK, January 17–19, 2001, pp. 81–92. ACM (2001). https://doi.org/10.1145/360204.360210
Lev-Ami, T., Sagiv, M.: TVLA: a system for implementing static analyses. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol. 1824, pp. 280–301. Springer, Heidelberg (2000). https://doi.org/10.1007/978-3-540-45099-3_15
Manevich, R., Yahav, E., Ramalingam, G., Sagiv, M.: Predicate abstraction and canonical abstraction for singly-linked lists. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 181–198. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30579-8_13
de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24
Mukai, R., Kobayashi, N., Sato, R.: Parameterized recursive refinement types for automated program verification (2022), a longer version of this paper, available from http://www.kb.is.s.u-tokyo.ac.jp/~koba/
Ong, C.H.L., Ramsay, S.: Verifying higher-order programs with pattern-matching algebraic data types. In: Proceedings of POPL, pp. 587–598. ACM Press (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 Press (2013)
Tondwalkar, A., Kolosick, M., Jhala, R.: Refinements of futures past: Higher-order specification with implicit refinement types. In: Møller, A., Sridharan, M. (eds.) 35th European Conference on Object-Oriented Programming, ECOOP 2021, July 11–17, 2021, Aarhus, Denmark (Virtual Conference). LIPIcs, vol. 194, pp. 18:1–18:29. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021). https://doi.org/10.4230/LIPIcs.ECOOP.2021.18
Unno, H., Kobayashi, N.: On-Demand refinement of dependent types. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol. 4989, pp. 81–96. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78969-7_8
Unno, H., Kobayashi, N.: Dependent type inference with interpolants. In: Proceedings of the 11th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, September 7–9, 2009, Coimbra, Portugal, pp. 277–288. ACM (2009)
Unno, H., Terauchi, T., Kobayashi, N.: Automating relatively complete verification of higher-order functional programs. In: The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, pp. 75–86. ACM (2013)
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). https://doi.org/10.1007/978-3-642-37036-6_13
Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Jones, S.L.P.: Refinement types for haskell. In: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming, Gothenburg, Sweden, September 1–3, 2014, pp. 269–282. ACM (2014)
**, H., Pfenning, F.: Eliminating array bound checking through dependent types. In: Davidson, J.W., Cooper, K.D., Berman, A.M. (eds.) Proceedings of the ACM SIGPLAN ’98 Conference on Programming Language Design and Implementation (PLDI), Montreal, Canada, June 17–19, 1998, pp. 249–257. ACM (1998). https://doi.org/10.1145/277650.277732
**, H., Pfenning, F.: Dependent types in practical programming. In: Proceedings of POPL, pp. 214–227 (1999)
Zhu, H., Nori, A.V., Jagannathan, S.: Learning refinement types. In: Proceedings of ICFP 2015, pp. 400–411. ACM (2015). https://doi.org/10.1145/2784731.2784766
Acknowledgments
We would like to thank anonymous referees for useful comments. This work was supported by JSPS KAKENHI Grant Number JP20H05703.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Appendices
Appendix
A Details of Experiments
Table 2 presents the experimental results for each backend CHC solver. The columns “n” and “Time” for each solver have the same meaning as Sect. 5.2.
As examples of the benchmark programs, Listings 1.1 and 1.2 respectively show the programs named “list-sum” and “bst-size” in Sect. 5.2.
Rights and permissions
Copyright information
© 2022 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Mukai, R., Kobayashi, N., Sato, R. (2022). Parameterized Recursive Refinement Types for Automated Program Verification. In: Singh, G., Urban, C. (eds) Static Analysis. SAS 2022. Lecture Notes in Computer Science, vol 13790. Springer, Cham. https://doi.org/10.1007/978-3-031-22308-2_18
Download citation
DOI: https://doi.org/10.1007/978-3-031-22308-2_18
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-22307-5
Online ISBN: 978-3-031-22308-2
eBook Packages: Computer ScienceComputer Science (R0)