Differential equations—a class of equations that relates variables with their rate of change—are used to model all types of physical systems, ranging from simple applications, like Newton’s laws of motion, to heat diffusion, quantum mechanics, and more.

Approaches to solving these types of equations can vary. To solve them numerically, techniques include stationary iterative methods, in which an initial guess is iterated upon over and over again until the result converges.

But what if a researcher goes through all this work, and the guess never does converge?

“If you run a simulation and get an unphysical result, you basically wasted resources,” explains Mohit Tekriwal, a postdoctoral researcher in LLNL’s Center for Applied Scientific Computing (CASC). “The idea is that you don’t want to wait to say something about the correctness until after you have run the simulation—you want some guarantee that the solution will at least converge.” (The flow chart above demonstrates the various types of errors that can occur in solving differential equations, including iterative convergence errors.)

Tekriwal co-authored a conference paper developing a formal verification of the mathematical properties of a set of differential equations that guarantee a convergent solution. The paper was presented at the NASA Formal Methods Symposium, held June 4–6 in Mountain View, CA, which provides a collaborative forum for theoreticians and practitioners to discuss formal techniques for software and system assurance for safety-critical systems. In particular, NASA uses SUNDIALS, a Livermore-developed ordinary differential equation solver, for simulating spacecraft trajectories.

The technique Tekriwal and his University of Michigan collaborators developed provides an approach to formally specify convergence for a linear system, and then obtain a set of machine-checkable conditions that a functional algorithm implementing the solver must adhere to in order to converge. A researcher can simply compare these conditions to their program to verify that their program conforms to the required specifications.

The team confirmed their theorem using Coq, an interactive theorem prover that checks mathematical assertions, and tested it on a one-dimensional model of heat diffusion in a rod.

“It’s exciting to stitch together so many different pieces to prove the theorem,” Tekriwal says. He notes that the work provides a foundation, but extending the theorem to develop conditions for nonlinear or higher-dimensional systems will require a much more rigorous mathematical framework. 

—Anashe Bandari