nach oben

Journal of Automated Reasoning

Erschienen in:

01.08.2020

ICE-Based Refinement Type Discovery for Higher-Order Functional Programs

verfasst von: Adrien Champion, Tomoya Chiba, Naoki Kobayashi, Ryosuke Sato

Erschienen in: Journal of Automated Reasoning | Ausgabe 7/2020

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We propose a method for automatically finding refinement types of higher-order function programs. Our method is an extension of the Ice framework of Garg et al. for finding invariants. In addition to the usual positive and negative samples in machine learning, their Ice framework uses implication constraints, which consist of pairs (x, y) such that if x satisfies an invariant, so does y. From these constraints, Ice infers inductive invariants effectively. We observe that the implication constraints in the original Ice framework are not suitable for finding invariants of recursive functions with multiple function calls. We thus generalize the implication constraints to those of the form \((\{x_1,\dots ,x_k\}, y)\), which means that if all of \(x_1,\dots ,x_k\) satisfy an invariant, so does y. We extend their algorithms for inferring likely invariants from samples, verifying the inferred invariants, and generating new samples. We have implemented our method and confirmed its effectiveness through experiments.

Vorheriger Artikel Chain Reduction for Binary and Zero-Suppressed Decision Diagrams

Nächster Artikel Fine-Grained Complexity of Safety Verification

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Nur mit Berechtigung zugänglich

We discuss how to extract these verification conditions in Sect. 2.

Hosted at https://github.com/hopv/r_type and https://github.com/hopv/hoice.

For more details, see https://www.rust-lang.org/en-US/.

The revision of Z3 in all the experiments is the latest at the time of writing: 5bc4c98 .

Hosted at https://github.com/hopv/benchmarks.

This is consistent with the OCaml results: 151 sat results, 9 unsat from programs RType cannot verify, and 2 unsat from unsafe programs.

Since the totality of \(f_{\rho }\) is undecidable in general, this check is necessarily heuristic. The check is omitted in the current implementation reported in Sect. 5.3. The implementation is thus unsound, although the unsoundness did not show up in the reported experiments.

Such as the use of conditional “check-sat” in the check https://rise4fun.com/Z3/cXot4.

Available at https://fmlab.unich.it/iclp2018.

This evaluation uses HoIce 1.8.1.

https://github.com/Z3Prover/z3/releases/tag/z3-4.7.1.

Arora, S., Barak, B.: Computational Complexity—A Modern Approach. Cambridge University Press, Cambridge (2009)CrossRef

Barrett, C.W., Sebastiani, R., Seshia, S.A., Tinelli, C.: In: Biere, A., Heule, M., Van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 825–885. IOS Press, Amsterdam (2009). https://doi.org/10.3233/978-1-58603-929-5-825

Beyer, D.: Competition on software verification—(SV-COMP). In: Flanagan, C., König, B. (eds.) Tools and Algorithms for the Construction and Analysis of Systems—18th International Conference, TACAS 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24–April 1, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7214, pp. 504–524. Springer, Berlin (2012). https://doi.org/10.1007/978-3-642-28756-5_38

Bjørner, N., Gurfinkel, A., McMillan, K.L., 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—Essays Dedicated to Yuri Gurevich on the Occasion of His 75th Birthday, Lecture Notes in Computer Science, vol. 9300, pp. 24–51. Springer, Berlin (2015). https://doi.org/10.1007/978-3-319-23534-9_2

Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D.A. (eds.) Verification, Model Checking, and Abstract Interpretation—12th International Conference, VMCAI 2011, Austin, TX, USA, January 23–25, 2011. Proceedings, Lecture Notes in Computer Science, vol. 6538, pp. 70–87. Springer, Berlin (2011). https://doi.org/10.1007/978-3-642-18275-4_7

Champion, A., Chiba, T., Kobayashi, N., Sato, R.: Ice-based refinement type discovery for higher-order functional programs. In: Tools and Algorithms for the Construction and Analysis of Systems—24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018, Proceedings, Part I, pp. 365–384 (2018). https://doi.org/10.1007/978-3-319-89960-2_20

Champion, A., Kobayashi, N., Sato, R.: Hoice: an ice-based non-linear horn clause solver. In: Ryu, S. (ed.) Programming Languages and Systems—16th Asian Symposium, APLAS 2018, Wellington, New Zealand, December 2–6, 2018, Proceedings, Lecture Notes in Computer Science, vol. 11275, pp. 146–156. Springer, Berlin (2018). https://doi.org/10.1007/978-3-030-02768-1_8

Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The Kind 2 model checker. In: Proceedings of CAV 2016, LNCS, vol. 9780, pp. 510–517. Springer, Berlin (2016). https://doi.org/10.1007/978-3-319-41540-6_29

De Angelis, E., Fioravanti, F., Pettorossi, A., Proietti, M.: Solving horn clauses on inductive data types without induction. TPLP 18(3–4), 452–469 (2018). https://doi.org/10.1017/S1471068418000157MathSciNetCrossRefMATH

10.

de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Proceedings of TACAS 2008, LNCS, vol. 4963, pp. 337–340. Springer, Berlin (2008). https://doi.org/10.1007/978-3-540-78800-3_24

11.

Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Solving constrained horn clauses using syntax and data. In: Bjørner, N., Gurfinkel, A. (eds.) 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30–November 2, 2018, pp. 1–9. IEEE (2018). https://doi.org/10.23919/FMCAD.2018.8603011

12.

Freeman, T.S., Pfenning, F.: Refinement types for ML. In: Proceedings of PLDI’91, pp. 268–277. ACM (1991). https://doi.org/10.1145/113445.113468

13.

Garg, P., Löding, C., Madhusudan, P., Neider, D.: ICE: a robust framework for learning invariants. In: Proceedings of CAV 2014, LNCS, vol. 8559, pp. 69–87. Springer, Berlin (2014). https://doi.org/10.1007/978-3-319-08867-9_5

14.

Garg, P., Neider, D., Madhusudan, P., Roth, D.: Learning invariants using decision trees and implication counterexamples. In: Proceedings of POPL 2016, pp. 499–512. ACM (2016). https://doi.org/10.1145/2837614.2837664

15.

Hoder, K., Bjørner, N.: Generalized property directed reachability. In: Cimatti, A., Sebastiani, R. (eds.) Theory and Applications of Satisfiability Testing—SAT 2012—15th International Conference, Trento, Italy, June 17–20, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7317, pp. 157–171. Springer, Berlin (2012). https://doi.org/10.1007/978-3-642-31612-8_13

16.

Hojjat, H., Konecný, F., Garnier, F., Iosif, R., Kuncak, V., Rümmer, P.: A verification toolkit for numerical transition systems—tool paper. In: Giannakopoulou, D., Méry, D. (eds.) FM 2012: Formal Methods—18th International Symposium, Paris, France, August 27–31, 2012. Proceedings, Lecture Notes in Computer Science, vol. 7436, pp. 247–251. Springer, Berlin (2012). https://doi.org/10.1007/978-3-642-32759-9_21

17.

Jhala, R., Majumdar, R., Rybalchenko, A.: HMC: verifying functional programs using abstract interpreters. In: Proceedings of CAV 2011, LNCS, vol. 6806, pp. 470–485. Springer, Berlin (2011). https://doi.org/10.1007/978-3-642-22110-1_38

18.

Komuravelli, A., Gurfinkel, A., Chaki, S.: SMT-based model checking for recursive programs. Form. Methods Syst. Des. 48(3), 175–205 (2016). https://doi.org/10.1007/s10703-016-0249-4CrossRefMATH

19.

Kovács, L., Voronkov, A.: Finding loop invariants for programs over arrays using a theorem prover. In: Proceedings of FASE 2009, LNCS, vol. 5503, pp. 470–485. Springer, Berlin (2009). https://doi.org/10.1007/978-3-642-00593-0_33

20.

Kuwahara, T., Terauchi, T., Unno, H., Kobayashi, N.: Automatic termination verification for higher-order functional programs. In: Proceedings of ESOP 2014, LNCS, vol. 8410, pp. 392–411. Springer, Berlin (2014)

21.

McMillan, K., Rybalchenko, A.: Computing relational fixed points using interpolation. Technical report (2013)

22.

Minsky, Y.: Ocaml for the masses. ACM Queue 9(9), 43 (2011). https://doi.org/10.1145/2030256.2038036CrossRef

23.

Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Berlin (1999). https://doi.org/10.1007/978-3-662-03811-6CrossRefMATH

24.

Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: Proceedings of PLDI 2008, pp. 159–169. ACM (2008). https://doi.org/10.1145/1375581.1375602

25.

Sato, R., Iwayama, N., Kobayashi, N.: Combining higher-order model checking with refinement type inference. In: Proceedings of the 2019 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, pp. 47–53. ACM (2019)

26.

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). https://doi.org/10.1145/2426890.2426900

27.

Sharma, R., Aiken, A.: From invariant checking to invariant inference using randomized search. In: Proceedings of CAV 2014, LNCS, vol. 8559, pp. 88–105. Springer, Berlin (2014). https://doi.org/10.1007/978-3-319-08867-9_6

28.

Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Liang, P., Nori, A.V.: A data driven approach for algebraic loop invariants. In: Proceedings of ESOP 2013, LNCS, vol. 7792, pp. 574–592. Springer, Berlin (2013). https://doi.org/10.1007/978-3-642-37036-6_31

29.

Sharma, R., Gupta, S., Hariharan, B., Aiken, A., Nori, A.V.: Verification as learning geometric concepts. In: Proceedings of SAS 2013, LNCS, vol. 7935, pp. 388–411. Springer, Berlin (2013). https://doi.org/10.1007/978-3-642-38856-9_21

30.

Terauchi, T.: Dependent types from counterexamples. In: Proceedings of POPL 2010, pp. 119–130. ACM (2010). https://doi.org/10.1145/1706299.1706315

31.

Unno, H., Kobayashi, N.: Dependent type inference with interpolants. In: Proceedings of PPDP 2009, pp. 277–288. ACM (2009). https://doi.org/10.1145/1599410.1599445

32.

Unno, H., Terauchi, T., Kobayashi, N.: Automating relatively complete verification of higher-order functional programs. In: Proceedings of POPL ’13, pp. 75–86. ACM (2013). https://doi.org/10.1145/2429069.2429081

33.

Xi, H., Pfenning, F.: Dependent types in practical programming. In: Proceedings of POPL ’99, pp. 214–227. ACM (1999). https://doi.org/10.1145/292540.292560

34.

Zhu, H., Jagannathan, S.: Compositional and lightweight dependent type inference for ML. In: Proceedings of VMCAI 2013, LNCS, vol. 7737, pp. 295–314. Springer, Berlin (2013). https://doi.org/10.1007/978-3-642-35873-9_19

35.

Zhu, H., Magill, S., Jagannathan, S.: A data-driven CHC solver. In: Foster, J.S., Grossman, D. (eds.) Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2018, Philadelphia, PA, USA, June 18–22, 2018, pp. 707–721. ACM (2018). https://doi.org/10.1145/3192366.3192416

36.

Zhu, H., Nori, A.V., Jagannathan, S.: Dependent array type inference from tests. In: Proceedings of VMCAI 2015, LNCS, vol. 8931, pp. 412–430. Springer, Berlin (2015). https://doi.org/10.1007/978-3-662-46081-8_23

37.

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

38.

Zhu, H., Petri, G., Jagannathan, S.: Automatically learning shape specifications. In: Proceedings of PLDI 2016, pp. 491–507. ACM (2016). https://doi.org/10.1145/2908080.2908125

Titel: ICE-Based Refinement Type Discovery for Higher-Order Functional Programs
verfasst von: Adrien Champion
Tomoya Chiba
Naoki Kobayashi
Ryosuke Sato
Publikationsdatum: 01.08.2020
Verlag: Springer Netherlands
Erschienen in: Journal of Automated Reasoning / Ausgabe 7/2020
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI: https://doi.org/10.1007/s10817-020-09571-y

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Wirtschaft"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 7/2020

Proof-Producing Synthesis of CakeML from Monadic HOL Functions

Selected and Extended Papers from TACAS 2018: Preface

Synthesizing Precise and Useful Commutativity Conditions

Preface: Special Issue of Selected Extended Papers from IJCAR 2018

A Learning-Based Approach to Synthesizing Invariants for Incomplete Verification Engines

Fine-Grained Complexity of Safety Verification