Trusting computations: A mechanized proof from partial differential equations to actual program

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]

@article{BoldoCFMMW14,
  title = {Trusting computations: A mechanized proof from partial differential equations to actual program},
  author = {Sylvie Boldo and François Clément and Jean-Christophe Filliâtre and Micaela Mayero and Guillaume Melquiond and Pierre Weis},
  year = {2014},
  doi = {10.1016/j.camwa.2014.06.004},
  url = {http://dx.doi.org/10.1016/j.camwa.2014.06.004},
  researchr = {https://researchr.org/publication/BoldoCFMMW14},
  cites = {0},
  citedby = {0},
  journal = {Computers & Mathematics with Applications},
  volume = {68},
  number = {3},
  pages = {325-352},
}