<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

Publié en ligne: 21 août 2019

Pages: 5 - 23

Reçu: 05 déc. 2018

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

Mots clés
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

Publié en ligne: 21 août 2019

Pages: 5 - 23

Reçu: 05 déc. 2018

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

Mots clésconstraint 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.

Mots clés
constraint database, Datalog, climate model, invariant, MLPQ system, software verification