<span class="var-sub_title">Hybrid Theorem Proving as a Lightweight Method for Verifying Numerical Software</span> SC18 Proceedings

The International Conference for High Performance Computing, Networking, Storage, and Analysis

2nd International Workshop on Software Correctness for HPC Applications (Correctness 2018)


Hybrid Theorem Proving as a Lightweight Method for Verifying Numerical Software

Authors: Alper Altuntas (National Center for Atmospheric Research)

Abstract: Large-scale numerical software requires substantial computer resources that complicate testing and debugging. A single run of a climate model may require many millions of core-hours and terabytes of disk space, making trial-and-error experiments burdensome and time consuming. In this study, we apply hybrid theorem proving from the field of cyber-physical systems to problems in scientific computation, and show how to verify the correctness of discrete updates that appear in the simulation of continuous physical systems. By viewing numerical software as a hybrid system that combines discrete and continuous behavior, test coverage and confidence in findings can be increased. We describe abstraction approaches for modeling numerical software and demonstrate the applicability of the approach in a case study that reproduces undesirable behavior encountered in a parameterization scheme, called the K-profile parameterization, widely used in ocean components of large-scale climate models. We then identify and model a fix in the configuration of the scheme, and verify that the undesired behavior is eliminated for all possible execution sequences. We conclude that hybrid theorem proving is an effective and efficient approach that can be used to verify and reason about properties of large-scale numerical software.

Archive Materials


Back to 2nd International Workshop on Software Correctness for HPC Applications (Correctness 2018) Archive Listing

Back to Full Workshop Archive Listing