Analysing computer arithmetic to improve software reliability


Project Leader: Peter Stuckey
Staff: Peter Stuckey, Harald Sondergaard, Peter Schachte
Collaborators: Michael Codish (Ben Gurion University of the Negev)
Sponsors: Australian Research Council
Primary Contact: Peter Stuckey (pstuckey@unimelb.edu.au)
Keywords: programming languages
Disciplines: Computing and Information Systems
Domains: Networks and data in society

This project aims to improve the reliability of the software we all use every day, by developing new techniques and tools for automatic reasoning about the integer computer arithmetic that the majority of programs use. Most program analyses treat integers as ideal mathematical integers, but this treatment can make reasoning unsound. Surprisingly, many existing automatic techniques for reasoning about computer integers are incorrect. The approaches that are sound are generally too inefficient for realistic programs and cannot automatically handle some ubiquitous programming constructs. This project will fill that gap, developing sound, tractable techniques for reasoning about computer integer arithmetic.