Martin Bodin, Thomas P. Jensen, Alan Schmitt: Certified Abstract Interpretation with Pretty-Big-Step Semantics. CPP 2015: 29-40