Abstract
We consider integer arithmetic modulo a power of 2 as provided by mainstream programming languages like Java or standard implementations of C. The difficulty here is that the ring ℤm of integers modulo m = 2ω, ω > 1, has zero divisors and thus cannot be embedded into a field. Not withstanding that, we present intra- and inter-procedural algorithms for inferring for every program point u, affine relations between program variables valid at u. Our algorithms are not only sound but also complete in that they detect all valid affine relations. Moreover, they run in time linear in the program size and polynomial in the number of program variables and can be implemented by using the same modular integer arithmetic as the target language to be analyzed.
Original language | English |
---|---|
Pages (from-to) | 46-60 |
Number of pages | 15 |
Journal | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
Volume | 3444 |
DOIs | |
State | Published - 2005 |
Event | 14th European Symposium on Programming, ESOP 2005, held as part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005 - Edinburgh, United Kingdom Duration: 4 Apr 2005 → 8 Apr 2005 |