{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:03:30Z","timestamp":1767927810513,"version":"3.49.0"},"publisher-location":"Cham","reference-count":11,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319296128","type":"print"},{"value":"9783319296135","type":"electronic"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-29613-5_6","type":"book-chapter","created":{"date-parts":[[2016,1,28]],"date-time":"2016-01-28T02:47:34Z","timestamp":1453949254000},"page":"94-109","source":"Crossref","is-referenced-by-count":7,"title":["How to Avoid Proving the Absence of Integer Overflows"],"prefix":"10.1007","author":[{"given":"Martin","family":"Clochard","sequence":"first","affiliation":[]},{"given":"Jean-Christophe","family":"Filli\u00e2tre","sequence":"additional","affiliation":[]},{"given":"Andrei","family":"Paskevich","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"Bloch, J.: Nearly all binary searches and mergesorts are broken (2006). \n                    http:\/\/googleresearch.blogspot.com\/2006\/06\/extra-extra-read-all-about-it-nearly.html"},{"key":"6_CR2","unstructured":"Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Min\u00e9, A., Monniaux, D., Rival, X.: The Astr\u00e9e static analyzer. \n                    http:\/\/www.astree.ens.fr\/"},{"key":"6_CR3","doi-asserted-by":"crossref","unstructured":"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\u2013148. IEEE Computer Society, Washington, DC (2009)","DOI":"10.1109\/ASE.2009.63"},{"key":"6_CR4","doi-asserted-by":"crossref","unstructured":"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\u2013108, Nice, France, January 2007","DOI":"10.1145\/1190216.1190234"},{"key":"6_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013)"},{"issue":"5","key":"6_CR6","first-page":"380","volume":"75","author":"NG Bruijn de","year":"1972","unstructured":"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\u2013392 (1972)","journal-title":"Proc. K. Ned. Akad."},{"key":"6_CR7","unstructured":"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)"},{"key":"6_CR8","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, pp. 53\u201364, Wroc\u0142aw, Poland, August 2011"},{"key":"6_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-38574-2_1","volume-title":"Automated Deduction \u2013 CADE-24","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C.: One logic to use them all. In: Bonacina, M.P. (ed.) CADE 2013. LNCS, vol. 7898, pp. 1\u201320. Springer, Heidelberg (2013)"},{"key":"6_CR10","series-title":"Lecture Notes in Computer Science","first-page":"1","volume-title":"Computer Aided Verification","author":"J-C Filli\u00e2tre","year":"2014","unstructured":"Filli\u00e2tre, J.-C., Gondelman, L., Paskevich, A.: The spirit of ghost code. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 1\u201316. Springer, Heidelberg (2014)"},{"issue":"5","key":"6_CR11","first-page":"1259","volume":"3","author":"GM Adel\u2019son-Vel\u2019ski\u012d","year":"1962","unstructured":"Adel\u2019son-Vel\u2019ski\u012d, G.M., Landis, E.M.: An algorithm for the organization of information. Sov. Math.-Dokl. 3(5), 1259\u20131263 (1962)","journal-title":"Sov. Math.-Dokl."}],"container-title":["Lecture Notes in Computer Science","Verified Software: Theories, Tools, and Experiments"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-29613-5_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T07:51:33Z","timestamp":1559375493000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-29613-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319296128","9783319296135"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-29613-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}