Reducing Lookups for Invariant Checking

This paper helps reducing the cost of invariant checking in
cases where access to data is expensive. Assume that a set of variables
satisfy a given invariant and a request is received to update a subset of
them. We reduce the set of variables to inspect, in order to verify that
the invariant is still satised. We present a formal model of this scenario,
based on a simple query language for the expression of invariants that
covers the core of a realistic query language. We present an algorithm
which simplies a representation of the invariant, along with a mechan-
ically veried proof of correctness. We also investigate the underlying
invariant checking problem in general and show that it is co-NP hard,
i.e., that solutions must be approximations to remain tractable. We have
seen more than an order of magnitude performance improvement using
these techniques in a case study

• Software Systems