{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,6]],"date-time":"2025-11-06T20:17:32Z","timestamp":1762460252817},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319104300"},{"type":"electronic","value":"9783319104317"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-10431-7_26","type":"book-chapter","created":{"date-parts":[[2014,8,4]],"date-time":"2014-08-04T05:27:28Z","timestamp":1407130048000},"page":"317-331","source":"Crossref","is-referenced-by-count":0,"title":["Verified Functional Iterators Using the FoCaLiZe Environment"],"prefix":"10.1007","author":[{"given":"Catherine","family":"Dubois","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Renaud","family":"Rioboo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"26_CR1","unstructured":"Proceedings of the 2006 Conference on Specification and Verification of Component-based Systems. ACM, New York (2006)"},{"key":"26_CR2","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-540-75560-9_13","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Bonichon","year":"2007","unstructured":"Bonichon, R., Delahaye, D., Doligez, D.: Zenon: An extensible automated theorem prover producing checkable proofs. In: Dershowitz, N., Voronkov, A. (eds.) LPAR 2007. LNCS (LNAI), vol.\u00a04790, pp. 151\u2013165. Springer, Heidelberg (2007)"},{"key":"26_CR3","unstructured":"Breunesse, C.-B., Poll, E.: Verifying jml specifications with model fields. In: Formal Techniques for Java-like Programs. Proceedings of the ECOOP 2003 Workshop (2003)"},{"key":"26_CR4","doi-asserted-by":"crossref","unstructured":"Cok, D.R.: Specifying java iterators with jml and esc\/java2. In: Proceedings of the 2006 Conference on Specification and Verification of Component-based Systems, SAVCBS 2006, pp. 71\u201374. ACM (2006)","DOI":"10.1145\/1181195.1181210"},{"key":"26_CR5","doi-asserted-by":"crossref","unstructured":"Dubois, C., Hardin, T., Vigui Donzeau-Gouge, V.: Building certified components within focal. In: Loidl, H.-W. (ed.) Revised Selected Papers from the Fifth Symposium on Trends in Functional Programming, TFP 2004, M\u00fcnchen, Germany. Trends in Functional Programming, vol.\u00a05, pp. 33\u201348. Intellect (2006)","DOI":"10.2307\/j.ctv36xw0k5.6"},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.-C.: Backtracking iterators. In: Proceedings of the ACM Workshop on ML 2006, Portland, Oregon, USA, pp. 55\u201362. ACM (2006)","DOI":"10.1145\/1159876.1159885"},{"key":"26_CR7","volume-title":"Design patterns: elements of reusable object-oriented software","author":"E. Gamma","year":"1994","unstructured":"Gamma, E., Helm, R., Johnson, R., Vlissides, J.M.: Design patterns: elements of reusable object-oriented software. Addison-Wesley, Reading (1994)"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/3-540-45442-X_11","volume-title":"Mathematics of Program Construction","author":"M. Huisman","year":"2002","unstructured":"Huisman, M.: Verification of java\u2019s abstractcollection class: A case study. In: Boiten, E.A., M\u00f6ller, B. (eds.) MPC 2002. LNCS, vol.\u00a02386, pp. 175\u2013194. Springer, Heidelberg (2002)"},{"key":"26_CR9","unstructured":"Jacobs, B., Meijer, E., Piessens, F., Schulte, W.: Iterators revisited: Proof rules and implementation. In: Workshop on Formal Techniques For Java-like Programs, FTFJP (2005)"},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"King, S., Morgan, C.: An iterator construct for the refinement calculus. In: Fourth Irish Workshop on Formal Methods (2000)","DOI":"10.14236\/ewic\/IWFM2000.3"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"Krishnaswami, N.R.: Reasoning about iterators with separation logic. In: Proceedings of the 2006 Conference on Specification and Verification of Component-based Systems, SAVCBS 2006, pp. 83\u201386. ACM (2006)","DOI":"10.1145\/1181195.1181213"},{"issue":"12","key":"26_CR12","doi-asserted-by":"publisher","first-page":"1352","DOI":"10.1109\/32.62444","volume":"16","author":"D.A. Lamb","year":"1990","unstructured":"Lamb, D.A.: Specification of iterators. IEEE Trans. Software Eng.\u00a016(12), 1352\u20131360 (1990)","journal-title":"IEEE Trans. Software Eng."},{"key":"26_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"339","DOI":"10.1007\/978-3-642-14052-5_24","volume-title":"Interactive Theorem Proving","author":"P. Lammich","year":"2010","unstructured":"Lammich, P., Lochbihler, A.: The isabelle collections framework. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 339\u2013354. Springer, Heidelberg (2010)"},{"key":"26_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-15057-9_8","volume-title":"Verified Software: Theories, Tools, Experiments","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M., Monahan, R.: Dafny meets the verification benchmarks challenge. In: Leavens, G.T., O\u2019Hearn, P., Rajamani, S.K. (eds.) VSTTE 2010. LNCS, vol.\u00a06217, pp. 112\u2013126. Springer, Heidelberg (2010)"},{"key":"26_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-642-14808-8_17","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2010","author":"G. Malecha","year":"2010","unstructured":"Malecha, G., Morrisett, G.: Mechanized verification with sharing. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol.\u00a06255, pp. 245\u2013259. Springer, Heidelberg (2010)"},{"key":"26_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-642-16612-9_12","volume-title":"Runtime Verification","author":"P. Meredith","year":"2010","unstructured":"Meredith, P., Ro\u015fu, G.: Runtime verification with the RV system. In: Barringer, H., et al. (eds.) RV 2010. LNCS, vol.\u00a06418, pp. 136\u2013152. Springer, Heidelberg (2010)"},{"issue":"3-4","key":"26_CR17","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/s10472-009-9156-3","volume":"56","author":"R. Rioboo","year":"2009","unstructured":"Rioboo, R.: Invariants for the FoCaL language. Annals of Mathematics and Artificial Intelligence\u00a056(3-4), 273\u2013296 (2009)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"26_CR18","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, pp. 75\u201377. ACM (2006)","DOI":"10.1145\/1181195.1181211"}],"container-title":["Lecture Notes in Computer Science","Software Engineering and Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-10431-7_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,7,15]],"date-time":"2023-07-15T14:21:54Z","timestamp":1689430914000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-10431-7_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319104300","9783319104317"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-10431-7_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}