Automated soundness proofs for dataflow analyses and transformations via local rules