I never wrote up all the details (which seemed somewhat mundane, since the bugs were in unproved code) but see Section 3.1 here: http://www.cs.utah.edu/~regehr

I never wrote up all the details (which seemed somewhat mundane, since the bugs were in unproved code) but see Section 3.1 here: http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf