skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.


This content will become publicly available on October 15, 2026

Title: Specification and Verification for Climate Modeling: Formalization Leading to Impactful Tooling
Earth System Models (ESMs) are critical for understanding past climates and projecting future scenarios. However, the complexity of these models, which include large code bases, a wide community of developers, and diverse computational platforms, poses significant challenges for software quality assurance. The increasing adoption of GPUs and heterogeneous architectures further complicates verification efforts. Traditional verification methods often rely on bitwise reproducibility, which is not always feasible, particularly under new compilers or hardware. Manual expert evaluation, on the other hand, is subjective and time-consuming. Formal methods offer a mathematically rigorous alternative, yet their application in ESM development has been limited due to the lack of climate model-specific representations and tools. Here, we advocate for the broader adoption of formal methods in climate modeling. In particular, we identify key aspects of ESMs that are well suited to formal specification and introduce abstraction approaches for a tailored framework. To demonstrate this approach, we present a case study using CIVL model checker to formally verify a bug fix in an ocean mixing parameterization scheme. Our goal is to develop accessible, domain-specific formal tools that enhance model confidence and support more efficient and reliable ESM development.  more » « less
Award ID(s):
1955852 2124205
PAR ID:
10650048
Author(s) / Creator(s):
; ; ; ;
Editor(s):
Siegel, Stephen F; Gopalakrishnan, Ganesh
Publisher / Repository:
EPTCS
Date Published:
Journal Name:
Electronic Proceedings in Theoretical Computer Science
Volume:
432
ISSN:
2075-2180
Page Range / eLocation ID:
60 to 75
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. Abstract. Earth system models (ESMs) are useful tools forpredicting and understanding past and future aspects of the climate system.However, the biological and physical parameters used in ESMs can have widevariations in their estimates. Even small changes in these parameters canyield unexpected results without a clear explanation of how a particularoutcome was reached. The standard method for estimating ESM sensitivity isto compare spatiotemporal distributions of variables from different runs ofa single ESM. However, a potential pitfall of this method is that ESM outputcould match observational patterns because of compensating errors. Forexample, if a model predicts overly weak upwelling and low nutrientconcentrations, it might compensate for this by allowing phytoplankton tohave a high sensitivity to nutrients. Recently, we demonstrated that neuralnetwork ensembles (NNEs) are capable of extracting relationships betweenpredictor and target variables within ocean biogeochemical models. Beingable to view the relationships between variables, along with spatiotemporaldistributions, allows for a more mechanistically based examination of ESMoutputs. Here, we investigated whether we could apply NNEs to help usdetermine why different ESMs produce different spatiotemporal distributionsof phytoplankton biomass. We tested this using three cases. The first andsecond case used different runs of the same ESM, except that the physicalcirculations differed between them in the first case, while the biologicalequations differed between them in the second. Our results indicated thatthe NNEs were capable of extracting the relationships between variables fordifferent runs of a single ESM, allowing us to distinguish betweendifferences due to changes in circulation (which do not changerelationships) from changes in biogeochemical formulation (which do changerelationships). In the third case, we applied NNEs to two different ESMs.The results of the third case highlighted the capability of NNEs to contrastthe apparent relationships of different ESMs and some of the challenges itpresents. Although applied specifically to the ocean components of an ESM,our study demonstrates that Earth system modelers can use NNEs to separatethe contributions of different components of ESMs. Specifically, this allowsmodelers to compare the apparent relationships across different ESMs andobservational datasets. 
    more » « less
  2. null (Ed.)
    This paper explores the adoption of a group-based Enterprise Social Media (ESM) tool (i.e., Microsoft Teams) in the context of a mid-sized undergraduate course in Information and Technology Management (ITM), thereby providing insights into the use and design of tools for group-based learning settings. The study used a mixed-methods approach—interviews, surveys, and server-side (i.e., objective) data—to investigate the effects of three core ESM affordances (i.e., editability, persistence, and visibility) on students’ perceptions of ESM functionality and efficiency, and in turn, on ESM-enabled perceived team productivity as well as the students’ level of system usage. Through leveraging a combination of qualitative and quantitative (both unobtrusive and self-reported) data, this paper aims to provide insights into the use of ESMs in group-based classrooms which is a theme of great importance given the need for high-quality online education experiences, especially during the current pandemic. 
    more » « less
  3. Abstract Simple climate models (SCMs) are computationally efficient and capable of emulating global mean output of more complex Earth system models (ESMs). In doing so, SCMs can play a critical role in climate research as stand‐ins for the computationally more expensive models, especially in studies involving low, spatial, and/or temporal resolution, providing more computationally efficient sources of climate data. Here we use Hector v2.5.0 to emulate the multiforcing historical and RCP scenario output for 31 concentration and seven emission‐driven ESMs. When calibrating Hector, sufficient calibration data must be used to constrain the model; otherwise, climate and/or carbon parameters affecting physical processes may be able to trade off with one another, allowing for solutions to use physically unreasonable fitted parameter values as well as limiting the application of the SCM as an emulator. We also present a novel methodology that uses the ESM range as a calibration data, which can be adopted when faced with missing variable output from a specific model. 
    more » « less
  4. Abstract Earth System Models (ESMs) are essential tools for understanding and predicting global change, but they cannot explicitly resolve hillslope‐scale terrain structures that fundamentally organize water, energy, and biogeochemical stores and fluxes at subgrid scales. Here we bring together hydrologists, Critical Zone scientists, and ESM developers, to explore how hillslope structures may modulate ESM grid‐level water, energy, and biogeochemical fluxes. In contrast to the one‐dimensional (1‐D), 2‐ to 3‐m deep, and free‐draining soil hydrology in most ESM land models, we hypothesize that 3‐D, lateral ridge‐to‐valley flow through shallow and deep paths and insolation contrasts between sunny and shady slopes are the top two globally quantifiable organizers of water and energy (and vegetation) within an ESM grid cell. We hypothesize that these two processes are likely to impact ESM predictions where (and when) water and/or energy are limiting. We further hypothesize that, if implemented in ESM land models, these processes will increase simulated continental water storage and residence time, buffering terrestrial ecosystems against seasonal and interannual droughts. We explore efficient ways to capture these mechanisms in ESMs and identify critical knowledge gaps preventing us from scaling up hillslope to global processes. One such gap is our extremely limited knowledge of the subsurface, where water is stored (supporting vegetation) and released to stream baseflow (supporting aquatic ecosystems). We conclude with a set of organizing hypotheses and a call for global syntheses activities and model experiments to assess the impact of hillslope hydrology on global change predictions. 
    more » « less
  5. null (Ed.)
    Cherchiglia et al. Effects of ESM Use for Classroom Teams Proceedings of the Nineteenth Annual Pre-ICIS Workshop on HCI Research in MIS, Virtual Conference, December 12, 2020 1 An Exploration of the Effects of Enterprise Social Media Use for Classroom Teams Leticia Cherchiglia Michigan State University leticia@msu.edu Wietske Van Osch HEC Montreal & Michigan State University wietske.van-osch@hec.ca Yuyang Liang Michigan State University liangyuy@msu.edu Elisavet Averkiadi Michigan State University averkiad@msu.edu ABSTRACT This paper explores the adoption of Microsoft Teams, a group-based Enterprise Social Media (ESM) tool, in the context of a hybrid Information Technology Management undergraduate course from a large midwestern university. With the primary goal of providing insights into the use and design of tools for group-based educational settings, we constructed a model to reflect our expectations that core ESM affordances would enhance students’ perceptions of Microsoft Teams’ functionality and efficiency, which in turn would increase both students’ perceptions of group productivity and students’ actual usage of Microsoft Teams for communication purposes. In our model we used three core ESM affordances from Treem and Leonardi (2013), namely editability (i.e., information can be created and/or edited after creation, usually in a collaborative fashion), persistence (i.e., information is stored permanently), and visibility (i.e., information is visible to other users). Analysis of quantitative (surveys, server-side; N=62) and qualitative (interviews; N=7) data led to intriguing results. It seems that although students considered that editability, persistency, and visibility affordances within Microsoft Teams were convenient functions of this ESM, problems when working collaboratively (such as connectivity, formatting, and searching glitches) might have prevented considerations of this ESM as fast and user-friendly (i.e., efficient). Moreover, although perceived functionality and efficiency were positively connected to group productivity, hidden/non-intuitive communication features within this ESM might help explain the surprising negative connection between efficiency and usage of this ESM for the purpose of group communication. Another explanation is that, given the plethora of competing tools specifically designed to afford seamless/optimal team communication, students preferred to use more familiar tools or tools perceived as more efficient for group communication than Microsoft Teams, a finding consistent with findings in organizational settings (Van Osch, Steinfield, and Balogh, 2015). Beyond theoretical contributions related to the impact that ESM affordances have on users’ interaction perceptions, and the impact of users’ interaction perceptions on team and system outcomes, from a strategic and practical point of view, our findings revealed several challenges for the use of Microsoft Teams (and perhaps ESM at large) in educational settings: 1) As the demand for online education grows, collaborative tools such as Microsoft Teams should strive to provide seamless experiences for multiple-user access to files and messages; 2) Microsoft Teams should improve its visual design in order to increase ease of use, user familiarity, and intuitiveness; 3) Microsoft Teams appears to have a high-learning curve, partially related to the fact that some features are hidden or take extra steps/clicks to be accessed, thus undermining their use; 4) Team communication is a complex topic which should be further studied because, given the choice, students will fall upon familiar tools therefore undermining the full potential for team collaboration through the ESM. We expect that this paper can provide insights for educators faced with the choice for an ESM tool best-suited for group-based classroom settings, as well as designers interested in adapting ESMs to educational contexts, which is a promising avenue for market expansion. 
    more » « less