CTL+FO Verification as Constraint Solving

TL;DR

This paper introduces an automatic verification method for CTL+FO properties, combining temporal and data reasoning through a novel constraint encoding integrated with existing solvers.

Contribution

It presents a new constraint-based approach that explicitly models the interaction of temporal and first-order quantifiers for CTL+FO verification.

Findings

Successfully verifies CTL+FO properties automatically

Integrates with existing solvers for practical applicability

Handles both invariants and ranking functions in verification

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.