This page links to the original bug reports that were made to the developers of different, compilers, and other software artifacts. These are all subtle bugs that are very hard to catch just through manual inspection (even after the tool points out the issue to you). The developers usually responded with thanks and fixed all these bugs promptly.

1. Bug in ICC-16.03 involving integer overflow.
   • This bug was found by our translation validator that checks equivalence between the generated binary and the original C program.
2. Bug in ICC-16.03 related to incorrect reordering of memory accesses.
   • This bug was found by our translation validator that checks equivalence between the generated binary and the original C program.
3. Bug in GCC-4.8 involving incorrect reordering of memory accesses.
   • This bug was found by our translation validator that checks equivalence between the generated binary and the original C program.
4. Bug in Qemu machine emulator that is shipped with Linux/KVM hypervisor.
   • This bug was found by our translation validator that checks equivalence between the generated PowerPC binary and the original x86 binary (in the context of Qemu's binary translator).
   • Sorav Bansal was tipped bitcoins for this bug fix
5. Three bugs in DietLibc, a C library for embedded systems (We describe one of the bugs below).
   • 
   • All these bugs involve subtle interactions of the char and int types. These bugs had escaped years of testing and production use.
   • The maintainer accepted these bug fixes with thanks. Abhishek Rose was acknowledged as a Dietlibc contributor by virtue of these fixes.
6. Bugs in Yices and Z3 SMT solvers
   • These bugs were found by differentially testing the output of one SMT solver against others during our verification runs for C programs.
   • Such bugs confirm that verification tools themselves are not immune to bugs. But it is usually possible to identify these bugs through simple testing, as we do in our tool.
7. Bug in strrchr() function in klibc-2.0.11 related to missing handling of c == 0 (kernel)
   • This bug relates to the case when the character to be searched is itself the null-character. This bug was identified by comparing multiple implementations of a C library function for equivalence using our equivalence checker.
8. Bug in swab() function in NetBSD’s C library (3290fbc).Fix on Github
   • This bug relates to an incorrect output on a well-formed input to the swab function. This bug was identified by comparing multiple implementations of a C library function for equivalence using our equivalence checker.
   • This bug was fixed upon our reporting and the Github commit message mentions that this bug had escaped over two decades of testing!
9. Bug in the memccpy() function in Newlib-4.2.0 (embedded systems C library)
   • This bug relates to a missing type-cast in the memccpy function. This bug was identified by comparing multiple implementations of a C library function for equivalence using our equivalence checker.