To refer to this page use:
|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.|
|Citation:||Kobayashi, Naoki, Grigory Fedyukovich, and Aarti Gupta. "Fold/Unfold Transformations for Fixpoint Logic." In International Conference on Tools and Algorithms for the Construction and Analysis of Systems (2020): pp. 195-214. doi:10.1007/978-3-030-45237-7_12|
|Pages:||195 - 214|
|Type of Material:||Conference Article|
|Journal/Proceeding Title:||International Conference on Tools and Algorithms for the Construction and Analysis of Systems|
|Version:||Final published version. This is an open access article.|
Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.