Sylvie Boldo, François Clément, Jean-Christophe Filliâtre, Micaela Mayero, Guillaume Melquiond, Pierre Weis. Trusting computations: A mechanized proof from partial differential equations to actual program. Computers & Mathematics with Applications, 68(3):325-352, 2014. [doi]
Abstract is missing.