Using Symbolic Execution to Verify the Order of Accuracy of Numerical Approximations

The order of accuracy of a numerical method relates the scheme's error to the discretization parameters. Scientists must know the order of accuracy of any numerical approximation, and often prove that the method satisfies the claimed order of accuracy by hand. However, the actual code to implement a method might be more complex and veer from the abstract mathematics. We show that the claimed order of accuracy of a numerical method implemented in a C program can be (largely) automatically verified using formal methods. The automation cannot be complete, because the problem is undecidable in general and because the programmer must provide some minimal annotations relating the code to the underlying mathematics. We have implemented the technique in the Concurrency Intermediate Verification Language model checker, and demonstrated its effectiveness on several finite difference method examples.

@TechReport{zirkel-siegel-rossi:2014:accuracy-tr,
	author = {Timothy K. Zirkel and Stephen F. Siegel and Louis F. Rossi},
	title = {Using Symbolic Execution to Verify the Order of Accuracy of Numerical Approximations},
	institution = {Department of Computer and Information Sciences, University of Delaware},
	year = {2014},
	number = {UD-CIS-2014/002}
}