Predicate abstraction and CEGAR for disproving termination of Higher-Order functional programs

Takuya Kuwahara, Ryosuke Sato, Hiroshi Unno, Naoki Kobayashi

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

13 Citations (Scopus)

Abstract

We propose an automated method for disproving termination of higher-order functional programs. Our method combines higherorder model checking with predicate abstraction and CEGAR. Our predicate abstraction is novel in that it computes a mixture of under- and overapproximations. For non-determinism of a source program (such as random number generation), we apply underapproximation to generate a subset of the actual branches, and check that some of the branches in the abstract program is non-terminating. For operations on infinite data domains (such as integers), we apply overapproximation to generate a superset of the actual branches, and check that every branch is nonterminating. Thus, disproving non-termination reduces to the problem of checking a certain branching property of the abstract program, which can be solved by higher-order model checking. We have implemented a prototype non-termination prover based on our method and have confirmed the effectiveness of the proposed approach through experiments.

Original languageEnglish
Title of host publicationComputer Aided Verification - 27th International Conference, CAV 2015, Proceedings
EditorsCorina S. Păsăreanu, Daniel Kroening
PublisherSpringer Verlag
Pages287-303
Number of pages17
ISBN (Print)9783319216676
DOIs
Publication statusPublished - 2015
Event27th International Conference on Computer Aided Verification, CAV 2015 - San Francisco, United States
Duration: Jul 18 2015Jul 24 2015

Publication series

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

Other

Other27th International Conference on Computer Aided Verification, CAV 2015
CountryUnited States
CitySan Francisco
Period7/18/157/24/15

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Predicate abstraction and CEGAR for disproving termination of Higher-Order functional programs'. Together they form a unique fingerprint.

Cite this