Google Research

Reducing Lookups for Invariant Checking

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


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

Learn more about how we do research

We maintain a portfolio of research projects, providing individuals and teams the freedom to emphasize specific types of work