Frédéric Besson, Thomas P. Jensen, Tiphaine Turpin: Small Witnesses for Abstract Interpretation-Based Proofs. ESOP 2007: 268-283