@inproceedings{altuntas-correctness-2018,
author = {Altuntas, Alper and Baugh, John},
title = {Hybrid theorem proving as a lightweight method for verifying
  numerical software},
booktitle = {Proceedings of the Second International Workshop on
  Software Correctness for {HPC} Applications, {Correctness'18}},
year = {2018},
isbn = {978-1-7281-0226-9},
location = {Dallas, TX, USA},
pages = {1-8},
doi = {10.1109/Correctness.2018.00005},
url_pdf = {papers/altuntas-correctness-2018.pdf},
publisher = {IEEE},
keywords = {hybrid systems, formal methods, scientific computation,
  KeYmaera X},
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.}
}

{"_id":"nyqYShTu2WH9qJ9zs","bibbaseid":"altuntas-baugh-hybridtheoremprovingasalightweightmethodforverifyingnumericalsoftware-2018","author_short":["Altuntas, A.","Baugh, J."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Altuntas"],"firstnames":["Alper"],"suffixes":[]},{"propositions":[],"lastnames":["Baugh"],"firstnames":["John"],"suffixes":[]}],"title":"Hybrid theorem proving as a lightweight method for verifying numerical software","booktitle":"Proceedings of the Second International Workshop on Software Correctness for HPC Applications, Correctness'18","year":"2018","isbn":"978-1-7281-0226-9","location":"Dallas, TX, USA","pages":"1-8","doi":"10.1109/Correctness.2018.00005","url_pdf":"papers/altuntas-correctness-2018.pdf","publisher":"IEEE","keywords":"hybrid systems, formal methods, scientific computation, KeYmaera X","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.","bibtex":"@inproceedings{altuntas-correctness-2018,\nauthor = {Altuntas, Alper and Baugh, John},\ntitle = {Hybrid theorem proving as a lightweight method for verifying\n numerical software},\nbooktitle = {Proceedings of the Second International Workshop on\n Software Correctness for {HPC} Applications, {Correctness'18}},\nyear = {2018},\nisbn = {978-1-7281-0226-9},\nlocation = {Dallas, TX, USA},\npages = {1-8},\ndoi = {10.1109/Correctness.2018.00005},\nurl_pdf = {papers/altuntas-correctness-2018.pdf},\npublisher = {IEEE},\nkeywords = {hybrid systems, formal methods, scientific computation,\n KeYmaera X},\nabstract = {\nLarge-scale numerical software requires substantial computer resources\nthat complicate testing and debugging. A single run of a climate model\nmay require many millions of core-hours and terabytes of disk space,\nmaking trial-and-error experiments burdensome and time consuming. In\nthis study, we apply hybrid theorem proving from the field of\ncyber-physical systems to problems in scientific computation, and show\nhow to verify the correctness of discrete updates that appear in the\nsimulation of continuous physical systems. By viewing numerical\nsoftware as a hybrid system that combines discrete and continuous\nbehavior, test coverage and confidence in findings can be\nincreased. We describe abstraction approaches for modeling numerical\nsoftware and demonstrate the applicability of the approach in a case\nstudy that reproduces undesirable behavior encountered in a\nparameterization scheme, called the K-profile parameterization, widely\nused in ocean components of large-scale climate models. We then\nidentify and model a fix in the configuration of the scheme, and\nverify that the undesired behavior is eliminated for all possible\nexecution sequences. We conclude that hybrid theorem proving is an\neffective and efficient approach that can be used to verify and reason\nabout properties of large-scale numerical software.}\n}\n\n","author_short":["Altuntas, A.","Baugh, J."],"key":"altuntas-correctness-2018","id":"altuntas-correctness-2018","bibbaseid":"altuntas-baugh-hybridtheoremprovingasalightweightmethodforverifyingnumericalsoftware-2018","role":"author","urls":{" pdf":"https://jwbaugh.github.io/papers/altuntas-correctness-2018.pdf"},"keyword":["hybrid systems","formal methods","scientific computation","KeYmaera X"],"metadata":{"authorlinks":{}},"downloads":6},"bibtype":"inproceedings","biburl":"https://jwbaugh.github.io/jwb.bib","dataSources":["pewK2DSYXKNLH3TTe"],"keywords":["hybrid systems","formal methods","scientific computation","keymaera x"],"search_terms":["hybrid","theorem","proving","lightweight","method","verifying","numerical","software","altuntas","baugh"],"title":"Hybrid theorem proving as a lightweight method for verifying numerical software","year":2018,"downloads":6}