@inproceedings{beyene2014ctl,
author = {Beyene, Tewodros A. and Brockschmidt, Marc and Rybalchenko, Andrey},
title = {CTL+FO Verification as Constraint Solving},
booktitle = {Symposium on Model Checking of Software (SPIN)},
year = {2014},
month = {July},
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.},
publisher = {ACM},
url = {http://approjects.co.za/?big=en-us/research/publication/ctlfo-verification-as-constraint-solving/},
edition = {Symposium on Model Checking of Software (SPIN)},
}