Sweeping in Abstract Interpretation

In this paper we present how sweeping line techniques, which are very popular in computational geometry, can be adapted for static analysis of computer software by abstract interpretation. We expose how concept of the sweeping line can be used to represent elements of a numerical abstract domain of boxes, which is a disjunctive refinement of a well known domain of intervals that allows finite number of disjunctions. We provide a detailed description of the representation along with standard domain operations algorithms. Furthermore we introduce very precise widening operator for the domain. Additionally we show that the presented idea of the representation based on sweeping line technique is a generalisation of the representation that uses Linear Decision Diagrams (LDD), which is one of possible optimisations of our idea. We also show that the presented widening operator is often more precise than the previous one.