This collection of papers was used in a reading course given during fall 2001.
The subject is integer range analysis. For example, given a program with an integer variable x, which values can x be bound to? Among the applications are elimination of array subscript range tests, worst-case execution time analysis and memory use optimizations.
It should be clear that it helps to know something about the relationships of variables. If we know that x == y+1, and we see a test x>0, we can deduce something about the value of y after the test succeeds. Several of the papers present techniques for reasoning about the relationships of variables.
Most of the papers are available online. However, the paper by Bultan et al. is not publicly available in the final version. My link goes to an earlier version. If you have an ACM account, or local access, you can get the final version. Karr's paper is not available online.
Patrick Cousot and Nicolas Halbwachs,
Automatic discovery of
linear constraints among variables of a program,
in Proc. of the
5th ACM Symp. on principles of programming languages (POPL), 84--96, 1978.
Michael P. Gerlek, Eric Stoltz and Michael Wolfe,
Beyond induction variables: detecting and classifying sequences using a
demand-driven SSA form,
ACM Trans. Program. Lang. Syst. 17, 1 (Jan. 1995), Pages 85 - 122.
Priyadarshan Kolte and Michael Wolfe,
Elimination of redundant array subscript range checks,
Proceedings of the conference on Programming
language design and implementation, 1995, Pages 270-278
Tevfik Bultan, Richard Gerber and William Pugh,
Model-checking concurrent systems with unbounded integer variables:
symbolic representations, approximations, and experimental results,
ACM Trans. Program. Lang. Syst.
21, 4 (Jul. 1999), Pages 747 - 789.
Local copy.
Acm copy.
J.R.C. Patterson,
Accurate static
branch prediction by value range propagation.
POPL'95, pages 67--78, 1995.
P. López-García, M. Hermenegildo, S. Debray, and
N. W. Lin,
Lower bound cost estimation for logic
programs.
Proceedings of the 1997 International Logic Programming
Symposium, pages 291--306, MIT Press, 1997.
Rastislav Bodík, Rajiv Gupta and Vivek Sarkar,
ABCD: eliminating array bounds checks on demand
PLDI'00,
Pages 321 - 333, 2000.
Radu Rugina and Martin Rinard,
Symbolic bounds analysis of pointers, array indices, and accessed memory regions
PLDI'00, Pages 182 - 195, 2000.
Mark Stephenson,
Jonathan Babb and Saman Amarasinghe,
Bidwidth analysis with application to silicon compilation,
PLDI'00, Pages 108 - 120, 2000.
R. van Engelen,
Efficient Symbolic Analysis for Optimizing Compilers,
Proceedings of the International Conference on Compiler Construction,
ETAPS 2001, LNCS 2027, pp. 118-132.
David Wagner, Jeffrey S. Foster, Eric A. Brewer, and Alexander
Aiken.
"
A First Step Toward Automated Detection of
Buffer Overrun Vulnerabilities."
Proceedings of the Network and
Distributed System Security Symposium, San Diego, California,
February 2000.
C. Healy, M. Sjodin, V. Rustagi, D. Whalley, and R. van Engelen,
"Supporting Timing Analysis by Automatic Bounding of Loop Iterations"
in Real-Time Systems, May 2000, pages 121-148.
W.-N. Chin and S.-C. Khoo,
Calculating sized types,
PEPM'00, pages 62--72. ACM, New York,
Jan. 2000.