Automated soundness proofs for dataflow analyses and transformations via local rules. - Sorin Lerner; Todd D. Millstein; Erika Rice; Craig Chambers (POPL, 2005)