Valentin Robert, Xavier Leroy: A Formally-Verified Alias Analysis. CPP 2012: 11-26