TY - CHAP
T1 - Minimally Comparing Relational Abstract Domains
AU - Ballou, Kenny
AU - Sherman, Elena
N1 - Ballou, Kenny and Sherman, Elena. (2023). "Minimally Comparing Relational Abstract Domains". In E. André and J. Sun (Eds.), ATVA 2023: Automated Technology for Verification and Analysis (Lecture Notes in Computer Science, 159-175). Springer, Cham. https://doi.org/10.1007/978-3-031-45332-8_8
PY - 2023/1/1
Y1 - 2023/1/1
N2 - Value-based static analysis techniques express computed program invariants as logical formula over program variables. Researchers and practitioners use these invariants to aid in software engineering and verification tasks. When selecting abstract domains, practitioners weigh the cost of a domain against its expressiveness. However, an abstract domain’s expressiveness tends to be stated in absolute terms; either mathematically via the sub-polyhedra the domain is capable of describing, empirically using a set of known properties to verify, or empirically via logical entailment using the entire invariant of the domain at each program point. Due to carry-over effects, however, the last technique can be problematic because it tends to provide simplistic and imprecise comparisons. We address these limitations of comparing, in general, abstract domains via logical entailment in this work. We provide a fixed-point algorithm for including the minimally necessary variables from each domain into the compared formula. Furthermore, we empirically evaluate our algorithm, comparing different techniques of widening over the Zones domain and comparing Zones to an incomparable Relational Predicates domain. Our empirical evaluation of our technique shows an improved granularity of comparison. It lowered the number of more precise invariants when comparing analysis techniques, thus, limiting the prevalent carry-over effects. Moreover, it removed undecidable invariants and lowered the number of incomparable invariants when comparing two incomparable relational abstract domain.
AB - Value-based static analysis techniques express computed program invariants as logical formula over program variables. Researchers and practitioners use these invariants to aid in software engineering and verification tasks. When selecting abstract domains, practitioners weigh the cost of a domain against its expressiveness. However, an abstract domain’s expressiveness tends to be stated in absolute terms; either mathematically via the sub-polyhedra the domain is capable of describing, empirically using a set of known properties to verify, or empirically via logical entailment using the entire invariant of the domain at each program point. Due to carry-over effects, however, the last technique can be problematic because it tends to provide simplistic and imprecise comparisons. We address these limitations of comparing, in general, abstract domains via logical entailment in this work. We provide a fixed-point algorithm for including the minimally necessary variables from each domain into the compared formula. Furthermore, we empirically evaluate our algorithm, comparing different techniques of widening over the Zones domain and comparing Zones to an incomparable Relational Predicates domain. Our empirical evaluation of our technique shows an improved granularity of comparison. It lowered the number of more precise invariants when comparing analysis techniques, thus, limiting the prevalent carry-over effects. Moreover, it removed undecidable invariants and lowered the number of incomparable invariants when comparing two incomparable relational abstract domain.
KW - abstract domain comparison
KW - abstract interpretation
KW - data-flow analysis
KW - static analysis
UR - https://scholarworks.boisestate.edu/cs_facpubs/402
UR - https://doi.org/10.1007/978-3-031-45332-8_8
M3 - Chapter
BT - ATVA 2023: Automated Technology for Verification and Analysis
ER -