Analysing computer arithmetic to improve software reliability

Project description

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.

Project team

Leader: Peter Stuckey

Staff: Peter Stuckey, Harald Sondergaard, Peter Schachte

Collaborators: Michael Codish (Ben Gurion University of the Negev)

Sponsors: Australian Research Council

Other projects

Networks and data in society projects


Computing and Information Systems


Networks and data in society


programming languages