@InProceedings{10.1007/978-3-030-76384-8_20,
author="Tekriwal, Mohit
and Duraisamy, Karthik
and Jeannin, Jean-Baptiste",
editor="Dutle, Aaron
and Moscato, Mariano M.
and Titolo, Laura
and Mu{\~{n}}oz, C{\'e}sar A.
and Perez, Ivan",
title="A Formal Proof of the Lax Equivalence Theorem for Finite Difference Schemes",
booktitle="NASA Formal Methods",
year="2021",
publisher="Springer International Publishing",
address="Cham",
pages="322--339",
abstract="The behavior of physical systems is typically modeled using differential equations which are too complex to solve analytically. In practical problems, these equations are discretized on a computational domain, and numerical solutions are computed. A numerical scheme is called convergent, if in the limit of infinitesimal discretization, the bounds on the discretization error is also infinitesimally small. The approximate solution converges to the ``true solution'' in this limit. The Lax equivalence theorem enables a proof of convergence given consistency and stability of the method.",
isbn="978-3-030-76384-8"
}