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

Acta Universitatis Sapientiae: Informatica

Revesz Peter Z.¹  Woodward Robert J.¹ 

[1] University of Nebraska–Lincoln, Department of Computer Science & Engineering, LincolnNE 68588-0115, USA;

关键词: g.2.2;    68r15;    constraint database;    datalog;    climate model;    invariant;    mlpq system;    software verification;   

DOI  :  10.2478/ausi-2019-0001

来源: DOAJ

【 摘 要 】

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.

【 授权许可】

Unknown