Estimating the maximum rise in temperature according to climate models using abstract interpretation. (English) Zbl 1477.68167
Summary: 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.
MSC:
| 68Q60 | Specification and verification (program logics, model checking, etc.) |
| 68P15 | Database theory |
| 86A08 | Climate science and climate modeling |
References:
| [1] | S. Anderson, P. Z. Revesz, CDB-PV: A constraint database-based program verifier, Proc. of the \(7^{th}\) International Symposium on Abstraction, Reformulation and Approximation, LNCS 4612, Springer, 2007, pp. 35-49. ⇒ 11, 21; |
| [2] | L. Bernstein et al., Climate Change 2007: Synthesis Report, Cambridge University Press, 2007. ⇒6, 7; |
| [3] | N. Collins et al., Design and implementation of components in the Earth System Modeling Framework, International Journal of High Performance Computing Applications, Fall/Winter 2005. DOI= 10.1177/1094342005056120. ⇒21; |
| [4] | P. Cousot, R. Cousot, Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints, Proce. ACM Principles on Programming Languages, ACM Press, 1977, pp. 238-252. ⇒11; |
| [5] | S. Haesevoets, B. Kuijpers, P. Z. Revesz, Affine-invariant triangulation of spatiotemporal data with an application to image retrieval, ISPRS International Journal of Geo-Information6, 4 (2017) 100. 37 pp. ⇒22; |
| [6] | C. Hill et al., Architecture of the Earth System Modeling Framework, Computing in Science and Engineering6 2004, Fall/Winter 2005. DOI= 10.1109/MCISE. 2004.1255817. ⇒21; |
| [7] | B. J. Hoskins, A. J. Simmons, A multi-layer spectral model and the semi-implicit method, Quarterly Journal of the Royal Meteorological Society101, 429 (1975) 637-655. ⇒21; |
| [8] | J. T. Houghton et al. (editors), Climate Change 2001: The Scientific Basis, Cambridge University Press, 2001. ⇒6, 7, 12, 13, 14, 21; |
| [9] | P. C Kanellakis, G. M. Kuper, P. Z. Revesz, Constraint query languages, Journal of Computer and System Sciences51, 1 (1995) 26-52. ⇒10; |
| [10] | L. Li, P. Z. Revesz, Interpolation methods for spatio-temporal geographic data, Computers, Environment and Urban Systems, 28, 3 (2004) 201-227. ⇒22; |
| [11] | B. Matthews, Java Climate Model, 2011. [Online]. Available: ⇒13; |
| [12] | S. C. B. Raper, J. M. Gregory, T. J. Osborn, Use of an upwelling-diffusion energy balance climate model to simulate and diagnose A/OGCM results, Climate Dynamics, 17 (2001) 601-613. ⇒12; |
| [13] | P. Z. Revesz, A closed form evaluation for Datalog queries with integer (gap)-order constraints, Theoretical Computer Science, 116, 1 (1993) 117-149. ⇒14; · Zbl 0785.68026 |
| [14] | P. Z. Revesz, Safe query languages for constraint databases, ACM Transactions on Database Systems, 23, 1 (1998) 117-149. ⇒14; |
| [15] | P. Z. Revesz, Introduction to Constraint Databases, Springer, 2002. ⇒10; · Zbl 0995.68035 |
| [16] | P. Z. Revesz, The constraint database approach to software verification, Proc. \(8^{th}\) International Conference on Verification, Model Checking, and Abstract Interpretation, LNCS 4349, Springer, 2007, pp. 329-345. ⇒7, 11, 21; · Zbl 1132.68339 |
| [17] | P. Z. Revesz, Introduction to Databases: From Biological to Spatio-Temporal, Springer, 2010. ⇒7, 8, 9, 10, 19; · Zbl 1191.68253 |
| [18] | P. Z. Revesz, A recurrence equation-based solution for the cubic spline interpolation problem, International Journal of Mathematical Models and Methods in Applied Sciences9 (2015) 446-452. ⇒22; |
| [19] | P. Z. Revesz, R. Chen, P. Kanjamala, Y. Li, Y. Liu, Y. Wang, The MLPQ/GIS constraint database system, ACM SIGMOD Record, 29, 2 (2000) p. 601. ⇒11; |
| [20] | P. Z. Revesz, R. J. Woodward, Variable bounds analysis of a climate model using software verification techniques, Proc. \(13^{th}\) International Conference on Software Engineering, Parallel and Distributed Systems, Gdansk, Poland, 2014, pp. 31-36. ⇒21; |
| [21] | P. Z. Revesz, S. Wu, Spatiotemporal reasoning about epidemiological data, Artificial Intelligence in Medicine, 38, 2 (2006) 157-170. ⇒22; |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
