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.