Analysing Computer Arithmetic to Improve Software Reliability
Grant number: DP140102194 | Funding period: 2014 - 2018
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.
Related publications (12)
An iterative approach to precondition inference using constrained Horn clauses
Bishoksan Kafle, John P Gallagher, Graeme Gange, Peter Schachte, Harald Sondergaard, Peter J Stuckey
We present a method for automatic inference of conditions on the initial states of a program that guarantee that the safety assert..