Towards a mostly-automated prover for bit-vector arithmetic

Abstract

We present work in progress on the development of EasyBV, a specialized theorem prover for fixed-size bit-vector arithmetic. © 2013 Authors.