Abstract
When proving safety of programs, we must show, in particular, the absence of integer overflows. Unfortunately, there are lots of situations where performing such a proof is extremely difficult, because the appropriate restrictions on function arguments are invasive and may be hard to infer. Yet, in certain cases, we can relax the desired property and only require the absence of overflow during the first n steps of execution, n being large enough for all practical purposes. It turns out that this relaxed property can be easily ensured for large classes of algorithms, so that only a minimal amount of proof is needed, if at all. The idea is to restrict the set of allowed arithmetic operations on the integer values in question, imposing a “speed limit” on their growth. For example, if we repeatedly increment a 64-bit integer, starting from zero, then we will need at least \(2^{64}\) steps to reach an overflow; on current hardware, this takes several hundred years. When we do not expect any single execution of our program to run that long, we have effectively proved its safety against overflows of all variables with controlled growth speed. In this paper, we give a formal explanation of this approach, prove its soundness, and show how it is implemented in the context of deductive verification.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Bloch, J.: Nearly all binary searches and mergesorts are broken (2006). http://googleresearch.blogspot.com/2006/06/extra-extra-read-all-about-it-nearly.html
Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Miné, A., Monniaux, D., Rival, X.: The Astrée static analyzer. http://www.astree.ens.fr/
Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. In: Proceedings of the 2009 IEEE/ACM International Conference on Automated Software Engineering, ASE 2009, pp. 137–148. IEEE Computer Society, Washington, DC (2009)
Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Hofmann, M., Felleisen, M. (eds.) Proceedings of 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2007), pp. 97–108, Nice, France, January 2007
Filliâtre, J.-C., Paskevich, A.: Why3 — where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125–128. Springer, Heidelberg (2013)
de Bruijn, N.G.: Lambda calculus with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Proc. K. Ned. Akad. 75(5), 380–392 (1972)
Littlewood, D., Richardson, A.: Group characters and algebra. In: Philosophical Transactions of the Royal Society of London: Mathematical and Physical Sciences. Harrison & Sons, London (1934)
Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, pp. 53–64, Wrocław, Poland, August 2011
Filliâtre, J.-C.: One logic to use them all. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 1–20. Springer, Heidelberg (2013)
Filliâtre, J.-C., Gondelman, L., Paskevich, A.: The spirit of ghost code. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 1–16. Springer, Heidelberg (2014)
Adel’son-Vel’skiĭ, G.M., Landis, E.M.: An algorithm for the organization of information. Sov. Math.-Dokl. 3(5), 1259–1263 (1962)
Acknowledgments
We are grateful to Arthur Charguéraud for detailed and constructive comments regarding a first draft of this paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Clochard, M., Filliâtre, JC., Paskevich, A. (2016). How to Avoid Proving the Absence of Integer Overflows. In: Gurfinkel, A., Seshia, S.A. (eds) Verified Software: Theories, Tools, and Experiments. VSTTE 2015. Lecture Notes in Computer Science(), vol 9593. Springer, Cham. https://doi.org/10.1007/978-3-319-29613-5_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-29613-5_6
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-29612-8
Online ISBN: 978-3-319-29613-5
eBook Packages: Computer ScienceComputer Science (R0)