Modular verification of higher-order functional programs

Ryosuke Sato, Naoki Kobayashi

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationProgramming Languages and Systems - 26th European Symposium on Programming, ESOP 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings
EditorsHongseok Yang
PublisherSpringer Verlag
Pages831-854
Number of pages24
ISBN (Print)9783662544334
DOIs
Publication statusPublished - Jan 1 2017
Externally publishedYes
Event26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017 - Uppsala, Sweden
Duration: Apr 22 2017Apr 29 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10201 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other26th European Symposium on Programming, ESOP 2017 held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017
CountrySweden
City Uppsala
Period4/22/174/29/17

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Modular verification of higher-order functional programs'. Together they form a unique fingerprint.

  • Cite this

    Sato, R., & Kobayashi, N. (2017). Modular verification of higher-order functional programs. In H. Yang (Ed.), Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017 Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Proceedings (pp. 831-854). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10201 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-662-54434-1_31