Domain Types: Selecting Abstractions Based on Variable Usage

Overview¶

This website provides supplementary material for the paper "Domain Types: Selecting Abstractions Based on Variable Usage". 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. 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. We experimentally demonstrate a significant impact of the choice of the abstract domain per variable. The experiments are based on standard verification tasks that are taken from recent competitions on software verification. We used and extended the verification framework CPAchecker (tag cpachecker-1.2.7-hvc13) for our experiments.

Results¶

We provide the results of our experiments on this supplementary website. The results are available for download as an archive or can be inspected in an interactive plot. To see a quantile plot of the cputimes click on the cell "cputime" in any of the configurations. We did not link the subject files and the log files, they are available in the CPAchecker repository (subject files) and in the result archive (log files). To enable other research groups to reproduce our results we also provide the CPAchecker configuration file for our experiments (here). To verify the ECA benchmarks, they have to be generated first. Use the script CPAchecker/test/programs/eca/prepare.php .

In the paper, we evaluate the number of variables per domain type. The corresponding results are available for download (as CSV file).