<abstract xmlns="http://www.w3.org/1999/xhtml"><p>Current climate models are complex computer programs that are typically iterated time-step by time-step to predict the next set of values of the climate-related variables. Since these iterative methods are necessarily computed only for a fixed number of iterations, they are unable to answer the natural question whether there is a limit to the rise of global temperature. In order to answer that question we propose to combine climate models with software verification techniques that can find invariant conditions for the set of program variables. In particular, we apply the constraint database approach to software verification to find that the rise in global temperature is bounded according to the common Java Climate Model that implements the Wigley/Raper Upwelling-Diffusion Energy Balance Model climate model.</p></abstract>

Current climate models are complex computer programs that are typically iterated time-step by time-step to predict the next set of values of the climate-related variables. Since these iterative methods are necessarily computed only for a fixed number of iterations, they are unable to answer the natural question whether there is a limit to the rise of global temperature. In order to answer that question we propose to combine climate models with software verification techniques that can find invariant conditions for the set of program variables. In particular, we apply the constraint database approach to software verification to find that the rise in global temperature is bounded according to the common Java Climate Model that implements the Wigley/Raper Upwelling-Diffusion Energy Balance Model climate model.

Estimating the maximum rise in temperature according to climate models using abstract interpretation

Department of Computer Science & Engineering

Acta Universitatis Sapientiae, Informatica

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 License.

Current climate models are complex computer programs that are typically iterated time-step by time-step to predict the next set of values of the...

Estimating the maximum rise in temperature according to climate models using abstract interpretation

Data publikacji: 21 sie 2019

Zakres stron: 5 - 23

Otrzymano: 05 gru 2018

DOI: https://doi.org/10.2478/ausi-2019-0001

Słowa kluczowe
constraint database, Datalog, climate model, invariant, MLPQ system, software verification

© 2019 Peter Z. Revesz et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 License.

Estimating the maximum rise in temperature according to climate models using abstract interpretation

Data publikacji: 21 sie 2019

Zakres stron: 5 - 23

Otrzymano: 05 gru 2018

DOI: https://doi.org/10.2478/ausi-2019-0001

Słowa kluczoweconstraint database, Datalog, climate model, invariant, MLPQ system, software verification

© 2019 Peter Z. Revesz et al., published by Sciendo

This work is licensed under the Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 License.

Słowa kluczowe
constraint database, Datalog, climate model, invariant, MLPQ system, software verification