# Reducing Lookups for Invariant Checking

In this project we developed a simple algorithm to simplify boolean expressions and we used it in a case study for Google Maps for optimizing its invariant checking mechanism.

**Coq Source Code**

The Coq source code is available online. More information about the structure of the Coq source code and how to compile it can be found in the README file.

**Research paper**

*"Reducing Lookups for Invariant Checking"* with Christian Clausen, Kristoffer Andersen, John Danaher (Google), & Erik Ernst. In proceedings of ECOOP'13: European Conference on Object-Oriented Programming. : [ paper ]

**Abstract**

This paper helps reduce 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 satisfied. 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 simplifies a representation of the invariant, along with a mechan- ically verified 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 a factor of thirty performance improvement using this algorithm in a case study.