{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,6]],"date-time":"2026-02-06T00:18:43Z","timestamp":1770337123112,"version":"3.49.0"},"publisher-location":"Cham","reference-count":64,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711763","type":"print"},{"value":"9783031711770","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>The KeY tool is a state-of-the-art deductive program verifier for the Java language. Its verification engine is based on a sequent calculus for dynamic logic, realizing forward symbolic execution of the target program, whereby all symbolic paths through a program are explored. Method contracts make verification scalable. KeY combines auto-active and fine-grained proof interaction, which is possible both at the level of the verification target and its specification, as well as at the level of proof rules and program logic. This makes KeY well-suited for teaching program verification, but also permits proof debugging at the source code level. The latter made it possible to verify some of the most complex Java code to date. The article provides a self-contained introduction to the working principles and the practical usage of KeY for anyone with basic knowledge in logic and formal methods.<\/jats:p>","DOI":"10.1007\/978-3-031-71177-0_32","type":"book-chapter","created":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:10:51Z","timestamp":1726121451000},"page":"597-623","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["The Java Verification Tool KeY:A Tutorial"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9672-3291","authenticated-orcid":false,"given":"Bernhard","family":"Beckert","sequence":"first","affiliation":[]},{"given":"Richard","family":"Bubel","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3036-8220","authenticated-orcid":false,"given":"Daniel","family":"Drodt","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8000-7613","authenticated-orcid":false,"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","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":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8446-4598","authenticated-orcid":false,"given":"Alexander","family":"Weigl","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,9,13]]},"reference":[{"key":"32_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/978-3-030-72013-1_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Abbasi","year":"2021","unstructured":"Abbasi, R., Schiffl, J., Darulova, E., Ulbrich, M., Ahrendt, W.: Deductive verification of floating-point java programs in KeY. In: TACAS 2021. LNCS, vol. 12652, pp. 242\u2013261. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72013-1_13"},{"key":"32_CR2","doi-asserted-by":"crossref","unstructured":"Abrial, J.R.: The B\u00a0Book: Assigning Programs to Meanings. Cambridge University Press (1996)","DOI":"10.1017\/CBO9780511624162"},{"issue":"1","key":"32_CR3","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/s10270-004-0058-x","volume":"4","author":"W Ahrendt","year":"2005","unstructured":"Ahrendt, W., et al.: The KeY tool: integrating object oriented design and formal verification. Software and System Modeling 4(1), 32\u201354 (2005). https:\/\/doi.org\/10.1007\/s10270-004-0058-x","journal-title":"Software and System Modeling"},{"key":"32_CR4","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification \u2013 The KeY Book: From Theory to Practice. No. 10001 in LNCS, Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"32_CR5","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Ulbrich, M. (eds.): Deductive Software Verification: Future Perspectives. No. 12345 in LNCS, Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-64354-6","DOI":"10.1007\/978-3-030-64354-6"},{"key":"32_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-319-49812-6_12","volume-title":"Deductive Software Verification \u2013 The KeY Book","author":"W Ahrendt","year":"2016","unstructured":"Ahrendt, W., Gladisch, C., Herda, M.: Proof-based test case generation. In: Deductive Software Verification \u2013 The KeY Book. LNCS, vol. 10001, pp. 415\u2013451. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6_12"},{"key":"32_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-319-49812-6_15","volume-title":"Deductive Software Verification \u2013 The KeY Book","author":"W Ahrendt","year":"2016","unstructured":"Ahrendt, W., Grebing, S.: Using the KeY prover. In: Deductive Software Verification \u2013 The KeY Book. LNCS, vol. 10001, pp. 495\u2013539. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6_15"},{"key":"32_CR8","doi-asserted-by":"publisher","unstructured":"Axtmann, M., Witt, S., Ferizovic, D., Sanders, P.: Engineering in-place (shared-memory) sorting algorithms. Comput. Res. Repository (CoRR) abs\/2009.13569 (2020). https:\/\/doi.org\/10.48550\/arXiv.2009.13569","DOI":"10.48550\/arXiv.2009.13569"},{"issue":"3","key":"32_CR9","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1145\/3182657","volume":"51","author":"R Baldoni","year":"2018","unstructured":"Baldoni, R., Coppa, E., D\u2019elia, D.C., Demetrescu, C., Finocchi, I.: A survey of symbolic execution techniques. ACM Comput. Surv. (CSUR) 51(3), 50 (2018). https:\/\/doi.org\/10.1145\/3182657","journal-title":"ACM Comput. Surv. (CSUR)"},{"key":"32_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/978-3-030-99524-9_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H Barbosa","year":"2022","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24"},{"key":"32_CR11","first-page":"364","volume-title":"FMCO","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: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.P. (eds.) FMCO, pp. 364\u2013387. Springer, Berlin, Heidelberg (2006)"},{"key":"32_CR12","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The satisfiability modulo theories library (SMT-LIB) (2016). www.SMT-LIB.org"},{"key":"32_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"541","DOI":"10.1007\/978-3-319-49812-6_16","volume-title":"Deductive Software Verification \u2013 The KeY Book","author":"B Beckert","year":"2016","unstructured":"Beckert, B., H\u00e4hnle, R., Hentschel, M., Schmitt, P.H.: Formal verification with KeY: a tutorial. In: Deductive Software Verification \u2013 The KeY Book. LNCS, vol. 10001, pp. 541\u2013570. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6_16"},{"key":"32_CR14","doi-asserted-by":"publisher","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P. (eds.): Verification of Object-Oriented Software The KeY Approach. No. 4334 in LNCS, Springer (2006). https:\/\/doi.org\/10.1007\/978-3-540-69061-0","DOI":"10.1007\/978-3-540-69061-0"},{"key":"32_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69061-0","volume-title":"Verification of Object-Oriented Software. The KeY Approach","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. The KeY Approach. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-69061-0"},{"key":"32_CR16","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":"32_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-319-49812-6_3","volume-title":"Deductive Software Verification \u2013 The KeY Book","author":"B Beckert","year":"2016","unstructured":"Beckert, B., Klebanov, V., Wei\u00df, B.: Dynamic logic for Java. In: Deductive Software Verification \u2013 The KeY Book. LNCS, vol. 10001, pp. 49\u2013106. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6_3"},{"key":"32_CR18","doi-asserted-by":"publisher","unstructured":"Beckert, B., Sanders, P., Ulbrich, M.: Formally verifying an efficient sorter. In: Finkbeiner, B., Kov\u00e1cs, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference TACAS, Luxembourg City, Luxembourg. LNCS, Springer, Cham (2024). https:\/\/doi.org\/10.1007\/978-3-031-57246-3_15","DOI":"10.1007\/978-3-031-57246-3_15"},{"key":"32_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/978-3-319-72308-2_3","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"B Beckert","year":"2017","unstructured":"Beckert, B., Schiffl, J., Schmitt, P.H., Ulbrich, M.: Proving JDK\u2019s dual pivot quicksort correct. In: Paskevich, A., Wies, T. (eds.) VSTTE 2017. LNCS, vol. 10712, pp. 35\u201348. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-72308-2_3"},{"key":"32_CR20","doi-asserted-by":"publisher","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development \u2013 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","DOI":"10.1007\/978-3-662-07964-5"},{"key":"32_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"102","DOI":"10.1007\/978-3-319-66845-1_7","volume-title":"Integrated Formal Methods","author":"S Blom","year":"2017","unstructured":"Blom, S., Darabi, S., Huisman, M., Oortwijn, W.: The VerCors tool set: verification of parallel and concurrent software. In: Polikarpova, N., Schneider, S. (eds.) IFM 2017. LNCS, vol. 10510, pp. 102\u2013110. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66845-1_7"},{"key":"32_CR22","unstructured":"Bobot, F., Filli\u00e2tre, J.C., March\u00e9, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, pp. 53\u201364. Wroc\u0142aw, Poland (2011)"},{"key":"32_CR23","doi-asserted-by":"publisher","unstructured":"de\u00a0Boer, F.S., Hiep, H.A.: Completeness and complexity of reasoning about call-by-value in Hoare logic. ACM Trans. Prog. Lang. Syst. 43(4), 17:1\u201317:35 (2021). https:\/\/doi.org\/10.1145\/3477143","DOI":"10.1145\/3477143"},{"key":"32_CR24","doi-asserted-by":"publisher","unstructured":"de\u00a0Boer, M., de\u00a0Gouw, S., Klamroth, J., Jung, C., Ulbrich, M., Weigl, A.: Formal specification and verification of JDK\u2019s identity hash map implementation. In: ter Beek, M.H., Monahan, R. (eds.) Integrated Formal Methods, pp. 45\u201362. no. 13274 in LNCS, Springer International Publishing, Cham (2022).https:\/\/doi.org\/10.1007\/978-3-031-07727-2_4","DOI":"10.1007\/978-3-031-07727-2_4"},{"key":"32_CR25","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":"32_CR26","doi-asserted-by":"crossref","unstructured":"Cok, D.R.: OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse. In: Dubois, C., Giannakopoulou, D., M\u00e9ry, D. (eds.) 1st Workshop on Formal Integrated Development Environment, F-IDE, Grenoble, France, pp. 79\u201392. No.\u00a0149 in EPTCS (2014)","DOI":"10.4204\/EPTCS.149.8"},{"key":"32_CR27","doi-asserted-by":"crossref","unstructured":"Dahlweid, M., Moskal, M., Santen, T., Tobies, S., Schulte, W.: VCC: Contract-based modular verification of concurrent C. In: International Conference on Software Engineering \u2013 Companion Volume, pp. 429\u2013430 (2009)","DOI":"10.1109\/ICSE-COMPANION.2009.5071046"},{"key":"32_CR28","doi-asserted-by":"crossref","unstructured":"De\u00a0Gouw, S., De\u00a0Boer, F.S., Bubel, R., H\u00e4hnle, R., Rot, J., Steinh\u00f6fel, D.: Verifying OpenJDK\u2019s sort method for generic collections. J. Automated Reasoning 62(6), 93\u2013126 (2019)","DOI":"10.1007\/s10817-017-9426-4"},{"key":"32_CR29","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 de Gouw","year":"2015","unstructured":"de Gouw, S., Rot, J., de 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). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_16"},{"key":"32_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"issue":"8","key":"32_CR31","doi-asserted-by":"publisher","first-page":"5","DOI":"10.5381\/JOT.2005.4.8.A1","volume":"4","author":"W Dietl","year":"2005","unstructured":"Dietl, W., M\u00fcller, P.: Universes: lightweight ownership for JML. J. Object Technol. 4(8), 5\u201332 (2005). https:\/\/doi.org\/10.5381\/JOT.2005.4.8.A1","journal-title":"J. Object Technol."},{"key":"32_CR32","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall (1976)"},{"key":"32_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-Order Logic and Automated Theorem Proving","author":"MC Fitting","year":"1996","unstructured":"Fitting, M.C.: First-Order Logic and Automated Theorem Proving, 2nd edn. Springer-Verlag, New York (1996). https:\/\/doi.org\/10.1007\/978-1-4612-2360-3","edition":"2"},{"key":"32_CR34","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"527","DOI":"10.1007\/978-3-319-21401-6_36","volume-title":"Automated Deduction - CADE-25","author":"N Fulton","year":"2015","unstructured":"Fulton, N., Mitsch, S., Quesel, J.-D., V\u00f6lp, M., Platzer, A.: KeYmaera\u00a0X: an axiomatic tactical theorem prover for hybrid systems. In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 527\u2013538. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_36"},{"key":"32_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-319-49812-6_9","volume-title":"Deductive Software Verification \u2013 The KeY Book","author":"D Grahl","year":"2016","unstructured":"Grahl, D., Bubel, R., Mostowski, W., Schmitt, P.H., Ulbrich, M., Wei\u00df, B.: Modular specification and verification. In: Deductive Software Verification \u2013 The KeY Book. LNCS, vol. 10001, pp. 289\u2013351. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6_9"},{"key":"32_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-319-49812-6_8","volume-title":"Deductive Software Verification \u2013 The KeY Book","author":"D Grahl","year":"2016","unstructured":"Grahl, D., Ulbrich, M.: From specification to proof obligations. In: Deductive Software Verification \u2013 The KeY Book. LNCS, vol. 10001, pp. 243\u2013287. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6_8"},{"key":"32_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/978-3-319-91908-9_18","volume-title":"Computing and Software Science","author":"R H\u00e4hnle","year":"2019","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive software verification: from pen-and-paper proofs to industrial tools. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 345\u2013373. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-319-91908-9_18"},{"key":"32_CR38","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D Harel","year":"2000","unstructured":"Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press (Oct, Foundations of Computing (2000)"},{"key":"32_CR39","doi-asserted-by":"publisher","unstructured":"Harel, D., Meyer, A.R., Pratt, V.R.: Computability and completeness in logics of programs (preliminary report). In: Hopcroft, J.E., Friedman, E.P., Harrison, M.A. (eds.) Proceedings of the 9th Annual ACM Symposium on Theory of Computing, Boulder, CO, USA, pp. 261\u2013268. ACM, New York, NY (1977). https:\/\/doi.org\/10.1145\/800105.803416","DOI":"10.1145\/800105.803416"},{"key":"32_CR40","doi-asserted-by":"publisher","unstructured":"Hentschel, M., Bubel, R., H\u00e4hnle, R.: Symbolic execution debugger (SED). In: Bonakdarpour, B., Smolka, S.A. (eds.) Runtime Verification, 14th International Conference, RV, Toronto, Canada, pp. 255\u2013262. No.\u00a08734 in LNCS, Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-11164-3_21","DOI":"10.1007\/978-3-319-11164-3_21"},{"issue":"5","key":"32_CR41","doi-asserted-by":"publisher","first-page":"485","DOI":"10.1007\/s10009-018-0490-9","volume":"21","author":"M Hentschel","year":"2018","unstructured":"Hentschel, M., Bubel, R., H\u00e4hnle, R.: The Symbolic Execution Debugger (SED): a platform for interactive symbolic execution, debugging verification and More. STTT 21(5), 485\u2013513 (2018)","journal-title":"STTT"},{"key":"32_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/978-3-030-45237-7_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"H-DA Hiep","year":"2020","unstructured":"Hiep, H.-D.A., Maathuis, O., Bian, J., de Boer, F.S., van Eekelen, M., de Gouw, S.: Verifying OpenJDK\u2019s LinkedList using key. In: TACAS 2020. LNCS, vol. 12079, pp. 217\u2013234. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-45237-7_13"},{"key":"32_CR43","doi-asserted-by":"crossref","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Comm. ACM 12(10), 576\u2013580, 583 (1969)","DOI":"10.1145\/363235.363259"},{"key":"32_CR44","unstructured":"Jacobs, B., Piessens, F.: The VeriFast program verifier. Technical Report CW-520, Department of Computer Science, Katholieke Universiteit Leuven (2008). http:\/\/www.cs.kuleuven.be\/~bartj\/verifast\/verifast.pdf"},{"key":"32_CR45","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"},{"issue":"3","key":"32_CR46","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/S00165-010-0152-5","volume":"23","author":"IT Kassios","year":"2011","unstructured":"Kassios, I.T.: The dynamic frames theory. Formal Aspects Comput. 23(3), 267\u2013288 (2011). https:\/\/doi.org\/10.1007\/S00165-010-0152-5","journal-title":"Formal Aspects Comput."},{"issue":"3","key":"32_CR47","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/s00165-014-0326-7","volume":"27","author":"F Kirchner","year":"2015","unstructured":"Kirchner, F., Kosmatov, N., Prevosto, V., Signoles, J., Yakobowski, B.: Frama-C: a software analysis perspective. Formal Aspects Comput. 27(3), 573\u2013609 (2015)","journal-title":"Formal Aspects Comput."},{"key":"32_CR48","unstructured":"Leavens, G.T., et al.: JML reference manual (2013). http:\/\/www.eecs.ucf.edu\/~leavens\/JML\/\/OldReleases\/jmlrefman.pdf, draft revision 2344"},{"key":"32_CR49","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"348","DOI":"10.1007\/978-3-642-17511-4_20","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348\u2013370. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20"},{"key":"32_CR50","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., W\u00fcstholz, V.: The Dafny integrated development environment. In: F-IDE 2014, pp. 3\u201315. No.\u00a0149 in EPTCS (2014)","DOI":"10.4204\/EPTCS.149.2"},{"key":"32_CR51","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1007\/978-3-030-71500-7_8","volume-title":"Fundamental Approaches to Software Engineering","author":"C Lidstr\u00f6m","year":"2021","unstructured":"Lidstr\u00f6m, C., Gurov, D.: An abstract contract theory for programs with procedures. In: FASE 2021. LNCS, vol. 12649, pp. 152\u2013171. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-71500-7_8"},{"key":"32_CR52","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: 2nd IFIP Congress, pp. 21\u201328. North-Holland (1962)"},{"key":"32_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"32_CR54","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-540-71070-7_15","volume-title":"Automated Reasoning","author":"A Platzer","year":"2008","unstructured":"Platzer, A., Quesel, J.-D.: KeYmaera: a hybrid theorem prover for hybrid systems (system description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 171\u2013178. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_15"},{"key":"32_CR55","doi-asserted-by":"publisher","unstructured":"Pratt, V.R.: Semantical considerations on Floyd-Hoare logic. In: 17th Annual Symposium on Foundations of Computer Science, Houston, TX, USA, pp. 109\u2013121. IEEE Computer Society, Los Alamitos, CA (1976).https:\/\/doi.org\/10.1109\/SFCS.1976.27","DOI":"10.1109\/SFCS.1976.27"},{"key":"32_CR56","doi-asserted-by":"publisher","unstructured":"Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: Symposium on Logic in Computer Science (LICS) 2002, pp. 55\u201374. IEEE Computer Society (2002).https:\/\/doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"32_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-319-49812-6_4","volume-title":"Deductive Software Verification \u2013 The KeY Book","author":"P R\u00fcmmer","year":"2016","unstructured":"R\u00fcmmer, P., Ulbrich, M.: Proof search with taclets. In: Deductive Software Verification \u2013 The KeY Book. LNCS, vol. 10001, pp. 107\u2013147. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6_4"},{"key":"32_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1007\/978-3-030-16722-6_2","volume-title":"Fundamental Approaches to Software Engineering","author":"T Runge","year":"2019","unstructured":"Runge, T., Schaefer, I., Cleophas, L., Th\u00fcm, T., Kourie, D., Watson, B.W.: Tool support for correctness-by-construction. In: H\u00e4hnle, R., van der Aalst, W. (eds.) FASE 2019. LNCS, vol. 11424, pp. 25\u201342. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-16722-6_2"},{"key":"32_CR59","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-319-49812-6_2","volume-title":"Deductive Software Verification \u2013 The KeY Book","author":"PH Schmitt","year":"2016","unstructured":"Schmitt, P.H.: First-order logic. In: Deductive Software Verification \u2013 The KeY Book. LNCS, vol. 10001, pp. 23\u201347. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6_2"},{"key":"32_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/978-3-642-18070-5_10","volume-title":"Formal Verification of Object-Oriented Software","author":"PH Schmitt","year":"2011","unstructured":"Schmitt, P.H., Ulbrich, M., Wei\u00df, B.: Dynamic frames in java dynamic logic. In: Beckert, B., March\u00e9, C. (eds.) FoVeOOS 2010. LNCS, vol. 6528, pp. 138\u2013152. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-18070-5_10"},{"key":"32_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/978-3-030-64437-6_16","volume-title":"Programming Languages and Systems","author":"D Steinh\u00f6fel","year":"2020","unstructured":"Steinh\u00f6fel, D.: REFINITY to model and prove program transformation rules. In: Oliveira, B.C.S. (ed.) APLAS 2020. LNCS, vol. 12470, pp. 311\u2013319. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-64437-6_16"},{"key":"32_CR62","doi-asserted-by":"crossref","unstructured":"Steinh\u00f6fel, D., H\u00e4hnle, R.: Schematic program proofs with abstract execution: theory and applications. J. Autom. Reason. 68(7), 7:1\u20137:57 (2024)","DOI":"10.1007\/s10817-023-09692-0"},{"key":"32_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1007\/978-3-662-46681-0_53","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Tschannen","year":"2015","unstructured":"Tschannen, J., Furia, C.A., Nordio, M., Polikarpova, N.: AutoProof: auto-active functional verification of object-oriented programs. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 566\u2013580. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46681-0_53"},{"key":"32_CR64","unstructured":"Tuerk, T.: Local reasoning about while-loops. In: VSTTE Theory Workshop (VS-Theory) (2012)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71177-0_32","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:15:34Z","timestamp":1726121734000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71177-0_32"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,13]]},"ISBN":["9783031711763","9783031711770"],"references-count":64,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71177-0_32","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,13]]},"assertion":[{"value":"13 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}