Predicate abstraction and CEGAR for disproving termination of higher-order functional programs

Abstract. We propose an automated method for disproving termina-tion of higher-order functional programs. Our method combines higher-order model checking with predicate abstraction and CEGAR. Our pred-icate 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 non-terminating. 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 con-firmed the effectiveness of the proposed approach through experiments.