nach oben

Erschienen in:

2017 | OriginalPaper | Buchkapitel

Modular Verification of Higher-Order Functional Programs

verfasst von : Ryosuke Sato, Naoki Kobayashi

Erschienen in: Programming Languages and Systems

Verlag: Springer Berlin Heidelberg

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

Fully automated verification methods for higher-order functional programs have recently been proposed based on higher-order model checking and/or refinement type inference. Most of those methods are, however, whole program analyses, suffering from the scalability problem. To address the problem, we propose a modular method for fully automated verification of higher-order programs. Our method takes a program consisting of multiple top-level functions as an input, and repeatedly applies procedures for (i) guessing refinement intersection types of each function in a counterexample-guided manner, and (ii) checking that each function indeed has the guessed refinement intersection types, until the whole program is proved/disproved to be safe. To avoid the whole program analysis, we introduce the notion of modular counterexamples, and utilize them in (i), and employ Sato et al.’s technique of reducing refinement type checking to assertion checking in (ii). We have implemented the proposed method as an extension to MoCHi, and confirmed its effectiveness through experiments.

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 "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

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

Vorheriges Kapitel Context-Free Session Type Inference

Nächstes Kapitel Commutative Semantics for Probabilistic Programming

Nur mit Berechtigung zugänglich

Mutual recursion can be realized by passing \(f_{i+1},\ldots ,f_n\) as arguments of \(f_i\). For example, \(\mathbf {let}\ \mathbf {rec}\ f_1\;x = C_1[f_1,f_2]\; \mathbf {and}\; f_2\;x=C_2[f_1,f_2]\ \mathbf {in}\ f_2\) can be expressed as \(\mathbf {let}\ \mathbf {rec}\ {f_1\;f_2\;x} = {C_1[f_1\;f_2, f_2]}\ \mathbf {in}\ \mathbf {let}\ \mathbf {rec}\ {f'_2\;x} = {C_2[f_1\;f'_2,f'_2]}\ \mathbf {in}\ f'_2\).

Thus, whether a recursive function is introduced by a top-level function definition or by \(\mathbf {fix}({f}, \lambda {x}.\,{t})\) does not matter for an execution of a program; it matters only for the modular verification method, which treats each top-level function definition as the unit of modular verification.

Here, for the readability of the reduction sequence, we treat let-expressions as primitives and extend the evaluation contexts with \(E \,\,{::}\!\!= \cdots \mid \mathbf {let}\ {x} = {v}\ \mathbf {in}\ E\).

It is actually an extension of straightline programs [9], and deviates from the standard notion of program slices; see Sect. 4.

Berezin, S., Campos, S., Clarke, E.M.: Compositional reasoning in model checking. In: Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol. 1536, pp. 81–102. Springer, Heidelberg (1998). doi:10.1007/3-540-49213-5_4CrossRef

Burch, J., Clarke, E.M., Long, D.: Symbolic model checking with partitioned transition relations. In: Proceedings of the IFIP TC10/WG 10.5 International Conference on Very Large Scale Integration (VLSI 1991), pp. 49–58 (1991)

Campos, S.V.A.: A quantitative approach to the formal verification of real-time systems. Ph.D. thesis, Carnegie Mellon University (1996)

Chaki, S., Gurfinkel, A.: Automated assume-guarantee reasoning for omega-regular systems and specifications. Innov. Syst. Softw. Eng. 7(2), 131–139 (2011)CrossRef

Cobleigh, J.M., Giannakopoulou, D., PĂsĂreanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003). doi:10.1007/3-540-36577-X_24CrossRefMATH

Filliâtre, J.C., Paskevich, A.: Why3 - where programs meet provers. In: Proceedings of the 22nd European Conference on Programming Languages and Systems (ESOP 2013), pp. 125–128 (2013)

Gheorghiu Bobaru, M., Păsăreanu, C.S., Giannakopoulou, D.: Automated assume-guarantee reasoning by abstraction refinement. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 135–148. Springer, Heidelberg (2008). doi:10.1007/978-3-540-70545-1_14CrossRef

Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Program. Lang. Syst. 16(3), 843–871 (1994)CrossRef

Kobayashi, N., Sato, R., Unno, H.: Predicate abstraction and CEGAR for higher-order model checking. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2011), pp. 222–233 (2011)

10.

Kobayashi, N., Tabuchi, N., Unno, H.: Higher-order multi-parameter tree transducers and recursion schemes for program verification. In: Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2010), pp. 495–508 (2010)

11.

Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). doi:10.1007/978-3-642-17511-4_20CrossRefMATH

12.

Matsumoto, Y., Kobayashi, N., Unno, H.: Automata-based abstraction for automated verification of higher-order tree-processing programs. In: Feng, X., Park, S. (eds.) APLAS 2015. LNCS, vol. 9458, pp. 295–312. Springer, Cham (2015). doi:10.1007/978-3-319-26529-2_16CrossRef

13.

Nguyen, P.C., Horn, D.V.: Relatively complete counterexamples for higher-order programs. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015), pp. 446–456. ACM (2015)

14.

Nguyen, P.C., Tobin-Hochstadt, S., Horn, D.V.: Soft contract verification. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP 2014), pp. 139–152 (2014)

15.

Ong, C.H.L., Ramsay, S.J.: Verifying higher-order functional programs with pattern-matching algebraic data types. In: Proceedings of the 38th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2011), pp. 587–598 (2011)

16.

Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2008), pp. 159–169 (2008)

17.

Sato, R., Asada, K., Kobayashi, N.: Refinement type checking via assertion checking. J. Inf. Process. 23(6), 827–834 (2015)

18.

Sato, R., Unno, H., Kobayashi, N.: Towards a scalable software model checker for higher-order programs. In: Proceedings of the ACM SIGPLAN 2013 Workshop on Partial Evaluation and Program Manipulation (PEPM 2013), pp. 53–62. ACM Press (2013)

19.

Swamy, N., Kohlweiss, M., Zinzindohoue, J.K., Zanella-Béguelin, S., HriÅ£cu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.Y., Swamy, N., HriÅ£cu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.Y., Kohlweiss, M., Zinzindohoue, J.K., Zanella-Béguelin, S.: Dependent types and multi-monadic effects in F*. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2016), pp. 256–270 (2016)

20.

Terao, T., Tsukada, T., Kobayashi, N.: Higher-order model checking in direct style. In: Igarashi, A. (ed.) APLAS 2016. LNCS, vol. 10017, pp. 295–313. Springer, Cham (2016). doi:10.1007/978-3-319-47958-3_16CrossRef

21.

Terauchi, T.: Dependent types from counterexamples. In: Proceedings of the 37th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL 2010), pp. 119–130 (2010)

22.

Touati, H., Savoj, H., Lin, B., Brayton, R., Sangiovanni-Vincentelli, A.: Implicit state enumeration of finite state machines using BDD’s. In: 1990 IEEE International Conference on Computer-Aided Design (ICCAD 1990), pp. 130–133 (1990)

23.

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 (PPDP 2009), pp. 277–288 (2009)

24.

Unno, H., Terauchi, T., Kobayashi, N.: Automating relatively complete verification of higher-order functional programs. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013), pp. 75–86 (2013)

25.

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, pp. 269–282 (2014)

26.

Voirol, N., Kneuss, E., Kuncak, V.: Counter-example complete verification for higher-order functions. In: Proceedings of the 6th ACM SIGPLAN Symposium on Scala (Scala 2015), pp. 18–29 (2015)

27.

Weis, P.: Caml examples (2001). http://caml.inria.fr/pub/old_caml_site/Examples/

28.

Xi, H., Pfenning, F.: Dependent types in practical programming. In: Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1999), pp. 214–227 (1999)

29.

Zhu, H., Jagannathan, S.: Compositional and lightweight dependent type inference for ML. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 295–314. Springer, Heidelberg (2013). doi:10.1007/978-3-642-35873-9_19CrossRefMATH

30.

Zhu, H., Nori, A.V., Jagannathan, S.: Learning refinement types. In: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (ICFP 2015), pp. 400–411 (2015)

31.

Zhu, H., Petri, G., Jagannathan, S.: Automatically learning shape specifications. In: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, (PLDI 2016), pp. 491–507 (2016)

Titel: Modular Verification of Higher-Order Functional Programs
verfasst von: Ryosuke Sato
Naoki Kobayashi
Verlag: Springer Berlin Heidelberg
Buch: Programming Languages and Systems
Print ISBN: 978-3-662-54433-4

Electronic ISBN: 978-3-662-54434-1

Copyright-Jahr: 2017
DOI: https://doi.org/10.1007/978-3-662-54434-1_31

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 "Technik"

Springer Professional "Wirtschaft"