Trusting computations: A mechanized proof from partial differential equations to actual program
Computers & Mathematics with Applications, pp. 325-352, 2014.
acoustic wave equationconvergence of numerical schemeformal proof of numerical programrounding error analysis
Computer programs may go wrong due to exceptional behaviors, out-of-bound array accesses, or simply coding errors. Thus, they cannot be blindly trusted. Scientific computing programs make no exception in that respect, and even bring specific accuracy issues due to their massive use of floating-point computations. Yet, it is uncommon to gu...更多