Asynchronous unfold/fold transformation for fixpoint logic

Various program verification problems for functional programs can be reduced to the validity checking problem for formulas of a fixpoint logic. Recently, Kobayashi et al. have shown that the unfold/fold transformation originally developed for logic programming can be extended and applied to prove the validity of fixpoint logic formulas. In the present paper, we refine their unfold/fold transformation, so that each predicate can be unfolded a different number of times in an asynchronous manner. Inspired by the work of Lee et al. on size change termination, we use a variant of size change graphs to find an appropriate number of unfoldings of each predicate. We have implemented an unfold/fold transformation tool based on the proposed method, and evaluated its effectiveness. (c) 2023 Elsevier B.V. All rights reserved.