Lund University → Faculty of Engineering → Department of Computer Science

• EDAP15 Program Analysis
• Moodle
• Completion & Grades
• CourseGit
• Schedule
• Skills
• Lab Exercises

Abstract Domains

• Properties of Program Analyses
• Skill: [3.5]

In program analysis, an abstract domain is a mathematical structure that we use to represent program features of interest to a particular analysis.

An abstract domain is an abstraction over a Concrete Domain, such that each element of the abstract domain represents one or more elements of the underlying concrete domain. Thie representation is not exclusive: the same concrete element is typically represented by multiple abstract elements in the abstract domain.

For example, if the concrete domain is the set of natural numbers, the abstract domain might be the Parity Abstract Domain, which }consist of three elements: - EvenNumbers - OddNumbers - AllNumbers such that e.g. the number 3 is represented both by OddNumbers and by AllNumbers.

In practice, abstract domains usually take the form of a Lattice (if we add a bottom element to the above). In the example above, the element AllNumbers would be strictly greater than OddNumbers, so we would normally try to define the Interpretation of the number 3 as the most precise element:

$$\llbracket 3 \rrbracket = \textbf{OddNumber}$$

We often use a function $\llbracket - \rrbracket$ to "interpret" values from the concrete domain to the abstract domain, and overload this function to recursively define the mapping from the language under analysis to the abstract domain, for example, we might define:

$$\llbracket x + y \rrbracket = \left \{ \begin{array}{lcl} \llbracket x \rrbracket & \textsf{if} & \llbracket y \rrbracket = \textbf{EvenNumbers} \\ \llbracket y \rrbracket & \textsf{if} & \llbracket x \rrbracket = \textbf{EvenNumbers} \\ \textbf{EvenNumbers} & \textsf{if} & \llbracket x \rrbracket = \llbracket y \rrbracket = \textbf{OddNumbers} \\ \llbracket y \rrbracket & \textsf{otherwise}& \\ \end{array} \right .$$

While the abstract domains from Forward Data Flow Analysis and Backward Data Flow Analysis always take the form of a Lattice, some other forms of program analysis use abstract domains with less structure.