Andrew W. Appel, Ariel Kellison: VCFloat2: Floating-Point Error Analysis in Coq. CPP 2024: 14-29