Abstract interpretation offers sound and decidable approximations for undecidable queries related to program behavior. The effectiveness of an abstract domain is entirely reliant on the abstract domain itself, and the worst-case scenario is when the abstract interpreter provides a response of “don’t know,” indicating that anything could happen during runtime. Conversely, a desirable outcome is when the abstract interpreter provides information that exceeds a specified level of precision, resulting in a more precise answer. The concept of completeness relates to the level of precision that is forfeited when performing computations within the abstract domain. Our focus is on the domain’s ability to express program behaviour, which is referred to as adequacy. In this paper, we present a simple proof system for adequacy, designed to determine whether an abstract domain is capable of providing satisfactory responses to specified program queries. The proof system is sound and capable of detecting instances where the response generated by the abstract interpreter falls below a specified threshold. Notably, this proof system is both language and domain agnostic, and can be readily incorporated to support static program analysis.
Sun 22 OctDisplayed time zone: Lisbon change
11:00 - 12:30
|How fitting is your abstract domain?
Roberto Giacobazzi University of Arizona, Isabella Mastroeni University of Verona, Italy, Elia Perantoni University of VeronaPre-print
|Domain Precision in Galois Connection-less Abstract Interpretation
|A Formal Framework to Measure the Incompleteness of Abstract Interpretations
Marco Campion INRIA & École Normale Supérieure | Université PSL, Caterina Urban Inria & École Normale Supérieure | Université PSL, Mila Dalla Preda University of Verona, Roberto Giacobazzi University of ArizonaPre-print