Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Minimally Comparing Relational Abstract Domains

Kenny Ballou, Elena Sherman

TL;DR

This paper tackles carry-over issues when comparing relational abstract domains by introducing a fixed-point algorithm that computes a common, minimally changed variable set $S$ using domain-specific minimization functions $\Delta$ and updated variables $dv$. It formalizes the problem in a DFA-like setting and provides a concrete algorithm to find $S$, enabling sound, fine-grained comparisons between Zones and Relational Predicates domains. Through extensive experiments on real Java methods, the authors show that minimal-change comparisons reduce undecidable and incomparable results, while preserving or clarifying precision gains across widening strategies. The approach yields a more reliable basis for selecting abstract domains and tuning analysis techniques, with potential extensions to additional relational domains and adaptive analysis scenarios.

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 a simplistic and imprecise comparisons. We address 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 domains.

Minimally Comparing Relational Abstract Domains

TL;DR

This paper tackles carry-over issues when comparing relational abstract domains by introducing a fixed-point algorithm that computes a common, minimally changed variable set using domain-specific minimization functions and updated variables . It formalizes the problem in a DFA-like setting and provides a concrete algorithm to find , enabling sound, fine-grained comparisons between Zones and Relational Predicates domains. Through extensive experiments on real Java methods, the authors show that minimal-change comparisons reduce undecidable and incomparable results, while preserving or clarifying precision gains across widening strategies. The approach yields a more reliable basis for selecting abstract domains and tuning analysis techniques, with potential extensions to additional relational domains and adaptive analysis scenarios.

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 a simplistic and imprecise comparisons. We address 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 domains.
Paper Structure (20 sections, 1 equation, 3 figures, 3 tables, 1 algorithm)

This paper contains 20 sections, 1 equation, 3 figures, 3 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Background and Motivation
  3. Minimal changes in relational abstract domains
  4. Comparing relational domains
  5. Approach
  6. Problem definition
  7. Finding a common changed variable set
  8. Methodology
  9. Subject programs
  10. Experimental platform
  11. Implementation
  12. Evaluations
  13. Evaluation Results and Discussions
  14. Technique Comparisons
  15. Zones versus Relational Predicates
  16. ...and 5 more sections

Figures (3)

  • Figure 1: Original Static Analysis (a) and Improved Static Analysis (b)
  • Figure 2: Frequency plot of proportion of variables selected by Algorithm \ref{['alg:fixed-point-union']} which are necessary for comparing two invariants. (a) represents the frequencies of proportions when comparing techniques using Zones. (b) represents the frequencies of proportions when comparing Zones to Relational Predicates.
  • Figure : Common minimal changed variable set

Theorems & Definitions (1)

  • proof