Presentation
Hybrid Theorem Proving as a Lightweight Method for Verifying Numerical Software
Author/Presenters
Event Type
Workshop
W
Applications
Correctness
Debugging
Verification
TimeMonday, November 12th10:30am - 10:50am
LocationD171
DescriptionLarge-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