Domain Types: Selecting Abstractions Based on Variable Usage

TL;DR

This paper introduces domain types to classify program variables based on usage, guiding the selection of abstract domains in software model checking to improve verification efficiency and accuracy.

Contribution

It proposes a novel method to determine domain types through variable usage analysis and assigns abstract domains accordingly, enhancing model checking performance.

Findings

Significant impact of domain-type guided domain selection on verification results

Effective classification of variables improves abstract domain assignment

Experimental validation on standard verification tasks shows performance gains

Abstract

The success of software model checking depends on finding an appropriate abstraction of the subject program. The choice of the abstract domain and the analysis configuration is currently left to the user, who may not be familiar with the tradeoffs and performance details of the available abstract domains. We introduce the concept of domain types, which classify the program variables into types that are more fine-grained than standard declared types, such as int or long, in order to guide the selection of an appropriate abstract domain for a model checker. Our implementation determines the domain type for each variable in a pre-processing step, based on the variable usage in the program, and then assigns each variable to an abstract domain. The model-checking framework that we use supports to specify a separate analysis precision for each abstract domain, such that we can freely configure the analysis. We experimentally demonstrate a significant impact of the choice of the abstract domain per variable. We consider one explicit (hash tables for integer values) and one symbolic (binary decision diagrams) domain. The experiments are based on standard verification tasks that are taken from recent competitions on software verification. Each abstract domain has unique advantages in representing the state space of variables of a certain domain type. Our experiments show that software model checkers can be improved with a domain-type guided combination of abstract domains.