Security is a continuing source of concern with the use of computers and software. Subtle programming errors that can be exploited by malicious hackers are continually being spotted even in the most widely used computer programs. One common error is code that allows buffers to overrun, that is, the program permits data to be written to a part of a memory which should really be forbidden. If a hacker can exploit such a memory access, then they might be able to launch a security attack. Such an attack is made by overwriting part of the program with a small program. One example of such a program is a "worm" that, when executed, not only erases precious work stored on the computer but often attacks other computers running the same buggy program. Since most computers today are connected via the Internet, it only takes a split second for a worm to attack other computers in the vicinity which in turn will attack many more. Worms like the MS Blaster Worm have incurred losses of hundreds of million of dollars to society by rendering computers unusable. Moreover, even those buffer overruns that cannot be exploited for malicious intent, still need to be tracked down because they are often symptomatic of errors or oversights introduced or made by the programmer. Therefore, detecting these errors is of great importance. To track down these faults, security companies such as Portcullis Computer Security recruit hackers who are prepared to use their skills and knowledge for fault finding. These so-called ethical hackers scrutinize code, manually searching for programming errors which can be exploited to create a security breach. Some of the most subtle errors relate to way computers store and manipulate numbers. Very large numbers can get mangled in a computer and if a program does not check that the result of calculation is erroneous, then it possible for the program to reach a confused state which can lay open the program, and the system on which the program runs, to attack. These problems reside in programs because it can be very difficult for a human to anticipate the knock-on effects of number mangling. Thus it is somewhat unsatisfactory relying on another human to check the program for such a flaw. Organisations such as Portcullis are therefore interested in collaborating in research on automating the discovery of such faults so that securing a program is less error-prone and more systematic. This suggests exploring techniques that have been developed within academia for fault finding. Within academia, the field of program analysis research is concerned with reasoning about programs in a systematic and principled way. This field of research is driven by fresh research challenges. Researchers are continually searching for new problems, particularly problems drawn from unusual settings, because these problems often lead to step-change advances in the field. The problem of diagnosing the potential for dangerous number mangling seems to be one such research problem where both the academic and industrial parties involved in the research stand to gain by working together on this problem.