Verifying Liveness Properties of ML Programs

TL;DR

This paper introduces an efficient algorithm for verifying CTL properties of trees generated by higher-order recursion schemes, enabling the verification of liveness properties in functional programs like OCaml.

Contribution

It extends Kobayashi's intersection type-based model checking technique to higher-order recursion schemes and provides an implementation called THORS for practical verification.

Findings

THORS performs well on small examples

Successfully verifies liveness properties in OCaml programs

Enables checking properties like socket closure and lock holding

Abstract

Higher-order recursion schemes are a higher-order analogue of Boolean Programs; they form a natural class of abstractions for functional programs. We present a new, efficient algorithm for checking CTL properties of the trees generated by higher-order recursion schemes, which is an extension of Kobayashi's intersection type-based model checking technique. We show that an implementation of this algorithm, THORS, performs well on a number of small examples and we demonstrate how it can be used to verify liveness properties of OCaml programs. Example properties include statements such as "all opened sockets are eventually closed" and "the lock is held until the file is closed".