Static verification traditionally produces yes/no answers. It either
provides a proof that a piece of code meets a property, or a
counterexample showing that the property can be violated. Hence, the
progress of static verification is hard to measure. Unlike in testing,
where coverage metrics can be used to track progress, static
verification does not provide any intermediate result until the proof
of correctness can be computed. This is in particular problematic
because of the inevitable incompleteness of static verifiers.

To overcome this, we propose a gradual verification approach,
GraVy. For a given piece of Java code, GraVy partitions the statements
into those that are unreachable, or from which exceptional termination
is impossible, inevitable, or possible. Further analysis can then
focus on the latter case. That is, even though some statements still
may terminate exceptionally, GraVy still computes a partial
result. This allows us to measure the progress of static verification.
We present an implementation of GraVy and evaluate it on several open
source projects.