@article{altuntas_baugh_2018, title={Hybrid theorem proving as a lightweight method for verifying numerical software}, DOI={10.1109/Correctness.2018.00005}, abstractNote={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.}, journal={PROCEEDINGS OF CORRECTNESS 2018: 2ND IEEE/ACM INTERNATIONAL WORKSHOP ON SOFTWARE CORRECTNESS FOR HPC APPLICATIONS}, publisher={IEEE}, author={Altuntas, Alper and Baugh, John}, year={2018}, pages={1–8} }
 @article{altuntas_baugh_2017, title={Adaptive subdomain modeling: A multi-analysis technique for ocean circulation models}, volume={115}, ISSN={["1463-5011"]}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-85020014888&partnerID=MN8TOARS}, DOI={10.1016/j.ocemod.2017.05.009}, abstractNote={Many coastal and ocean processes of interest operate over large temporal and geographical scales and require a substantial amount of computational resources, particularly when engineering design and failure scenarios are also considered. This study presents an adaptive multi-analysis technique that improves the efficiency of these computations when multiple alternatives are being simulated. The technique, called adaptive subdomain modeling, concurrently analyzes any number of child domains, with each instance corresponding to a unique design or failure scenario, in addition to a full-scale parent domain providing the boundary conditions for its children. To contain the altered hydrodynamics originating from the modifications, the spatial extent of each child domain is adaptively adjusted during runtime depending on the response of the model. The technique is incorporated in ADCIRC++, a re-implementation of the popular ADCIRC ocean circulation model with an updated software architecture designed to facilitate this adaptive behavior and to utilize concurrent executions of multiple domains. The results of our case studies confirm that the method substantially reduces computational effort while maintaining accuracy.}, journal={OCEAN MODELLING}, author={Altuntas, Alper and Baugh, John}, year={2017}, month={Jul}, pages={86–104} }
 @article{baugh_altuntas_2016, place={Cham}, title={Modeling a Discrete Wet-Dry Algorithm for Hurricane Storm Surge in Alloy}, volume={9675}, ISBN={["978-3-319-33599-5"]}, ISSN={["1611-3349"]}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-84978698635&partnerID=MN8TOARS}, DOI={10.1007/978-3-319-33600-8_18}, abstractNote={We describe an Alloy model that helps check the correctness of a discrete wet-dry algorithm used in a system for hurricane storm surge prediction. Derived from simplified physics and encoded with empirical rules, the algorithm operates on a finite element mesh to allow the propagation of overland flows. Our study is motivated by complex interactions between the algorithm and a recent performance enhancement to the system that involves mesh partitioning. We briefly outline our approach and describe safety properties of the extension, as well as directions for future work.}, note={Lecture Notes in Computer Science 9675}, journal={ABSTRACT STATE MACHINES, ALLOY, B, TLA, VDM, AND Z (ABZ 2016)}, publisher={Springer}, author={Baugh, John and Altuntas, Alper}, editor={Butler, Michael and Schewe, Klaus-Dieter and Mashkoor, Atif and Biro, MiklosEditors}, year={2016}, pages={256–261} }
 @article{baugh_altuntas_dyer_simon_2015, title={An exact reanalysis technique for storm surge and tides in a geographic region of interest}, volume={97}, ISSN={["1872-7379"]}, url={http://www.scopus.com/inward/record.url?eid=2-s2.0-85027939365&partnerID=MN8TOARS}, DOI={10.1016/j.coastaleng.2014.12.003}, abstractNote={Understanding the effects of storm surge in hurricane-prone regions is necessary for protecting public and lifeline services and improving resilience. While coastal ocean hydrodynamic models like ADCIRC may be used to assess the extent of inundation, the computational cost may be prohibitive since many local changes corresponding to design and failure scenarios would ideally be considered. We present an exact reanalysis technique and corresponding implementation that enable the assessment of local subdomain changes with less computational effort than would be required by a complete resimulation of the full domain. So long as the subdomain is large enough to fully contain the altered hydrodynamics, changes may be made and simulations performed within it without the need to calculate new boundary values. Accurate results are obtained even when subdomain boundary conditions are forced only intermittently, and convergence is demonstrated by progressively increasing the frequency at which they are applied. Descriptions of the overall methodology, performance results, and accuracy, as well as case studies, are presented.}, journal={COASTAL ENGINEERING}, author={Baugh, John and Altuntas, Alper and Dyer, Tristan and Simon, Jason}, year={2015}, month={Mar}, pages={60–77} }