Skip to main content
SpringerLink
Log in

Refinement Type Inference via Horn Constraint Optimization

  • Conference paper
  • First Online:
Static Analysis (SAS 2015)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9291))

Included in the following conference series:

Abstract

We propose a novel method for inferring refinement types of higher-order functional programs. The main advantage of the proposed method is that it can infer maximally preferred (i.e., Pareto optimal) refinement types with respect to a user-specified preference order. The flexible optimization of refinement types enabled by the proposed method paves the way for interesting applications, such as inferring most-general characterization of inputs for which a given program satisfies (or violates) a given safety (or termination) property. Our method reduces such a type optimization problem to a Horn constraint optimization problem by using a new refinement type system that can flexibly reason about non-determinism in programs. Our method then solves the constraint optimization problem by repeatedly improving a current solution until convergence via template-based invariant generation. We have implemented a prototype inference system based on our method, and obtained promising results in preliminary experiments.

This work was supported by Kakenhi 25730035, 23220001, 15H05706, and 25280020.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    Here, we use quantifier-free linear arithmetic as the underlying theory and consider only atomic predicates for P and Q.

  2. 2.

    If \(\sqsubset \) were partial, the relation \(\prec _{(\rho ,\sqsubset )}\) defined shortly would not be a strict partial order. Our implementation described in Sect. 7 uses topological sort to obtain a strict total order \(\sqsubset \) from a user-specified partial one.

  3. 3.

    Here, minimality is with respect to the number of recursive calls within the path.

  4. 4.

    The presented code here is thus specialized to solve \(\varTheta _{ atom }\)-restricted Horn constraint optimization problems. To solve \(\varTheta \)-restricted optimization problems for other \(\varTheta \), we need here to generate templates that conform to the shape of substitutions in \(\varTheta \) instead. Our implementation in Sect. 7 iteratively increases the template size.

  5. 5.

    Note here that even though no assignment is found, \(\mathcal {H}\) may have a \(\varTheta _{ atom }\)-restricted solution because Farkas’ lemma is not complete for QFLIA formulas [3, 7] and Skolemization of \(\exists \widetilde{c}.\forall \widetilde{x}.\exists \widetilde{y}.\phi \) into \(\exists \widetilde{c},\widetilde{z}.\forall \widetilde{x}.\phi '\) here assumes that \(\widetilde{y}\) are expressed as linear expressions over \(\widetilde{x}\) [1, 11, 19].

References

  1. Beyene, T.A., Popeea, C., Rybalchenko, A.: Solving existentially quantified horn clauses. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 869–882. Springer, Heidelberg (2013)

    Google Scholar 

  2. Chen, H.-Y., Cook, B., Fuhs, C., Nimkar, K., O’Hearn, P.: Proving nontermination via safety. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 156–171. Springer, Heidelberg (2014)

    Google Scholar 

  3. Colón, M.A., Sankaranarayanan, S., Sipma, H.B.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 420–432. Springer, Heidelberg (2003)

    Google Scholar 

  4. Emmes, F., Enger, T., Giesl, J.: Proving non-looping non-termination automatically. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS, vol. 7364, pp. 225–240. Springer, Heidelberg (2012)

    Google Scholar 

  5. Freeman, T., Pfenning, F.: Refinement types for ML. In: PLDI 1991, pp. 268–277. ACM (1991)

    Google Scholar 

  6. Gulwani, S., Mehra, K.K., Chilimbi, T.: SPEED: Precise and efficient static estimation of program computational complexity. In: POPL 2009, pp. 127–139. ACM (2009)

    Google Scholar 

  7. Gulwani, S., Srivastava,S., Venkatesan, R.: Program analysis as constraint solving. In: PLDI 2008, pp. 281–292. ACM (2008)

    Google Scholar 

  8. Hashimoto, K. Unno, H.: Refinement type inference via horn constraint optimization. An extended version (2015). http://www.cs.tsukuba.ac.jp/~uhiro/

  9. Jhala, R., Majumdar, R., Rybalchenko, A.: HMC: verifying functional programs using abstract interpreters. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 470–485. Springer, Heidelberg (2011)

    Google Scholar 

  10. Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: PLDI 2011, pp. 222–233. ACM (2011)

    Google Scholar 

  11. Kuwahara, T., Sato, R., Unno, H., Kobayashi, N.: Predicate abstraction and CEGAR for disproving termination of higher-order functional programs. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 287–303. Springer, Heidelberg (2015)

    Google Scholar 

  12. Kuwahara, T., Terauchi, T., Unno, H., Kobayashi, N.: Automatic termination verification for higher-order functional programs. In: Shao, Z. (ed.) ESOP 2014 (ETAPS). LNCS, vol. 8410, pp. 392–411. Springer, Heidelberg (2014)

    Google Scholar 

  13. Larraz, D., Nimkar, K., Oliveras, A., Rodríguez-Carbonell, E., Rubio, A.: Proving non-termination using max-SMT. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 779–796. Springer, Heidelberg (2014)

    Google Scholar 

  14. Nieuwenhuis, R., Oliveras, A.: On SAT modulo theories and optimization problems. In: Biere, A., Gomes, C.P. (eds.) SAT 2006. LNCS, vol. 4121, pp. 156–169. Springer, Heidelberg (2006)

    Google Scholar 

  15. Rondon, P., Kawaguchi, M., Jhala, R.: Liquid types. In: PLDI 2008, pp. 159–169. ACM (2008)

    Google Scholar 

  16. Terauchi, T.: Dependent types from counterexamples. In: POPL 2010, pp. 119–130. ACM (2010)

    Google Scholar 

  17. 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)

    Google Scholar 

  18. Unno, H., Kobayashi, N.: Dependent type inference with interpolants. In: PPDP 2009, pp. 277–288. ACM (2009)

    Google Scholar 

  19. Unno, H., Terauchi,T., Kobayashi, N.: Automating relatively complete verification of higher-order functional programs. In: POPL 2013, pp. 75–86. ACM (2013)

    Google Scholar 

  20. Xi, H., Pfenning, F.: Dependent types in practical programming. In: POPL 1999, pp. 214–227. ACM (1999)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Tsukuba, Tsukuba, Japan

    Kodai Hashimoto & Hiroshi Unno

Authors
  1. Kodai Hashimoto
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hiroshi Unno
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kodai Hashimoto .

Editor information

Editors and Affiliations

  1. Université Rennes 1, Rennes, France

    Sandrine Blazy

  2. Inria, Rennes, France

    Thomas Jensen

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Hashimoto, K., Unno, H. (2015). Refinement Type Inference via Horn Constraint Optimization. In: Blazy, S., Jensen, T. (eds) Static Analysis. SAS 2015. Lecture Notes in Computer Science(), vol 9291. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48288-9_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-48288-9_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-48287-2

  • Online ISBN: 978-3-662-48288-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation