Program analysis using abstract interpretation has been successfully applied in practice to find run-time bugs or prove software correct. Often, these techniques rely on numerical abstract domains, such as intervals (boxes), octagons, or polyhedra to compute over-approximations of the reachable state-space efficiently. Most domains that are used widely rely on convexity for their scalability.
However, the ability to express non-convex properties is sometimes mandatory in order to achieve a precise analysis of some numerical properties. This work combines already known abstract domains in a novel way in order to design new abstract domains that tackle some non-convex invariants. The abstract objects of interest are encoded as a pair of two convex abstract objects: the first abstract object defines an over-approximation of the possible reached values, as is done customarily. The second abstract object under-approximates the set of impossible values within the state-space of the first abstract object. Therefore, the geometrical concretization of our objects is defined by a convex set minus another convex set (or hole). We thus call these domains donut domains.
The talk is be twofold. The first part presents the abstract domain (lattice structure) with a focus on the set-theoretical operations (join and meet). The second part, dedicated to the assignment operation, presents a novel method to compute under-approximations, needed for soundness, of polyhedra based on arbitrary linear templates (boxes, zones, octagons, etc.). At the end of each part, we present preliminary experiments based on our implementation of donut domains on top of the Apron library.