The Stormer-Verlet ("leapfrog") method is a numerical method for solving ordinary differential equations (ODEs).
This repository contains Coq proofs for the formal verification of a C implementation of leapfrog integration of the simple harmonic oscillator.
A dependency graph for our theorems in the leapfrog_project directory can be found in the project paper draft.