Tags:abstract domains, correctness, efficiency and precision
Abstract:
The Abstract Interpretation framework provides invaluable guidance for the design of abstract domains to be used in static analysis tools. Nonetheless, the development of an adequate abstract domain can be a challenging task: besides the mandatory correctness requirements, also its precision and efficiency need to be properly considered. Drawing mainly from past experience, we show a few examples of the problems that an abstract domain developer may be facing. We rediscuss the tradeoffs that could be adopted while working through the solutions, somehow confirming known rules of thumb, possible exceptions to the rules of thumb and other interesting relationships between correctness, precision and efficiency.