Source-Level Bitwise Branching for Temporal Verification

Yuandong Cyrus Liu, Ton-Chanh Le, Eric Koskinen

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 increase…