Mode-based Reduction from Validity Checking of Fixpoint Logic Formulas to Test-Friendly Reachability Problem

A logical approach to automated program verification has been drawing attention recently, where various program verification problems are transformed into formulas of fixpoint logics such as CHC and νHFL(Z), so that a given program satisfies a property just if the corresponding fixpoint formula is valid. In this paper, we show a kind of converse transformation, converting fixpoint logic formulas to programs so that a formula is valid just if the resulting program never evaluates to an (error) value. This, together with the aforementioned transformation from programs to formulas, allows us to go back and forth between logical formulas and programs. In particular, our transformation enables us to use random testing to disprove a given formula, implying that the original program does not satisfy the specified property. As the programs generated by a naive transformation are not suitable for random testing, we employ mode analysis to generate more test-friendly programs. We have implemented the mode-guided transformation and confirmed its effectiveness through experiments. © The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd. 2025.