{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T01:49:26Z","timestamp":1742953766580,"version":"3.40.3"},"publisher-location":"Cham","reference-count":24,"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_14","type":"book-chapter","created":{"date-parts":[[2022,7,3]],"date-time":"2022-07-03T23:03:27Z","timestamp":1656889407000},"page":"290-312","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["The Karlsruhe Java Verification Suite"],"prefix":"10.1007","author":[{"given":"Jonas","family":"Klamroth","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8560-6324","authenticated-orcid":false,"given":"Florian","family":"Lanzinger","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9478-9641","authenticated-orcid":false,"given":"Wolfram","family":"Pfeifer","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2350-1831","authenticated-orcid":false,"given":"Mattias","family":"Ulbrich","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,7,4]]},"reference":[{"key":"14_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 - From Theory to Practice","year":"2016","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, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-030-61362-4_4","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles","author":"B Beckert","year":"2020","unstructured":"Beckert, B., Kirsten, M., Klamroth, J., Ulbrich, M.: Modular verification of JML contracts using bounded model checking. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12476, pp. 60\u201380. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_4"},{"key":"14_CR3","series-title":"Texts in Theoretical Computer Science. An EATCS Series","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development - Coq\u2019Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series, Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-662-07964-5"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/978-3-030-61362-4_8","volume-title":"Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles","author":"D Beyer","year":"2020","unstructured":"Beyer, D., Wehrheim, H.: Verification artifacts in cooperative verification: survey and unifying component framework. In: Margaria, T., Steffen, B. (eds.) ISoLA 2020. LNCS, vol. 12476, pp. 143\u2013167. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-61362-4_8"},{"key":"14_CR6","doi-asserted-by":"publisher","unstructured":"Bingmann, T., Marianczuk, J., Sanders, P.: Engineering faster sorters for small sets of items. Softw. Pract. Exp. 51(5), 965\u20131004 (2021). https:\/\/doi.org\/10.1002\/spe.2922. https:\/\/onlinelibrary.wiley.com\/doi\/abs\/10.1002\/spe.2922","DOI":"10.1002\/spe.2922"},{"key":"14_CR7","unstructured":"Bracha, G.: Pluggable type systems. In: OOPSLA 2004 Workshop on Revival of Dynamic Languages, October 2004"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"472","DOI":"10.1007\/978-3-642-20398-5_35","volume-title":"NASA Formal Methods","author":"DR Cok","year":"2011","unstructured":"Cok, D.R.: OpenJML: JML for Java 7 by extending OpenJDK. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 472\u2013479. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_35"},{"key":"14_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-319-96145-3_10","volume-title":"Computer Aided Verification","author":"L Cordeiro","year":"2018","unstructured":"Cordeiro, L., Kesseli, P., Kroening, D., Schrammel, P., Trtik, M.: JBMC: a bounded model checking tool for verifying java bytecode. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 183\u2013190. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_10"},{"key":"14_CR10","doi-asserted-by":"publisher","unstructured":"Dietl, W., Dietzel, S., Ernst, M.D., Muslu, K., Schiller, T.: Building and using pluggable type-checkers. In: Proceedings of the 33rd International Conference on Software Engineering, ICSE 2011, pp. 681\u2013690. Association for Computing Machinery (2011). https:\/\/doi.org\/10.1145\/1985793.1985889","DOI":"10.1145\/1985793.1985889"},{"issue":"1\u20133","key":"14_CR11","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"MD Ernst","year":"2007","unstructured":"Ernst, M.D., et al.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program. 69(1\u20133), 35\u201345 (2007). https:\/\/doi.org\/10.1016\/j.scico.2007.01.015","journal-title":"Sci. Comput. Program."},{"key":"14_CR12","doi-asserted-by":"publisher","unstructured":"Freeman, T., Pfenning, F.: Refinement types for ML. In: Proceedings of the ACM SIGPLAN 1991 Conference on Programming Language Design and Implementation, PLDI 1991, pp. 268\u2013277. Association for Computing Machinery, New York (1991). https:\/\/doi.org\/10.1145\/113445.113468","DOI":"10.1145\/113445.113468"},{"key":"14_CR13","unstructured":"Gamboa, C., Santos, P.A., Timperley, C.S., Fonseca, A.: User-driven design and evaluation of liquid types in Java. CoRR abs\/2110.05444 (2021). https:\/\/arxiv.org\/abs\/2110.05444"},{"key":"14_CR14","doi-asserted-by":"publisher","unstructured":"Jakobs, M.-C.: PART$$_{\\rm PW}$$: from partial analysis results to a proof witness. In: Cimatti, A., Sirjani, M. (eds.) SEFM 2017. LNCS, vol. 10469, pp. 120\u2013135. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66197-1_8","DOI":"10.1007\/978-3-319-66197-1_8"},{"key":"14_CR15","doi-asserted-by":"publisher","unstructured":"Jung, R., Jourdan, J.H., Krebbers, R., Dreyer, D.: RustBelt: securing the foundations of the Rust programming language. Proc. ACM Program. Lang. 2(POPL), 1\u201334 (2017). https:\/\/doi.org\/10.1145\/3158154","DOI":"10.1145\/3158154"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/11813040_19","volume-title":"FM 2006: Formal Methods","author":"IT Kassios","year":"2006","unstructured":"Kassios, I.T.: Dynamic frames: support for framing, dependencies and sharing without restrictions. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 268\u2013283. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11813040_19"},{"key":"14_CR17","doi-asserted-by":"publisher","unstructured":"Knowles, K., Flanagan, C.: Hybrid type checking. ACM Trans. Program. Lang. Syst. 32(2), 1\u201334 (2010). https:\/\/doi.org\/10.1145\/1667048.1667051","DOI":"10.1145\/1667048.1667051"},{"key":"14_CR18","doi-asserted-by":"publisher","unstructured":"Lanzinger, F., Weigl, A., Ulbrich, M., Dietl, W.: Scalability and precision by combining expressive type systems and deductive verification. Proc. ACM Program. Lang. 5(OOPSLA), Article no: 143 (2021). https:\/\/doi.org\/10.1145\/3485520","DOI":"10.1145\/3485520"},{"key":"14_CR19","unstructured":"Leavens, G.T., et al.: JML Reference Manual, May 2013. http:\/\/www.eecs.ucf.edu\/~leavens\/JML\/\/refman\/jmlrefman.pdf. Revision 2344"},{"key":"14_CR20","doi-asserted-by":"publisher","unstructured":"Mccarthy, J.: Towards a mathematical science of computation. In: In IFIP Congress, pp. 21\u201328. North-Holland (1962). https:\/\/doi.org\/10.1007\/978-94-011-1793-7_2","DOI":"10.1007\/978-94-011-1793-7_2"},{"issue":"10","key":"14_CR21","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1109\/2.161279","volume":"25","author":"B Meyer","year":"1992","unstructured":"Meyer, B.: Applying \u201cdesign by contract\u2019\u2019. Computer 25(10), 40\u201351 (1992). https:\/\/doi.org\/10.1109\/2.161279","journal-title":"Computer"},{"key":"14_CR22","doi-asserted-by":"publisher","unstructured":"Papi, M.M., Ali, M., Correa Jr., T.L., Perkins, J.H., Ernst, M.D.: Practical pluggable types for Java. In: International Symposium on Software Testing and Analysis, ISSTA, pp. 201\u2013212. ACM, Association for Computing Machinery (2008). https:\/\/doi.org\/10.1145\/1390630.1390656","DOI":"10.1145\/1390630.1390656"},{"key":"14_CR23","doi-asserted-by":"publisher","unstructured":"Vazou, N., Seidel, E.L., Jhala, R., Vytiniotis, D., Peyton Jones, S.: Refinement types for Haskell. In: Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, ICFP 2014, pp. 269\u2013282. Association for Computing Machinery, September 2014. https:\/\/doi.org\/10.1145\/2628136.2628161","DOI":"10.1145\/2628136.2628161"},{"key":"14_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-642-18070-5_13","volume-title":"Formal Verification of Object-Oriented Software","author":"DM Zimmerman","year":"2011","unstructured":"Zimmerman, D.M., Nagmoti, R.: JMLUnit: the next generation. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 183\u2013197. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18070-5_13"}],"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_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,3]],"date-time":"2022-07-03T23:39:22Z","timestamp":1656891562000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-08166-8_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031081651","9783031081668"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-08166-8_14","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"}}]}}