Fold/Unfold Transformations for Fixpoint Logic
Naoki Kobayashi, Grigory Fedyukovich, Aarti Gupta · Lecture notes in computer science · 2020
Abstract Fixpoint logics have recently been drawing attention as common foundations for automated program verification. We formalize fold/unfold transformations for fixpoint logic formulas and show how they can be used to enhance a recent fixpoint-logic approach to automated program verification, including automated verification of relational and temporal properties. We have implemented the transformations in a tool and confirmed its effectiveness through experiments.