Interval analysis and machine arithmetic: why signedness ignorance is bliss

Graeme Gange, Jorge A. Navas, Peter Schachte, Harald Søndergaard, Peter J. Stuckey

Research output: Contribution to journalArticleResearchpeer-review

5 Citations (Scopus)

Abstract

The most commonly used integer types have fixed bit-width, making it possible for computations to wrap around, and many programs depend on this behaviour. Yet much work to date on program analysis and verification of integer computations treats integers as having infinite precision, and most analyses that do respect fixed width lose precision when overflow is possible. We present a novel integer interval abstract domain that correctly handles wrap-around. The analysis is signedness agnostic. By treating integers as strings of bits, only considering signedness for operations that treat them differently, we produce precise, correct results at a modest cost in execution time.

Original languageEnglish
Article number1
Number of pages35
JournalACM Transactions on Programming Languages and Systems
Volume37
Issue number1
DOIs
Publication statusPublished - Jan 2015
Externally publishedYes

Cite this