This repository includes the KeYmaera X models of the KPP-scheme (a numerical ocean model parameterization) from a conference paper titled "Hybrid Theorem Proving as a Lightweight Method for Verifying Numerical Software".
Link to paper: https://ieeexplore.ieee.org/document/8638360
Cite: A. Altuntas and J. Baugh, "Hybrid Theorem Proving as a Lightweight Method for Verifying Numerical Software," 2018 IEEE/ACM 2nd International Workshop on Software Correctness for HPC Applications (Correctness), Dallas, TX, USA, 2018, pp. 1-8. doi: 10.1109/Correctness.2018.00005