muRelBench: MicroBenchmarks for Zonotope Domains

TL;DR

muRelBench is a flexible benchmarking framework designed to evaluate and validate the performance and correctness of algorithms in weakly-relational numerical abstract domains, facilitating rapid prototyping and comparison.

Contribution

It introduces an extensible microbenchmarking framework specifically for weakly-relational abstract domains, supporting performance evaluation and correctness verification.

Findings

Enables quick performance assessment of abstract domain algorithms

Supports correctness checks for synthetic benchmarks

Facilitates comparison of different numerical abstract domain operations

Abstract

We present \texttt{muRelBench}, a framework for synthetic benchmarks for weakly-relational abstract domains and their operations. This extensible microbenchmarking framework enables researchers to experimentally evaluate proposed algorithms for numerical abstract domains, such as closure,least-upper bound, and forget, enabling them to quickly prototype and validate performance improvements before considering more intensive experimentation. Additionally, the framework provides mechanisms for checking correctness properties for each of the benchmarks to ensure correctness within the synthetic benchmarks.