Minimal Comparison of Octagonal Abstract Domains (opens in new tab)

Numerical abstract domains vary in their expressiveness; more expressive domains like Zones yield more precise invariants than Intervals. A comprehensive approach to selecting abstract domains is a minimal comparison of abstract states. However, to be effective, it requires abstract states to be free of spurious constraints. While previous work developed spurious constraint elimination for Zones, this work introduces a novel algorithm for elimin...