Minimally Comparing Relational Abstract Domains

Kenny Ballou, Elena Sherman

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

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.

Original languageAmerican English
Title of host publicationATVA 2023: Automated Technology for Verification and Analysis
StatePublished - 1 Jan 2023

Keywords

  • abstract domain comparison
  • abstract interpretation
  • data-flow analysis
  • static analysis

EGS Disciplines

  • Computer Sciences

Fingerprint

Dive into the research topics of 'Minimally Comparing Relational Abstract Domains'. Together they form a unique fingerprint.

Cite this