QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers

ABSTRACT. This paper introduces QUICr, a library that implements abstract domains for simultaneous reasoning about numbers and sets of numbers. QUICr is an abstract domain combinator that lifts any domain for numbers into an efficient domain for numbers and sets of numbers. As a library, it is useful for inferring relational data invariants in programs that manipulate data structures. As a testbed, it allows easy extension of widening and join heuristics, enabling adaptations to new and varied applications. In this paper we present the architecture of the library, guidelines on how to select heuristics, and an example instantiation of the library using the NewPolka polyhedra library to verify set-manipulating programs.