Verifying Bit-vector Invertibility Conditions in Coq (Extended Abstract)

Burak Ekici, Arjun Viswanathan, Yoni Zohar +2

This work is a part of an ongoing effort to prove the correctness of invertibility conditions for the theory of fixed-width bit-vectors, which are used to solve quantified bit-vect…