On Higher-Order Reachability Games vs May Reachability

TL;DR

This paper explores the relationship between reachability games and may-reachability in higher-order programs, establishing reductions between them using higher-order fixpoint logic to enhance verification techniques.

Contribution

It introduces formal reductions between reachability games and may-reachability for higher-order programs, advancing the theoretical understanding and verification methods.

Findings

Reachability games for order-n programs reduce to may-reachability for order-(n+1) programs.

Reductions are formalized and proven correct using higher-order fixpoint logic.

Applications to higher-order program verification are discussed.

Abstract

We consider the reachability problem for higher-order functional programs and study the relationship between reachability games (i.e., the reachability problem for programs with angelic and demonic nondeterminism) and may-reachability (i.e., the reachability problem for programs with only angelic nondeterminism). We show that reachability games for order-n programs can be reduced to may-reachability for order-(n+1) programs, and vice versa. We formalize the reductions by using higher-order fixpoint logic and prove their correctness. We also discuss applications of the reductions to higher-order program verification.