Catchconv is a proof-of-concept tool that generates test cases for signed/unsigned conversion erors in binary code. Using Valgrind, Catchconv observes a Linux binary program on an example input, then generates a query for the STP decision procedure. If a signed/unsigned bug exists, STP then synthesizes new program inputs that exhibit the bug. Well, in principle, anyway. In practice we're still working on it.... read more