Jump to Content

Reducing Lookups for Invariant Checking

Jakob G. Thomsen
Christian Clausen
Kristoffer J. Andersen
Erik Ernst
John Danaher
Proceedings of ECOOP 2013 (to appear)
Google Scholar


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

Research Areas