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 mechanically 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. © 2013 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Thomsen, J. G., Clausen, C., Andersen, K. J., Danaher, J., & Ernst, E. (2013). Reducing lookups for invariant checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7920 LNCS, pp. 426–450). Springer Verlag. https://doi.org/10.1007/978-3-642-39038-8_18
Mendeley helps you to discover research relevant for your work.