@inproceedings{altuntas-iss-2023,
title = {Verifying {ParamGen}: A case study in scientific software abstraction and modeling},
author = {Altuntas, Alper and Baugh, John and Nusbaumer, Jesse},
booktitle = {Proceedings of the 2023 Improving Scientific Software Conference},
note = {{(No.~NCAR/TN-576+PROC)}},
year = {2023},
pages = {1-9},
url_pdf = {papers/altuntas-iss-2023.pdf},
doi = {10.5065/j0e4-ss70},
abstract = {
We introduce ParamGen, an infrastructure library for climate models to
generate input files that specify physics, parameterizations, and
other behavior. ParamGen supports arbitrary Python expressions for
specifying a default set of runtime parameters and values, thereby
providing a high level of expressiveness and flexibility. Initially
developed for the MOM6 ocean component in Community Earth System Model
(CESM), ParamGen is now used by several additional CESM
components. Therefore, it is of high importance that it operates
correctly, i.e., absent any undesired and unexpected behavior. To that
end, we develop an abstract verification model of ParamGen in Alloy, a
software modeling and analysis tool with a declarative language that
combines first-order logic and relational calculus. We evaluate the
correctness of ParamGen via Alloy and discuss how abstract models and
formal verification can help quickly frame questions and get answers
regarding the structure and behavior of our scientific computing
applications. We also describe our experience in coming to a cleaner
and well-formed software design and abstractions as a result of the
modeling exercise we present in this study.}
}

{"_id":"W3thX7GaErYrDSWuj","bibbaseid":"altuntas-baugh-nusbaumer-verifyingparamgenacasestudyinscientificsoftwareabstractionandmodeling-2023","author_short":["Altuntas, A.","Baugh, J.","Nusbaumer, J."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"Verifying ParamGen: A case study in scientific software abstraction and modeling","author":[{"propositions":[],"lastnames":["Altuntas"],"firstnames":["Alper"],"suffixes":[]},{"propositions":[],"lastnames":["Baugh"],"firstnames":["John"],"suffixes":[]},{"propositions":[],"lastnames":["Nusbaumer"],"firstnames":["Jesse"],"suffixes":[]}],"booktitle":"Proceedings of the 2023 Improving Scientific Software Conference","note":"(No. NCAR/TN-576+PROC)","year":"2023","pages":"1-9","url_pdf":"papers/altuntas-iss-2023.pdf","doi":"10.5065/j0e4-ss70","abstract":"We introduce ParamGen, an infrastructure library for climate models to generate input files that specify physics, parameterizations, and other behavior. ParamGen supports arbitrary Python expressions for specifying a default set of runtime parameters and values, thereby providing a high level of expressiveness and flexibility. Initially developed for the MOM6 ocean component in Community Earth System Model (CESM), ParamGen is now used by several additional CESM components. Therefore, it is of high importance that it operates correctly, i.e., absent any undesired and unexpected behavior. To that end, we develop an abstract verification model of ParamGen in Alloy, a software modeling and analysis tool with a declarative language that combines first-order logic and relational calculus. We evaluate the correctness of ParamGen via Alloy and discuss how abstract models and formal verification can help quickly frame questions and get answers regarding the structure and behavior of our scientific computing applications. We also describe our experience in coming to a cleaner and well-formed software design and abstractions as a result of the modeling exercise we present in this study.","bibtex":"@inproceedings{altuntas-iss-2023,\ntitle = {Verifying {ParamGen}: A case study in scientific software abstraction and modeling},\nauthor = {Altuntas, Alper and Baugh, John and Nusbaumer, Jesse},\nbooktitle = {Proceedings of the 2023 Improving Scientific Software Conference},\nnote = {{(No.~NCAR/TN-576+PROC)}},\nyear = {2023},\npages = {1-9},\nurl_pdf = {papers/altuntas-iss-2023.pdf},\ndoi = {10.5065/j0e4-ss70},\nabstract = {\nWe introduce ParamGen, an infrastructure library for climate models to\ngenerate input files that specify physics, parameterizations, and\nother behavior. ParamGen supports arbitrary Python expressions for\nspecifying a default set of runtime parameters and values, thereby\nproviding a high level of expressiveness and flexibility. Initially\ndeveloped for the MOM6 ocean component in Community Earth System Model\n(CESM), ParamGen is now used by several additional CESM\ncomponents. Therefore, it is of high importance that it operates\ncorrectly, i.e., absent any undesired and unexpected behavior. To that\nend, we develop an abstract verification model of ParamGen in Alloy, a\nsoftware modeling and analysis tool with a declarative language that\ncombines first-order logic and relational calculus. We evaluate the\ncorrectness of ParamGen via Alloy and discuss how abstract models and\nformal verification can help quickly frame questions and get answers\nregarding the structure and behavior of our scientific computing\napplications. We also describe our experience in coming to a cleaner\nand well-formed software design and abstractions as a result of the\nmodeling exercise we present in this study.}\n}\n\n","author_short":["Altuntas, A.","Baugh, J.","Nusbaumer, J."],"key":"altuntas-iss-2023","id":"altuntas-iss-2023","bibbaseid":"altuntas-baugh-nusbaumer-verifyingparamgenacasestudyinscientificsoftwareabstractionandmodeling-2023","role":"author","urls":{" pdf":"https://jwbaugh.github.io/papers/altuntas-iss-2023.pdf"},"metadata":{"authorlinks":{}},"downloads":8},"bibtype":"inproceedings","biburl":"https://jwbaugh.github.io/jwb.bib","dataSources":["pewK2DSYXKNLH3TTe"],"keywords":[],"search_terms":["verifying","paramgen","case","study","scientific","software","abstraction","modeling","altuntas","baugh","nusbaumer"],"title":"Verifying ParamGen: A case study in scientific software abstraction and modeling","year":2023,"downloads":8}