Boxes: A Symbolic Abstract Domain of Boxes

Symbolic Abstract Domain of Boxes Arie Gurfinkel and Sagar Chaki Carnegie Mellon University Abstract. Numeric abstract domains are widely used in program analyses. The simplest numeric domains over-approximate disjunction by an imprecise join, typically yielding path-insensitive analyses. This problem is addressed by domain refinements, such as finite powersets, which provide exact disjunction. However, developing correct and efficient disjunctive refinement is challenging. First, there must be an efficient way to represent and manipulate abstract values. The simple approach of usets of base abstract values” is often not scalable. Second, while a widening must strike the right balance between precision and the rate of convergence, it is notoriously hard to get correct. In this paper, we an implementation of the Boxes abstract domain – a refinement of the well-known Box (or Intervals) domain with finite disjunctions. An element of Boxes is a finite union of boxes, i.e., expre...

• Type: Journal
• Year: 2010
• Where: SAS
• Authors: Arie Gurfinkel, Sagar Chaki
• Keywords: Abstract Domain, Abstract Values, Boxes, Formal Methods, SAS 2010