  A program invariant is a property that holds for every execution of the
program. Recent work suggest to infer likely-only invariants, via dynamic
analysis. A likely invariant is a property that holds for some executions but
is not guaranteed to hold for all executions. In this paper, we present work in
progress addressing the challenging problem of automatically verifying that
likely invariants are actual invariants. We propose a constraint-based
reasoning approach that is able, unlike other approaches, to both prove or
disprove likely invariants. In the latter case, our approach provides
counter-examples. We illustrate the approach on a motivating example where
automatically generated likely invariants are verified.
