{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T09:59:36Z","timestamp":1742983176084,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031081651"},{"type":"electronic","value":"9783031081668"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"DOI":"10.1007\/978-3-031-08166-8_24","type":"book-chapter","created":{"date-parts":[[2022,7,3]],"date-time":"2022-07-03T23:03:27Z","timestamp":1656889407000},"page":"500-519","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Transparent Treatment of\u00a0for-Loops in\u00a0Proofs"],"prefix":"10.1007","author":[{"given":"Nathan","family":"Wasser","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,7,4]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book - From Theory to Practice. LNCS, vol. 10001. Springer (2016)","DOI":"10.1007\/978-3-319-49812-6"},{"key":"24_CR2","doi-asserted-by":"crossref","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. The KeY Approach, LNCS, vol.\u00a04334. Springer (2007)","DOI":"10.1007\/978-3-540-69061-0"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/11804192_16","volume-title":"Formal Methods for Components and Objects","author":"P Chalin","year":"2006","unstructured":"Chalin, P., Kiniry, J.R., Leavens, G.T., Poll, E.: Beyond assertions: advanced specification and verification with JML and ESC\/Java2. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 342\u2013363. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_16"},{"key":"24_CR4","doi-asserted-by":"crossref","unstructured":"Cok, D.R.: OpenJML: software verification for Java 7 using JML, OpenJDK, and Eclipse. In: Proceedings 1st Workshop on Formal Integrated Development Environment, pp. 79\u201392 (2014)","DOI":"10.4204\/EPTCS.149.8"},{"key":"24_CR5","unstructured":"Dreher, B.: Transparent treatment of loops in JavaDL. B.Sc. thesis, Darmstadt University of Technology, Germany (2019)"},{"issue":"5","key":"24_CR6","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-011-0211-0","volume":"13","author":"JC Filli\u00e2tre","year":"2011","unstructured":"Filli\u00e2tre, J.C.: Deductive software verification. Int. J. Softw. Tools Technol. Transfer 13(5), 397 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on POPL, pp. 193\u2013205. ACM (2001)","DOI":"10.1145\/373243.360220"},{"key":"24_CR8","volume-title":"The Java Language Specification","author":"J Gosling","year":"1996","unstructured":"Gosling, J., Joy, B., Steele, G.L.: The Java Language Specification, 1st edn. Addison-Wesley Longman Publishing Co., Inc., Boston (1996)","edition":"1"},{"issue":"1","key":"24_CR9","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/s10817-017-9426-4","volume":"62","author":"S de Gouw","year":"2019","unstructured":"de Gouw, S., de Boer, F.S., Bubel, R., H\u00e4hnle, R., Rot, J., Steinh\u00f6fel, D.: Verifying OpenJDK\u2019s sort method for generic collections. J. Autom. Reason. 62(1), 93\u2013126 (2019)","journal-title":"J. Autom. Reason."},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"Harel, D., Tiuryn, J., Kozen, D.: Dynamic Logic. MIT Press (2000)","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-3-642-20398-5_4","volume-title":"NASA Formal Methods","author":"B Jacobs","year":"2011","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41\u201355. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4"},{"issue":"3","key":"24_CR12","first-page":"1","volume":"11","author":"B Jacobs","year":"2015","unstructured":"Jacobs, B., Vogels, F., Piessens, F.: Featherweight VeriFast. Log. Methods Comput. Sci. 11(3), 1\u201357 (2015)","journal-title":"Log. Methods Comput. Sci."},{"issue":"7","key":"24_CR13","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1145\/360248.360252","volume":"19","author":"JC King","year":"1976","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385\u2013394 (1976)","journal-title":"Commun. ACM"},{"key":"24_CR14","unstructured":"Kleene, S.C.: Representation of events in nerve nets and finite automata (1951)"},{"key":"24_CR15","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/j.jlap.2003.07.006","volume":"58","author":"C March\u00e9","year":"2004","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The KRAKATOA tool for certification of JAVA\/JAVACARD programs annotated in JML. J. Log. Algebr. Program. 58, 89\u2013106 (2004)","journal-title":"J. Log. Algebr. Program."},{"key":"24_CR16","unstructured":"Schlager, S.: Symbolic execution as a framework for deductive verification of object-oriented programs. Ph.D. thesis, Karlsruhe Institute of Technology (2007)"},{"key":"24_CR17","unstructured":"Steinh\u00f6fel, D.: Abstract execution: automatically proving infinitely many programs. Ph.D. thesis, Darmstadt University of Technology, Germany (2020). http:\/\/tuprints.ulb.tu-darmstadt.de\/8540\/"},{"key":"24_CR18","doi-asserted-by":"crossref","unstructured":"Steinh\u00f6fel, D., Wasser, N.: A new invariant rule for the analysis of loops with non-standard control flows. In: 13th International Conference on Integrated Formal Methods IFM, pp. 279\u2013294 (2017)","DOI":"10.1007\/978-3-319-66845-1_18"},{"key":"24_CR19","unstructured":"Stenzel, K.: Verification of Java card programs. Ph.D. thesis, Universit\u00e4t Augsburg (2005)"},{"key":"24_CR20","unstructured":"Wasser, N.: Automatic generation of specifications using verification tools. Ph.D. thesis, Darmstadt University of Technology, Germany (2016)"},{"key":"24_CR21","unstructured":"Wasser, N., Steinh\u00f6fel, D.: Using loop scopes with for-loops. Tech. rep., Darmstadt University of Technology, Germany (2019). https:\/\/arxiv.org\/abs\/1901.06839"},{"key":"24_CR22","unstructured":"Wasser, N., Steinh\u00f6fel, D.: Treating for-loops as first-class citizens in proofs. Tech. rep., Darmstadt University of Technology, Germany (2020). https:\/\/arxiv.org\/abs\/2002.00776"}],"container-title":["Lecture Notes in Computer Science","The Logic of Software. A Tasting Menu of Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-08166-8_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,3]],"date-time":"2022-07-03T23:40:45Z","timestamp":1656891645000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-08166-8_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031081651","9783031081668"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-08166-8_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"4 July 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}