Methods for binary symbolic execution