CTL+FO Verification as Constraint Solving

Tewodros A. Beyene, Marc Brockschmidt, and Andrey Rybalchenko

Abstract

Expressing program correctness often requires relating program data throughout (different branches of) an execution. Such properties can be represented using CTL+FO, a logic

that allows mixing temporal and first-order quantification. Verifying that a program satisfies a CTL+FO property is a challenging problem that requires both temporal and data reasoning. Temporal quantifiers require discovery of invariants and ranking functions, while first-order quantifiers demand instantiation techniques. In this paper, we present a constraint-based method for proving CTL+FO properties automatically. Our method makes the interplay between the temporal and first-order quantification explicit in a constraint encoding that combines recursion and existential quantification. By integrating this constraint encoding with an off-the-shelf solver we obtain an automatic verifier for CTL+FO.

Details

Publication typeInproceedings
Published inSPIN
PublisherACM
> Publications > CTL+FO Verification as Constraint Solving