Asynchronous Unfolding for Fold/Unfold Transformation of Fixpoint Logic Formula
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.
Wed 11 MayDisplayed time zone: Osaka, Sapporo, Tokyo change
23:10 - 00:00
|Asynchronous Unfolding for Fold/Unfold Transformation of Fixpoint Logic Formula|
|On Transforming Cut- and Quantifier-Free Cyclic Proofs into Rewriting-Induction Proofs|