Analysing Computer Arithmetic to Improve Software Reliability

大多数计算机程序处理整数。用于验证软件正确行为的自动化工具通常假设软件处理理想化的数学整数，因为这大大简化了推理。实际上，大多数程序都使用近似理想的整数表示。这损害了许多核查工具的可靠性。这个项目将设计出合理的推理工具，了解计算机整数运算的真正本质。

Most computer programs deal with integers. Automated tools designed to verify the correct behaviour of software usually assume the software deals with idealised mathematical integers, since this simplifies reasoning significantly. In reality, most programs work with integer number representations that approximate the ideal. This compromises the soundness of many verification tools. This project will design sound reasoning tools that are aware of the true nature of computer integer arithmetic.