This paper describes the precise specification, design, analysis,
implementation, and measurements of an efficient algorithm for
solving regular tree grammar based constraints. The particular
constraints are for dead-code elimination on recursive data, but the
method used for the algorithm design and complexity analysis is
general and applies to other program analysis problems as well. The
method is centered around Paige's finite differencing,
i.e., computing expensive set expressions incrementally, and allows
the algorithm to be derived and analyzed formally and implemented
easily. We study higher-level transformations that make the derived
algorithm concise and allow its complexity to be analyzed
accurately. Although a rough analysis shows that the worst-case
time complexity is cubic in program size,
an accurate analysis shows that it is linear in the number of live
program points and in other parameters, including mainly the arity
of data constructors and the number of selector applications into
whose arguments the value constructed at a program point might flow.
These parameters explain the performance of the analysis in practice.
Our implementation also runs two to ten times as fast as a previous
implementation of an informally designed algorithm.