{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,2]],"date-time":"2025-09-02T10:50:44Z","timestamp":1756810244828,"version":"3.37.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319668444"},{"type":"electronic","value":"9783319668451"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-66845-1_18","type":"book-chapter","created":{"date-parts":[[2017,8,26]],"date-time":"2017-08-26T11:37:20Z","timestamp":1503747440000},"page":"279-294","source":"Crossref","is-referenced-by-count":10,"title":["A New Invariant Rule for the Analysis of Loops with Non-standard Control Flows"],"prefix":"10.1007","author":[{"given":"Dominic","family":"Steinh\u00f6fel","sequence":"first","affiliation":[]},{"given":"Nathan","family":"Wasser","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,8,27]]},"reference":[{"key":"18_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6","volume-title":"Deductive Software Verification - The KeY Book","year":"2016","unstructured":"Ahrendt, W., Beckert, B. (eds.): Deductive Software Verification - The KeY Book. LNCS, vol. 10001. Springer, Cham (2016). doi: 10.1007\/978-3-319-49812-6"},{"key":"18_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11804192_17","volume-title":"Formal Methods for Components and Objects","author":"M Barnett","year":"2006","unstructured":"Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: Boer, F.S., Bonsangue, M.M., Graf, S., Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). doi: 10.1007\/11804192_17"},{"key":"18_CR3","unstructured":"Bobot, F., Filli\u00e2tre, J.C., et al.: Why3: Shepherd your herd of provers. In: Boogie 2011: First International Workshop on IVL, pp. 53\u201364 (2011)"},{"key":"18_CR4","unstructured":"Cadar, C., Dunbar, D., et al.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: 8th USENIX Conference on OSDI, pp. 209\u2013224. USENIX Association, Berkeley (2008)"},{"issue":"2","key":"18_CR5","doi-asserted-by":"crossref","first-page":"82","DOI":"10.1145\/2408776.2408795","volume":"56","author":"C Cadar","year":"2013","unstructured":"Cadar, C., Sen, K.: Symbolic execution for software testing: three decades later. Commun. ACM 56(2), 82\u201390 (2013)","journal-title":"Commun. ACM"},{"key":"18_CR6","doi-asserted-by":"crossref","unstructured":"Cok, D.R.: OpenJML: software verification for Java 7 using JML, OpenJDK, and Eclipse. In: Proceedings of the 1st Workshop on FIDE, pp. 79\u201392 (2014)","DOI":"10.4204\/EPTCS.149.8"},{"key":"18_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1007\/978-3-642-33826-7_16","volume-title":"Software Engineering and Formal Methods","author":"P Cuoq","year":"2012","unstructured":"Cuoq, P., Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds.) SEFM 2012. LNCS, vol. 7504, pp. 233\u2013247. Springer, Heidelberg (2012). doi: 10.1007\/978-3-642-33826-7_16"},{"issue":"1","key":"18_CR8","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1109\/TSE.1982.234773","volume":"SE\u20138","author":"R Dannenberg","year":"1982","unstructured":"Dannenberg, R., Ernst, G.: Formal program verification using symbolic execution. IEEE Trans. Softw. Eng. SE\u20138(1), 43\u201352 (1982)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"5","key":"18_CR9","doi-asserted-by":"crossref","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. Transf. (STTT) 13(5), 397\u2013403 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transf. (STTT)"},{"issue":"3","key":"18_CR10","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1145\/373243.360220","volume":"36","author":"C Flanagan","year":"2001","unstructured":"Flanagan, C., Saxe, J.B.: Avoiding exponential explosion: generating compact verification conditions. SIGPLAN Not. 36(3), 193\u2013205 (2001)","journal-title":"SIGPLAN Not."},{"key":"18_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-319-21690-4_16","volume-title":"Computer Aided Verification","author":"S Gouw","year":"2015","unstructured":"Gouw, S., Rot, J., Boer, F.S., Bubel, R., H\u00e4hnle, R.: OpenJDK\u2019s Java.utils.Collection.sort() is broken: the good, the bad and the worst case. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 273\u2013289. Springer, Cham (2015). doi: 10.1007\/978-3-319-21690-4_16"},{"key":"18_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-319-09099-3_7","volume-title":"Tests and Proofs","author":"M Hentschel","year":"2014","unstructured":"Hentschel, M., H\u00e4hnle, R., Bubel, R.: Visualizing unbounded symbolic execution. In: Seidl, M., Tillmann, N. (eds.) TAP 2014. LNCS, vol. 8570, pp. 82\u201398. Springer, Cham (2014). doi: 10.1007\/978-3-319-09099-3_7"},{"issue":"10","key":"18_CR13","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"18_CR14","doi-asserted-by":"crossref","unstructured":"Jaffar, J., Murali, V., et al.: Boosting concolic testing via interpolation. In: Proceedings of 9th Joint Meeting on FSE, pp. 48\u201358. USA. ACM, New York (2013)","DOI":"10.1145\/2491411.2491425"},{"issue":"1\u20132","key":"18_CR15","doi-asserted-by":"crossref","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., et al.: The KRAKATOA tool for certification of JAVA\/JAVACARD programs annotated in JML. J. Logic Algebr. Program. 58(1\u20132), 89\u2013106 (2004)","journal-title":"J. Logic Algebr. Program."},{"key":"18_CR16","unstructured":"Pariente, D., Ledinot, E.: Formal verification of industrial C code using Frama-C: a case study. In: Proceedings of the 1st International Conference on FoVeOOS, p. 205 (2010)"},{"key":"18_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"164","DOI":"10.1007\/978-3-540-24732-6_13","volume-title":"Model Checking Software","author":"CS P\u0103s\u0103reanu","year":"2004","unstructured":"P\u0103s\u0103reanu, C.S., Visser, W.: Verification of Java programs using symbolic execution and invariant generation. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 164\u2013181. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-24732-6_13"},{"key":"18_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-319-47846-3_5","volume-title":"Formal Methods and Software Engineering","author":"D Scheurer","year":"2016","unstructured":"Scheurer, D., H\u00e4hnle, R., Bubel, R.: A general lattice model for merging symbolic execution branches. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 57\u201373. Springer, Cham (2016). doi: 10.1007\/978-3-319-47846-3_5"},{"key":"18_CR19","doi-asserted-by":"crossref","unstructured":"Steinh\u00f6fel, D., Wasser, N.: A new invariant rule for the analysis of loops with non-standard control flows. Technical report, TU Darmstadt (2017). http:\/\/tinyurl.com\/loop-scopes-tr","DOI":"10.1007\/978-3-319-66845-1_18"},{"key":"18_CR20","unstructured":"Stenzel, K.: Verification of Java card programs. Ph.D. thesis, University of Augsburg, Germany (2005)"},{"issue":"3","key":"18_CR21","first-page":"1","volume":"11","author":"F Vogels","year":"2015","unstructured":"Vogels, F., Jacobs, B., et al.: Featherweight VeriFast. LMCS 11(3), 1\u201357 (2015)","journal-title":"LMCS"},{"key":"18_CR22","unstructured":"Wasser, N.: Automatic generation of specifications using verification tools. Ph.D. thesis, Technische Universit\u00e4t Darmstadt, Darmstadt, January 2016"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66845-1_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,2]],"date-time":"2019-10-02T16:51:56Z","timestamp":1570035116000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-66845-1_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319668444","9783319668451"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66845-1_18","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}