|Home | People | Curriculum | Projects | Resources | Media|
In the late 90's, I performed detailed empirical studies of the behavior of the algorithms I use for simplification of Presburger Formulas. I identified several characteristics that lead to quick solution, rather than exponential blowup, for the formulas that arise during analysis of typical (benchmark) programs. These characteristics, as well as the algorithms and experimental system, are described in the paper (gzipped) that appeared in the May '98 issue of ACM Transactions on Programming Languages and Systems.
More recently, Rob Seater (HC '02) and I developed a formal description of a subdomain of Presburger Arithmetic that can be manipulated in polynomial time, and which includes almost all of the affine formulas involved in analysis of loop-carried dataflow. This work is described in our paper "Polynomial Time Array Dataflow Analysis" at LCPC '01. We went on to develop efficient algorithms for a domain that includes a wider variety of "disequality" constraints: See "Efficient Manipulation of Disequalities During Dependence Analysis" (published at LCPC '02) for details. I started this investigation at DIMACS (where I spent part of my junior leave); Vince Gabor (HC '99) worked with me during the preliminary investigation.