Source-Level Bitwise Branching for Temporal Verification

TL;DR

This paper introduces source-level bitwise branching transformations that over-approximate bitvector operations with linear constraints, enhancing the capability of verification tools for termination and LTL verification of bitvector programs.

Contribution

It presents novel source-level transformations using rewriting and weakening rules to improve verification of bitvector programs by leveraging integer reasoning.

Findings

Enables competitive termination verification of bitvector programs.

First effective technique for LTL verification of bitvector programs.

Improves verification success by over-approximating bitvector operations with linear constraints.

Abstract

There is increasing interest in applying verification tools to programs that have bitvector operations. SMT solvers, which serve as a foundation for these tools, have thus increased support for bitvector reasoning through bit-blasting and linear arithmetic approximations. Still, verification tools are limited on termination and LTL verification of bitvector programs. In this work, we show that similar linear arithmetic approximation of bitvector operations can be done at the source level through transformations. Specifically, we introduce new paths that over-approximate bitvector operations with linear conditions/constraints, increasing branching but allowing us to better exploit the well-developed integer reasoning and interpolation of verification tools. We present two sets of rules, namely rewriting rules and weakening rules, that can be implemented as bitwise branching of program transformation, the branching path can facilitate verification tools widen verification tasks over bitvector programs. Our experiment shows this exploitation of integer reasoning and interpolation enables competitive termination verification of bitvector programs and leads to the first effective technique for LTL verification of bitvector programs.