{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T02:46:42Z","timestamp":1767926802577,"version":"3.49.0"},"publisher-location":"Cham","reference-count":16,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319406473","type":"print"},{"value":"9783319406480","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-40648-0_24","type":"book-chapter","created":{"date-parts":[[2016,6,3]],"date-time":"2016-06-03T09:42:13Z","timestamp":1464946933000},"page":"322-336","source":"Crossref","is-referenced-by-count":11,"title":["A Modular Way to Reason About Iteration"],"prefix":"10.1007","author":[{"given":"Jean-Christophe","family":"Filli\u00e2tre","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"M\u00e1rio","family":"Pereira","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,6,4]]},"reference":[{"issue":"6","key":"24_CR1","doi-asserted-by":"crossref","first-page":"709","DOI":"10.1007\/s10009-014-0314-5","volume":"17","author":"F Bobot","year":"2015","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Let\u2019s verify this with Why3. Int. J. Softw. Tools Technol. Transf. (STTT) 17(6), 709\u2013727 (2015)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"Boyer, R.S., Moore, J.S.: Mjrty: A fast majority vote algorithm. In: Automated Reasoning: Essays in Honor of Woody Bledsoe, pp. 105\u2013118 (1991)","DOI":"10.1007\/978-94-011-3488-0_5"},{"key":"24_CR3","doi-asserted-by":"crossref","unstructured":"Chargu\u00e9raud, A.: Characteristic formulae for the verification of imperative programs. In: Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming (ICFP), pp. 418\u2013430. ACM, Tokyo, Japan, September 2011","DOI":"10.1145\/2034773.2034828"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/978-3-319-12154-3_3","volume-title":"Verified Software: Theories, Tools and Experiments","author":"M Clochard","year":"2014","unstructured":"Clochard, M., Filli\u00e2tre, J.-C., March\u00e9, C., Paskevich, A.: Formalizing semantics with an automatic program verifier. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 37\u201351. Springer, Heidelberg (2014)"},{"key":"24_CR5","volume-title":"Advanced C++ Programming Styles and Idioms","author":"JO Coplien","year":"1992","unstructured":"Coplien, J.O.: Advanced C++ Programming Styles and Idioms. Addison-Wesley, Reading (1992)"},{"key":"24_CR6","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.C.: Backtracking iterators. In: ACM SIGPLAN Workshop on ML, Portland, Oregon, September 2006","DOI":"10.1145\/1159876.1159885"},{"key":"24_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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":"24_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/978-3-319-08867-9_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)"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"308","DOI":"10.1007\/978-3-642-38977-1_23","volume-title":"Safe and Secure Software Reuse","author":"G Kulczycki","year":"2013","unstructured":"Kulczycki, G.: A language for building verified software components. In: Favaro, J., Morisio, M. (eds.) ICSR 2013. LNCS, vol. 7925, pp. 308\u2013314. Springer, Heidelberg (2013)"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., Birkedal, L.: Ynot: reasoning with the awkward squad. In: Proceedings of ICFP 2008 (2008)","DOI":"10.1145\/1411204.1411237"},{"key":"24_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"414","DOI":"10.1007\/978-3-319-19249-9_26","volume-title":"FM 2015: Formal Methods","author":"N Polikarpova","year":"2015","unstructured":"Polikarpova, N., Tschannen, J., Furia, C.A.: A fully verified container library. In: Bj\u00f8rner, N., de Boer, F. (eds.) FM 2015. LNCS, vol. 9109, pp. 414\u2013434. Springer, Heidelberg (2015)"},{"key":"24_CR13","doi-asserted-by":"crossref","unstructured":"Rondon, P.M., Kawaguchi, M., Jhala, R.: Liquid types. In: Gupta, R., Amarasinghe, S.P. (eds.) PLDI 2008, Tucson, AZ, USA, 7\u201313 June 2008, pp. 159\u2013169. ACM (2008)","DOI":"10.1145\/1375581.1375602"},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"Swamy, N., Hri\u0163cu, C., Keller, C., Rastogi, A., Delignat-Lavaud, A., Forest, S., Bhargavan, K., Fournet, C., Strub, P.Y., Kohlweiss, M., Zinzindohoue, J.K., Zanella-B\u00e9guelin, S.: Dependent types and multi-monadic effects in F*. In: 43rd ACM Symposium on Principles of Programming Languages (POPL), pp. 256\u2013270. ACM, January 2016","DOI":"10.1145\/2837614.2837655"},{"key":"24_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"209","DOI":"10.1007\/978-3-642-37036-6_13","volume-title":"Programming Languages and Systems","author":"N Vazou","year":"2013","unstructured":"Vazou, N., Rondon, P.M., Jhala, R.: Abstract refinement types. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 209\u2013228. Springer, Heidelberg (2013)"},{"key":"24_CR16","doi-asserted-by":"crossref","unstructured":"Weide, B.W.: SAVCBS 2006 challenge: specification of iterators. In: Proceedings of the 2006 Conference on Specification and Verification of Component-Based Systems, SAVCBS 2006, NY, USA, pp. 75\u201377. ACM, New York (2006)","DOI":"10.1145\/1181195.1181211"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-40648-0_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,24]],"date-time":"2017-06-24T11:41:26Z","timestamp":1498304486000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-40648-0_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319406473","9783319406480"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-40648-0_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016]]}}}