{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T18:29:45Z","timestamp":1743100185755,"version":"3.40.3"},"publisher-location":"Cham","reference-count":148,"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_15","type":"book-chapter","created":{"date-parts":[[2022,7,3]],"date-time":"2022-07-03T23:03:27Z","timestamp":1656889407000},"page":"313-349","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Further Lessons from\u00a0the\u00a0JML Project"],"prefix":"10.1007","author":[{"given":"Gary T.","family":"Leavens","sequence":"first","affiliation":[]},{"given":"David R.","family":"Cok","sequence":"additional","affiliation":[]},{"given":"Amirfarhad","family":"Nilizadeh","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,7,4]]},"reference":[{"key":"15_CR1","unstructured":"Ahrendt, W.: The Java Modeling Language - a basis for static and dynamic verification, June 2018. https:\/\/youtu.be\/9ItK0jxJ0oQ"},{"key":"15_CR2","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., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M. (eds.): Deductive Software Verification - The KeY Book. LNCS, vol. 10001. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6"},{"key":"15_CR3","doi-asserted-by":"publisher","unstructured":"Banerjee, A., Naumann, D.A.: Local reasoning for global invariants, part ii: dynamic boundaries. J. ACM 60(3), 19:1\u201319:73 (2013). https:\/\/doi.org\/10.1145\/2485981. http:\/\/doi.acm.org\/10.1145\/2485981","DOI":"10.1145\/2485981"},{"key":"15_CR4","doi-asserted-by":"publisher","unstructured":"Banerjee, A., Naumann, D.A., Rosenberg, S.: Local reasoning for global invariants, part i: region logic. J. ACM 60(3), 18:1\u201318:56 (2013). https:\/\/doi.org\/10.1145\/2485982. http:\/\/doi.acm.org\/10.1145\/2485982","DOI":"10.1145\/2485982"},{"key":"15_CR5","unstructured":"Bao, Y.: Reasoning about frame properties in object-oriented programs. Technical report, CS-TR-17-05, Computer Science, University of Central Florida, Orlando, Florida, December 2017. The author\u2019s dissertation. https:\/\/goo.gl\/WZGMiB"},{"key":"15_CR6","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-319-98047-8_2","volume-title":"Principled Software Development","author":"Y Bao","year":"2018","unstructured":"Bao, Y., Leavens, G.T.: A methodology for invariants, framing, and subtyping in JML. In: M\u00fcller, P., Schaefer, I. (eds.) Principled Software Development, pp. 19\u201339. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-98047-8_2"},{"key":"15_CR7","doi-asserted-by":"publisher","unstructured":"Bao, Y., Leavens, G.T., Ernst, G.: Unifying separation logic and region logic to allow interoperability. Form. Asp. Comput. 30, 381\u2013441 (2018). https:\/\/doi.org\/10.1007\/s00165-018-0455-5","DOI":"10.1007\/s00165-018-0455-5"},{"key":"15_CR8","unstructured":"Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison Wesley, New York (2003)"},{"key":"15_CR9","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: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2005. LNCS, vol. 4111, pp. 364\u2013387. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11804192_17"},{"key":"15_CR10","doi-asserted-by":"crossref","unstructured":"Barnett, M., DeLine, R., F\u00e4hndrich, M., Leino, K.R.M., Schulte, W.: Verification of object-oriented programs with invariants. J. Object Technol. 3(6), 27\u201356 (2004). http:\/\/tinyurl.com\/m2a8j","DOI":"10.5381\/jot.2004.3.6.a2"},{"key":"15_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49\u201369. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30569-9_3"},{"issue":"3","key":"15_CR12","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1007\/BF00264250","volume":"21","author":"H Barringer","year":"1984","unstructured":"Barringer, H., Cheng, J.H., Jones, C.B.: A logic covering undefinedness in program proofs. Acta Informatica 21(3), 251\u2013269 (1984)","journal-title":"Acta Informatica"},{"key":"15_CR13","unstructured":"Baudin, P., et al.: ACSL: ANSI C Specification Language (2008ff). http:\/\/frama-c.com\/download\/acsl_1.4.pdf"},{"key":"15_CR14","doi-asserted-by":"publisher","unstructured":"Baudin, P., et al.: The dogged pursuit of bug-free C programs: the Frama-C software analysis platform. Commun. ACM 64(8), 56\u201368 (2021). https:\/\/doi.org\/10.1145\/3470569","DOI":"10.1145\/3470569"},{"key":"15_CR15","unstructured":"Beckert, B.: A dynamic logic for Java Card. In: Drossopoulou, S., Eisenbach, S., Jacobs, B., Leavens, G.T., M\u00fcller, P., Poetzsch-Heffter, A. (eds.) Workshop on Formal Techniques for Java Programs (FTfJP). Technical report 269, Fernuniversit\u00e4t Hagen (2000)"},{"key":"15_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69061-0","volume-title":"Verification of Object-Oriented Software: The KeY Approach","author":"B Beckert","year":"2007","unstructured":"Beckert, B., H\u00e4hnle, R., Schmitt, P.H.: Verification of Object-Oriented Software: The KeY Approach. LNCS, vol. 4334. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-69061-0"},{"key":"15_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/3-540-45319-9_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J van den Berg","year":"2001","unstructured":"van den Berg, J., Jacobs, B.: The loop compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 299\u2013312. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45319-9_21"},{"key":"15_CR18","unstructured":"van den Berg, J., Poll, E., Jacobs, B.: First steps in formalising JML: exceptions in predicates. In: Drossopoulou, S., Eisenbach, S., Jacobs, B., Leavens, G.T., M\u00fcller, P., Poetzsch-Heffter, A. (eds.) Formal Techniques for Java Programs. Proceedings of the ECOOP\u201900 Workshop. Technical report, Fernuniversit\u00e4t Hagen (2000). http:\/\/www.cs.ru.nl\/~erikpoll\/publications\/ftfjp00.ps.gz"},{"key":"15_CR19","doi-asserted-by":"crossref","unstructured":"Blanc, R., Kuncak, V., Kneuss, E., Suter, P.: An overview of the leon verification system: verification by translation to recursive functions. In: Proceedings of the 4th Workshop on Scala. SCALA 2013. Association for Computing Machinery, New York (2013). https:\/\/doi.org\/10.1145\/2489837.2489838","DOI":"10.1145\/2489837.2489838"},{"key":"15_CR20","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). https:\/\/hal.inria.fr\/hal-00790310"},{"key":"15_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-319-98938-9_3","volume-title":"Integrated Formal Methods","author":"J Boerman","year":"2018","unstructured":"Boerman, J., Huisman, M., Joosten, S.: Reasoning about JML: differences between KeY and OpenJML. In: Furia, C.A., Winter, K. (eds.) IFM 2018. LNCS, vol. 11023, pp. 30\u201346. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-98938-9_3"},{"key":"15_CR22","doi-asserted-by":"crossref","unstructured":"Borgida, A., Mylopoulos, J., Reiter, R.: On the frame problem in procedure specifications. IEEE Trans. Softw. Eng. 21(10), 785\u2013798 (1995). http:\/\/doi.ieeecomputersociety.org\/10.1109\/32.469460","DOI":"10.1109\/32.469460"},{"key":"15_CR23","unstructured":"Breunesse, C.B., Poll, E.: Verifying JML specifications with model fields. In: Formal Techniques for Java-like Programs (FTfJP), pp. 51\u201360. No. 408 in Technical report, ETH Zurich, July 2003. http:\/\/www.cs.ru.nl\/~erikpoll\/publications\/ftfjp03.pdf"},{"key":"15_CR24","unstructured":"B\u00fcchi, M., Weck, W.: A plea for grey-box components. In: Leavens, G.T., Sitaraman, M. (eds.) Foundations of Component-Based Systems Workshop. University of Central Florida (1997). https:\/\/www.cs.ucf.edu\/~leavens\/FoCBS\/buechi.html"},{"key":"15_CR25","unstructured":"Burdy, L., et al.: An overview of JML tools and applications. In: Arts, T., Fokkink, W. (eds.) Eighth International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2003). Electronic Notes in Theoretical Computer Science (ENTCS), vol. 80, pp. 73\u201389. Elsevier (2003). http:\/\/www.sciencedirect.com\/science\/journal\/15710661"},{"key":"15_CR26","unstructured":"Chalin, P.: Back to basics: language support and semantics of basic infinite integer types in JML and Larch. Technical report, CU-CS 2002\u2013003.1, Computer Science Department, Concordia University (2002). http:\/\/www.cs.concordia.ca\/~faculty\/chalin\/papers\/TR-CU-CS-2002-003.1.pdf"},{"key":"15_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"440","DOI":"10.1007\/978-3-540-45236-2_25","volume-title":"FME 2003: Formal Methods","author":"P Chalin","year":"2003","unstructured":"Chalin, P.: Improving JML: for a safer and more effective language. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 440\u2013461. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_25http:\/\/www.springerlink.com\/content\/26cpmd9b3vbgd2et"},{"key":"15_CR28","doi-asserted-by":"crossref","unstructured":"Chalin, P.: Logical foundations of program assertions: What do practitioners want? In: Proceedings of the 3rd International Conference on Software Engineering and Formal Method (SEFM). IEEE Computer Society, Los Alamitos, California (2005). http:\/\/www.cs.concordia.ca\/~chalin\/papers\/TR-2005-002-r2.pdf","DOI":"10.1109\/SEFM.2005.26"},{"key":"15_CR29","unstructured":"Chalin, P.: Towards support for non-null types and non-null-by default in Java. In: Workshop on Formal Techniques for Java-like Programs (FTfJP) (2006). http:\/\/www.disi.unige.it\/person\/AnconaD\/FTfJP06\/paper03.pdf"},{"key":"15_CR30","doi-asserted-by":"crossref","unstructured":"Chalin, P.: A sound assertion semantics for the dependable systems evoluation verifying compiler. In: International Conference on Software Engineering (ICSE), Los Alamitos, California, pp. 23\u201333. IEEE, May 2007. http:\/\/dx.doi.org\/10.1109\/ICSE.2007.9","DOI":"10.1109\/ICSE.2007.9"},{"key":"15_CR31","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_16https:\/\/tinyurl.com\/3z2vk55n"},{"key":"15_CR32","doi-asserted-by":"crossref","unstructured":"Chalin, P., Rioux, F.: Non-null references by default in the Java modeling language. In: Proceedings of the Workshop on the Specification and Verification of Component-Based Systems (SAVCBS 2005). ACM Software Engineering Notes, vol. 31, no. 2. ACM (2005)","DOI":"10.1145\/1118537.1123068"},{"key":"15_CR33","first-page":"91","volume-title":"Foundations of Component-Based Systems","author":"Y Chen","year":"2000","unstructured":"Chen, Y., Cheng, B.H.C.: A semantic foundation for specification matching. In: Leavens, G.T., Sitaraman, M. (eds.) Foundations of Component-Based Systems, pp. 91\u2013109. Cambridge University Press, New York (2000)"},{"key":"15_CR34","unstructured":"Cheng, J.H., Jones, C.B.: On the usability of logics which handle partial functions. In: Morgan, C., Woodcock, J.C.P. (eds.) Proceedings of the Third Refinement Workshop. Workshops in Computing Series, pp. 51\u201369. Springer, Berlin (1991)"},{"issue":"6","key":"15_CR35","first-page":"39","volume":"7","author":"Y Cheon","year":"1994","unstructured":"Cheon, Y., Leavens, G.T.: A quick overview of Larch\/C++. J. Object-Oriented Program. 7(6), 39\u201349 (1994)","journal-title":"J. Object-Oriented Program."},{"key":"15_CR36","unstructured":"Cheon, Y., Leavens, G.T.: A runtime assertion checker for the Java modeling language (JML). In: Arabnia, H.R., Mun, Y. (eds.) Proceedings of the International Conference on Software Engineering Research and Practice (SERP 2002), Las Vegas, Nevada, USA, 24\u201327 June 2002, pp. 322\u2013328. CSREA Press (2002). ftp:\/\/ftp.cs.iastate.edu\/pub\/techreports\/TR02-05\/TR.pdf"},{"key":"15_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/3-540-47993-7_10","volume-title":"ECOOP 2002 \u2014 Object-Oriented Programming","author":"Y Cheon","year":"2002","unstructured":"Cheon, Y., Leavens, G.T.: A simple and practical approach to unit testing: the JML and JUnit way. In: Magnusson, B. (ed.) ECOOP 2002. LNCS, vol. 2374, pp. 231\u2013255. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-47993-7_10https:\/\/tinyurl.com\/4tk2nzzd"},{"key":"15_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/3-540-45337-7_4","volume-title":"ECOOP 2001 \u2014 Object-Oriented Programming","author":"DG Clarke","year":"2001","unstructured":"Clarke, D.G., Noble, J., Potter, J.M.: Simple ownership types for object containment. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 53\u201376. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45337-7_4"},{"key":"15_CR39","unstructured":"Clifton, C.: MultiJava: design, implementation, and evaluation of a Java-compatible language supporting modular open classes and symmetric multiple dispatch. Technical report, 01-10, Department of Computer Science, Iowa State University, Ames, Iowa, 50011, November 2001. ftp:\/\/ftp.cs.iastate.edu\/pub\/techreports\/TR01-10\/TR.pdf. The author\u2019s masters thesis"},{"key":"15_CR40","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":"15_CR41","unstructured":"Cok, D.R.: (2018). http:\/\/www.openjml.org"},{"key":"15_CR42","doi-asserted-by":"crossref","unstructured":"Cok, D.R.: Reasoning about functional programming in Java and C++. In: Companion Proceedings for the ISSTA\/ECOOP 2018 Workshops, ISSTA 2018, pp. 37\u201339. Association for Computing Machinery, New York (2018). https:\/\/doi.org\/10.1145\/3236454.3236483","DOI":"10.1145\/3236454.3236483"},{"key":"15_CR43","doi-asserted-by":"crossref","unstructured":"Cok, D.R.: JML and OpenJML for Java 16. In: Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs, FTfJP 2021, pp. 65\u201367. Association for Computing Machinery, New York (2021). https:\/\/doi.org\/10.1145\/3464971.3468417","DOI":"10.1145\/3464971.3468417"},{"key":"15_CR44","doi-asserted-by":"crossref","unstructured":"Cok, D.R., Kiniry, J.: ESC\/Java2: uniting ESC\/Java and JML. progress and issues in building and using ESC\/Java2 and a report on a case study involving the use of ESC\/Java2 to verify portions of an internet voting tally system, May 2004. Presented at CASSIS 2004 and submitted for publication","DOI":"10.1007\/978-3-540-30569-9_6"},{"key":"15_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-30569-9_6","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"DR Cok","year":"2005","unstructured":"Cok, D.R., Kiniry, J.R.: ESC\/Java2: uniting ESC\/Java and JML. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 108\u2013128. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-30569-9_6"},{"key":"15_CR46","unstructured":"Cok, D.R., Leavens, G.T., Ulbrich, M.: Java Modeling Language (JML) Reference Manual, 2nd edn (2022, in progress). https:\/\/www.openjml.org\/documentation\/JML_Reference_Manual.pdf"},{"key":"15_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-030-03592-1_15","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"DR Cok","year":"2018","unstructured":"Cok, D.R., Tasiran, S.: Practical methods for reasoning about java 8\u2019s functional programming features. In: Piskac, R., R\u00fcmmer, P. (eds.) VSTTE 2018. LNCS, vol. 11294, pp. 267\u2013278. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03592-1_15"},{"key":"15_CR48","doi-asserted-by":"crossref","unstructured":"Damm, W., Josko, B.: A sound and relatively complete Hoare-logic for a language with higher type procedures. Acta Informatica 20(1), 59\u2013101 (1983). http:\/\/dx.doi.org\/10.1007\/BF00264295","DOI":"10.1007\/BF00264295"},{"key":"15_CR49","unstructured":"DeLine, R., Leino, K.R.M.: BoogiePL: a typed procedural language for checking object-oriented programs. Technical report, MSR-TR-2005-70, Microsoft Research (2005). ftp:\/\/ftp.research.microsoft.com\/pub\/tr\/TR-2005-70.pdf"},{"key":"15_CR50","unstructured":"Detlefs, D.L., Leino, K.R.M., Nelson, G., Saxe, J.B.: Extended static checking. SRC Research Report 159, Compaq Systems Research Center, 130 Lytton Ave., Palo Alto, December 1998"},{"key":"15_CR51","unstructured":"Dhara, K.K., Leavens, G.T.: Forcing behavioral subtyping through specification inheritance. In: Proceedings of the 18th International Conference on Software Engineering, Berlin, Germany, pp. 258\u2013267. IEEE Computer Society Press, Los Alamitos (1996). http:\/\/doi.ieeecomputersociety.org\/10.1109\/ICSE.1996.493421. A corrected version is ISU CS TR #95-20c. http:\/\/tinyurl.com\/s2krg"},{"issue":"8","key":"15_CR52","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminancy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"key":"15_CR53","volume-title":"A Discipline of Programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall Inc, Englewood Cliffs (1976)"},{"key":"15_CR54","doi-asserted-by":"crossref","unstructured":"Dillig, I., Dillig, T., Li, B., McMillan, K.: Inductive invariant generation via abductive inference. In: Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages and Applications, OOPSLA 2013, pp. 443\u2013456. Association for Computing Machinery, New York (2013). https:\/\/doi.org\/10.1145\/2509136.2509511","DOI":"10.1145\/2509136.2509511"},{"key":"15_CR55","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/978-3-540-70592-5_18","volume-title":"ECOOP 2008 \u2013 Object-Oriented Programming","author":"S Drossopoulou","year":"2008","unstructured":"Drossopoulou, S., Francalanza, A., M\u00fcller, P., Summers, A.J.: A unified framework for verification techniques for object invariants. In: Vitek, J. (ed.) ECOOP 2008. LNCS, vol. 5142, pp. 412\u2013437. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-70592-5_18"},{"key":"15_CR56","unstructured":"Drossopoulou, S., Francalanza, A., M\u00fcller, P.: A unified framework for verification techniques for object invariants. In: International Workshop on Foundations of Object-Oriented Languages (FOOL 2008) (2008). http:\/\/fool08.kuis.kyoto-u.ac.jp\/drossopoulou.pdf"},{"issue":"1\u20133","key":"15_CR57","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1016\/j.scico.2007.02.003","volume":"69","author":"T Ekman","year":"2007","unstructured":"Ekman, T., Hedin, G.: The JastAdd system \u2013 modular extensible compiler construction. Sci. Comput. Program. 69(1\u20133), 14\u201326 (2007). https:\/\/doi.org\/10.1016\/j.scico.2007.02.003","journal-title":"Sci. Comput. Program."},{"key":"15_CR58","unstructured":"EPFL, Lausanne, Switzerland: Stainless Verification Framework (2022). https:\/\/epfl-lara.github.io\/stainless\/intro.html"},{"issue":"2","key":"15_CR59","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF00264436","volume":"18","author":"GW Ernst","year":"1982","unstructured":"Ernst, G.W., Navlakha, J.K., Ogden, W.F.: Verification of programs with procedure-type parameters. Acta Informatica 18(2), 149\u2013169 (1982)","journal-title":"Acta Informatica"},{"key":"15_CR60","doi-asserted-by":"crossref","unstructured":"Ernst, M., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. IEEE Trans. Softw. Eng. 27(2), 99\u2013123 (2001). http:\/\/doi.ieeecomputersociety.org\/10.1109\/32.908957","DOI":"10.1109\/32.908957"},{"key":"15_CR61","unstructured":"Ernst, M., et al.: Daikon website. https:\/\/plse.cs.washington.edu\/daikon\/. Accessed Sept 2021"},{"key":"15_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/978-3-642-37036-6_8","volume-title":"Programming Languages and Systems","author":"J-C Filli\u00e2tre","year":"2013","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3 \u2014 where programs meet provers. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 125\u2013128. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37036-6_8"},{"key":"15_CR63","doi-asserted-by":"crossref","unstructured":"Findler, R.B., Felleisen, M.: Contract soundness for object-oriented languages. In: OOPSLA 2001 Conference Proceedings. Object-Oriented Programming, Systems, Languages, and Applications, 14\u201318 October 2001, Tampa Bay, Florida, USA, pp. 1\u201315. ACM, New York (2001)","DOI":"10.1145\/504311.504283"},{"key":"15_CR64","volume-title":"Modelling Systems: Practical Tools in Software Development","author":"J Fitzgerald","year":"1998","unstructured":"Fitzgerald, J., Larsen, P.G.: Modelling Systems: Practical Tools in Software Development. Cambridge University Press, Cambridge (1998)"},{"key":"15_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45251-6_29","volume-title":"FME 2001: Formal Methods for Increasing Software Productivity","author":"C Flanagan","year":"2001","unstructured":"Flanagan, C., Leino, K.R.M.: Houdini, an annotation assistant for ESC\/Java. In: Oliveira, J.N., Zave, P. (eds.) FME 2001. LNCS, vol. 2021, pp. 500\u2013517. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45251-6_29http:\/\/www.springerlink.com\/content\/nxukfdgg7623q3a9"},{"key":"15_CR66","unstructured":"(2011ff). https:\/\/frama-c.com"},{"key":"15_CR67","unstructured":"Gosling, J., Joy, B., Steele, G.: The Java Language Specification. The Java Series. Addison-Wesley, Reading (1996). http:\/\/www.aw.com\/cp\/javaseries.html"},{"key":"15_CR68","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":"15_CR69","doi-asserted-by":"crossref","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. In: Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2008, pp. 281\u2013292. Association for Computing Machinery, New York (2008). https:\/\/doi.org\/10.1145\/1375581.1375616","DOI":"10.1145\/1375581.1375616"},{"issue":"2","key":"15_CR70","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/0167-6423(86)90021-3","volume":"6","author":"JV Guttag","year":"1986","unstructured":"Guttag, J.V., Horning, J.J.: Report on the larch shared language. Sci. Comput. Program. 6(2), 103\u2013134 (1986)","journal-title":"Sci. Comput. Program."},{"key":"15_CR71","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2704-5","volume-title":"Larch: Languages and Tools for Formal Specification","author":"JV Guttag","year":"1993","unstructured":"Guttag, J.V., Horning, J.J., Garland, S.J., Jones, K.D., Modet, A., Wing, J.M.: Larch: Languages and Tools for Formal Specification. Springer, New York (1993). https:\/\/doi.org\/10.1007\/978-1-4612-2704-5"},{"issue":"5","key":"15_CR72","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1109\/MS.1985.231756","volume":"2","author":"JV Guttag","year":"1985","unstructured":"Guttag, J.V., Horning, J.J., Wing, J.M.: The Larch family of specification languages. IEEE Softw. 2(5), 24\u201336 (1985)","journal-title":"IEEE Softw."},{"key":"15_CR73","unstructured":"Haddad, G., Leavens, G.T.: Extensible dynamic analysis for JML: a case study with loop annotations. Technical report, CS-TR-08-05, School of Electrical Engineering and Computer Science, University of Central Florida, Orlando, Florida, April 2008"},{"key":"15_CR74","doi-asserted-by":"crossref","unstructured":"Haddad, G., Leavens, G.T.: Specifying subtypes in safety critical Java programs. Concurr. Comput. Pract. Exp. 25(16), 2290\u20132306 (2013)","DOI":"10.1002\/cpe.2930"},{"issue":"5","key":"15_CR75","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1109\/52.57887","volume":"7","author":"A Hall","year":"1990","unstructured":"Hall, A.: Seven myths of formal methods. IEEE Softw. 7(5), 11\u201319 (1990)","journal-title":"IEEE Softw."},{"key":"15_CR76","doi-asserted-by":"crossref","unstructured":"Hamza, J., Voirol, N., Kun\u010dak, V.: System FR: formalized foundations for the Stainless verifier. Proc. ACM Program. Lang. 3(OOPSLA) (2019). https:\/\/doi.org\/10.1145\/3360592","DOI":"10.1145\/3360592"},{"key":"15_CR77","doi-asserted-by":"publisher","unstructured":"Hatcliff, J., Leavens, G.T., Leino, K.R.M., M\u00fcller, P., Parkinson, M.: Behavioral interface specification languages. ACM Comput. Surv. 44(3), 16:1\u201316:58 (2012). https:\/\/doi.org\/10.1145\/2187671.2187678. http:\/\/doi.acm.org\/10.1145\/2187671.2187678","DOI":"10.1145\/2187671.2187678"},{"key":"15_CR78","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"60","DOI":"10.1007\/978-3-642-19835-9_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Hoder","year":"2011","unstructured":"Hoder, K., Kov\u00e1cs, L., Voronkov, A.: Invariant generation in vampire. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 60\u201364. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_7"},{"key":"15_CR79","doi-asserted-by":"crossref","unstructured":"Hubbers, E., Oostdijk, M., Poll, E.: From finite state machines to provably correct JavaCard applets. In: Workshop of IFIP WG 11.2 - Small Systems Security. IFIP (2003). http:\/\/www.cs.ru.nl\/~erikpoll\/publications\/sec03.pdf","DOI":"10.1007\/978-0-387-35691-4_47"},{"key":"15_CR80","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"284","DOI":"10.1007\/3-540-46428-X_20","volume-title":"Fundamental Approaches to Software Engineering","author":"M Huisman","year":"2000","unstructured":"Huisman, M., Jacobs, B.: Java program verification via a hoare logic with abrupt termination. In: Maibaum, T. (ed.) FASE 2000. LNCS, vol. 1783, pp. 284\u2013303. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-46428-X_20"},{"key":"15_CR81","doi-asserted-by":"crossref","unstructured":"Hussain, F., Leavens, G.T.: temporaljmlc: a JML runtime assertion checker extension for specification and checking of temporal properties. Technical report, CS-TR-10-08, UCF, Department of EECS, Orlando, Florida, July 2010","DOI":"10.1109\/SEFM.2010.15"},{"key":"15_CR82","doi-asserted-by":"crossref","unstructured":"Ishtiaq, S.S., O\u2019Hearn, P.W.: BI as an assertion language for mutable data structures. In: Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2001, pp. 14\u201326. ACM, New York (2001). http:\/\/doi.acm.org\/10.1145\/360204.375719","DOI":"10.1145\/373243.375719"},{"key":"15_CR83","doi-asserted-by":"crossref","unstructured":"Jacobs, B., van den Berg, J., Huisman, M., van Berkum, M., Hensel, U., Tews, H.: Reasoning about Java classes (preliminary report). In: OOPSLA 1998 Conference Proceedings. ACM SIGPLAN Notices, vol. 33, no. 10, pp. 329\u2013340. ACM, October 1998","DOI":"10.1145\/286942.286973"},{"key":"15_CR84","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-39656-7_8","volume-title":"Formal Methods for Components and Objects","author":"B Jacobs","year":"2003","unstructured":"Jacobs, B., Kiniry, J., Warnier, M.: Java program verification challenges. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2002. LNCS, vol. 2852, pp. 202\u2013219. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-39656-7_8"},{"key":"15_CR85","unstructured":"Jacobs, B., Meijer, H., Poll, E.: VerifiCard: a European project for smart card verification. Newsletter 5 of the Dutch Association for Theoretical Computer Science (NVTI) (2001). https:\/\/repository.ubn.ru.nl\/bitstream\/handle\/2066\/130369\/130369.pdf"},{"key":"15_CR86","unstructured":"Jones, C.B.: Program specification and verification in VDM. Technical report, UMCS-86-10-5, Department of Computer Science, University of Manchester, Manchester M13 9PL, England, November 1986"},{"key":"15_CR87","series-title":"International Series in Computer Science","volume-title":"Systematic software development using VDM","author":"CB Jones","year":"1986","unstructured":"Jones, C.B.: Systematic software development using VDM. International Series in Computer Science, Prentice-Hall Inc., Englewood Cliffs (1986)"},{"key":"15_CR88","unstructured":"The KeY project. https:\/\/www.key-project.org. Accessed Sept 2021"},{"key":"15_CR89","doi-asserted-by":"crossref","unstructured":"Leavens, G.T.: An overview of Larch\/C++: behavioral specifications for C++ modules. In: Kilov, H., Harvey, W. (eds.) Specification of Behavioral Semantics in Object-Oriented Information Modeling, chap. 8, pp. 121\u2013142. Kluwer Academic Publishers, Boston (1996). An extended version is TR #96-01d, Department of Computer Science, Iowa State University, Ames, Iowa, 50011","DOI":"10.1007\/978-0-585-27524-6_8"},{"key":"15_CR90","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/11901433_2","volume-title":"Formal Methods and Software Engineering","author":"GT Leavens","year":"2006","unstructured":"Leavens, G.T.: JML\u2019s rich, inherited specifications for behavioral subtypes. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 2\u201334. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11901433_2"},{"key":"15_CR91","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1087","DOI":"10.1007\/3-540-48118-4_8","volume-title":"FM\u201999 \u2014 Formal Methods","author":"GT Leavens","year":"1999","unstructured":"Leavens, G.T., Baker, A.L.: Enhancing the pre- and postcondition technique for more expressive specifications. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1709, pp. 1087\u20131106. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48118-4_8"},{"key":"15_CR92","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: a Java modeling language. In: Formal Underpinnings of Java Workshop (at OOPSLA 1998), October 1998. http:\/\/www-dse.doc.ic.ac.uk\/~sue\/oopsla\/cfp.html"},{"key":"15_CR93","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. ACM SIGSOFT Softw. Eng. Notes 31(3), 1\u201338 (2006). http:\/\/doi.acm.org\/10.1145\/1127878.1127884","DOI":"10.1145\/1127878.1127884"},{"key":"15_CR94","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-69149-5_15","volume-title":"Verified Software: Theories, Tools, Experiments","author":"GT Leavens","year":"2008","unstructured":"Leavens, G.T., Clifton, C.: Lessons from the JML project. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 134\u2013143. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-69149-5_15"},{"key":"15_CR95","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Leino, K.R.M., M\u00fcller, P.: Specification and verification challenges for sequential object-oriented programs. Formal Aspects Comput. 19(2), 159\u2013189 (2007). http:\/\/dx.doi.org\/10.1007\/s00165-007-0026-7","DOI":"10.1007\/s00165-007-0026-7"},{"key":"15_CR96","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., M\u00fcller, P.: Information hiding and visibility in interface specifications. In: International Conference on Software Engineering (ICSE), Los Alamitos, California, pp. 385\u2013395. IEEE, May 2007. http:\/\/dx.doi.org\/10.1109\/ICSE.2007.44","DOI":"10.1109\/ICSE.2007.44"},{"key":"15_CR97","doi-asserted-by":"publisher","unstructured":"Leavens, G.T., Naumann, D.A.: Behavioral subtyping, specification inheritance, and modular reasoning. TOPLAS 37(4), 13:1\u201313:88 (2015). https:\/\/doi.org\/10.1145\/2766446. http:\/\/doi.acm.org\/10.1145\/2766446","DOI":"10.1145\/2766446"},{"key":"15_CR98","unstructured":"Leavens, G.T., Naumann, D.A., Rosenberg, S.: Preliminary definition of Core JML. CS Report 2006-07, Stevens Institute of Technology, September 2006. http:\/\/www.cs.stevens.edu\/~naumann\/publications\/SIT-TR-2006-07.pdf"},{"key":"15_CR99","unstructured":"Leavens, G.T., et al.: JML Reference Manual, May 2008. http:\/\/www.jmlspecs.org"},{"key":"15_CR100","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Weihl, W.E.: Reasoning about object-oriented programs that use subtypes (extended abstract). In: Meyrowitz, N. (ed.) OOPSLA ECOOP 1990 Proceedings. ACM SIGPLAN Notices, vol. 25, no. 10, pp. 212\u2013223. ACM (1990). http:\/\/doi.acm.org\/10.1145\/97945.97970","DOI":"10.1145\/97946.97970"},{"key":"15_CR101","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Weihl, W.E.: Specification and verification of object-oriented programs using supertype abstraction. Acta Informatica 32(8), 705\u2013778 (1995). http:\/\/dx.doi.org\/10.1007\/BF01178658","DOI":"10.1007\/BF01178658"},{"key":"15_CR102","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Wing, J.M.: Protective interface specifications. Formal Aspects Comput. 10(1), 59\u201375 (1998). http:\/\/dx.doi.org\/10.1007\/PL00003926","DOI":"10.1007\/PL00003926"},{"key":"15_CR103","unstructured":"Leino, K.R.M.: Specification and verification of object-oriented software (2008). http:\/\/research.microsoft.com\/en-us\/um\/people\/leino\/papers\/krml190.pdf. Lecture notes from Marktoberdorf Internation Summer School. http:\/\/research.microsoft.com\/en-us\/um\/people\/leino\/papers\/krml190.pdf"},{"key":"15_CR104","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":"15_CR105","unstructured":"Leino, K.R.M., Ford, R.L., Cok, D.R.: Dafny reference manual, July 2021. https:\/\/github.com\/dafny-lang\/dafny\/blob\/master\/docs\/DafnyRef\/out\/DafnyRef.pdf"},{"key":"15_CR106","doi-asserted-by":"crossref","unstructured":"Leino, K.R.M., Monahan, R.: Reasoning about comprehensions with first-order SMT solvers. In: Proceedings of the 2009 ACM Symposium on Applied Computing, SAC 2009, pp. 615\u2013622. Association for Computing Machinery, New York (2009). https:\/\/doi.org\/10.1145\/1529282.1529411","DOI":"10.1145\/1529282.1529411"},{"key":"15_CR107","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":"KRM 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. 6217, pp. 112\u2013126. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15057-9_8"},{"key":"15_CR108","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-540-24851-4_22","volume-title":"ECOOP 2004 \u2013 Object-Oriented Programming","author":"KRM Leino","year":"2004","unstructured":"Leino, K.R.M., M\u00fcller, P.: Object invariants in dynamic contexts. In: Odersky, M. (ed.) ECOOP 2004. LNCS, vol. 3086, pp. 491\u2013515. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24851-4_22http:\/\/www.springerlink.com\/content\/ttfnjg36yq64pah8"},{"key":"15_CR109","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1007\/11526841_4","volume-title":"FM 2005: Formal Methods","author":"KRM Leino","year":"2005","unstructured":"Leino, K.R.M., M\u00fcller, P.: Modular verification of static class invariants. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 26\u201342. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11526841_4https:\/\/tinyurl.com\/4xfc2989"},{"key":"15_CR110","unstructured":"Leino, K.R.M., et al.: Dafny github site. https:\/\/github.com\/dafny-lang\/dafny. Accessed Sept 2021"},{"key":"15_CR111","doi-asserted-by":"crossref","unstructured":"March\u00e9, C., Paulin-Mohring, C., Urbain, X.: The KRAKATOA tool for certification of JAVA\/JAVACARD programs annotated in JML. J. Logic Algebraic Program. 58(1\u20132), 89\u2013106 (2004). http:\/\/dx.doi.org\/10.1016\/j.jlap.2003.07.006","DOI":"10.1016\/j.jlap.2003.07.006"},{"key":"15_CR112","volume-title":"Object-Oriented Software Construction","author":"B Meyer","year":"1997","unstructured":"Meyer, B.: Object-Oriented Software Construction, vol. 2. Prentice Hall, New York (1997)"},{"key":"15_CR113","series-title":"LNCS","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45651-1","volume-title":"Modular Specification and Verification of Object-Oriented Programs","author":"P M\u00fcller","year":"2002","unstructured":"M\u00fcller, P.: Modular Specification and Verification of Object-Oriented Programs. LNCS, vol. 2262. Springer, Berlin (2002). https:\/\/doi.org\/10.1007\/3-540-45651-1http:\/\/tinyurl.com\/jtwot"},{"key":"15_CR114","doi-asserted-by":"publisher","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular specification of frame properties in JML. Concurr. Comput. Pract. Exp. 15(2), 117\u2013154 (2003). https:\/\/doi.org\/10.1002\/cpe.713. ftp:\/\/ftp.cs.iastate.edu\/pub\/techreports\/TR02-02\/TR.pdf","DOI":"10.1002\/cpe.713"},{"key":"15_CR115","doi-asserted-by":"crossref","unstructured":"M\u00fcller, P., Poetzsch-Heffter, A., Leavens, G.T.: Modular invariants for layered object structures. Sci. Comput. Program. 62(3), 253\u2013286 (2006). http:\/\/dx.doi.org\/10.1016\/j.scico.2006.03.001","DOI":"10.1016\/j.scico.2006.03.001"},{"issue":"3","key":"15_CR116","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1016\/j.tcs.2007.02.004","volume":"376","author":"DA Naumann","year":"2007","unstructured":"Naumann, D.A.: Observational purity and encapsulation. Theor. Comput. Sci. 376(3), 205\u2013224 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"15_CR117","unstructured":"Nilizadeh, A.: Test overfitting: challenges, approaches, and measurements. Technical report, University of Central Florida, Computer Science (2021)"},{"key":"15_CR118","doi-asserted-by":"crossref","unstructured":"Nilizadeh, A.: Automated program repair and test overfitting: measurements and approaches using formal methods. In: 2022 15th IEEE Conference on Software Testing, Verification and Validation (ICST). IEEE (2022, in press)","DOI":"10.1109\/ICST53961.2022.00061"},{"key":"15_CR119","doi-asserted-by":"crossref","unstructured":"Nilizadeh, A., Calvo, M., Leavens, G.T., Cok, D.R.: Generating counterexamples in the form of unit tests from Hoare-style verification attempts. In: IEEE\/ACM 10th International Conference on Formal Methods in Software Engineering (FormaliSE). IEEE (2022, in press)","DOI":"10.1145\/3524482.3527656"},{"key":"15_CR120","doi-asserted-by":"crossref","unstructured":"Nilizadeh, A., Calvo, M., Leavens, G.T., Le, X.B.D.: More reliable test suites for dynamic APR by using counterexamples. In: 2021 IEEE 32nd International Symposium on Software Reliability Engineering (ISSRE), Los Altos, pp. 208\u2013219. IEEE (2021). https:\/\/doi.org\/10.1109\/ISSRE52982.2021.00032","DOI":"10.1109\/ISSRE52982.2021.00032"},{"key":"15_CR121","doi-asserted-by":"crossref","unstructured":"Nilizadeh, A., Leavens, G.T.: Be realistic: automated program repair is a combination of undecidable problems. In: 2022 IEEE\/ACM International Workshop on Automated Program Repair (APR). IEEE (2022, in press)","DOI":"10.1145\/3524459.3527346"},{"key":"15_CR122","doi-asserted-by":"crossref","unstructured":"Nilizadeh, A., Leavens, G.T., Le, X.B.D., P\u0103s\u0103reanu, C.S., Cok, D.R.: Exploring true test overfitting in dynamic automated program repair using formal methods. In: 2021 14th IEEE Conference on Software Testing, Verification and Validation (ICST), Los Altos, pp. 229\u2013240. IEEE (2021). https:\/\/tinyurl.com\/bn3ecw98","DOI":"10.1109\/ICST49551.2021.00033"},{"key":"15_CR123","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/978-3-030-79379-1_5","volume-title":"Tests and Proofs","author":"A Nilizadeh","year":"2021","unstructured":"Nilizadeh, A., Leavens, G.T., P\u0103s\u0103reanu, C.S.: Using a guided fuzzer and preconditions to achieve branch coverage with valid inputs. In: Loulergue, F., Wotawa, F. (eds.) TAP 2021. LNCS, vol. 12740, pp. 72\u201384. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79379-1_5https:\/\/tinyurl.com\/4xzxxrn2"},{"key":"15_CR124","doi-asserted-by":"crossref","unstructured":"Nimmer, J.W., Ernst, M.D.: Static verification of dynamically detected program invariants: integrating daikon and ESC\/Java. In: Proceedings of RV\u201901, First Workshop on Runtime Verification. Elsevier (2001). http:\/\/dx.doi.org\/10.1016\/S1571-0661(04)00256-7","DOI":"10.1016\/S1571-0661(04)00256-7"},{"key":"15_CR125","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"158","DOI":"10.1007\/BFb0054091","volume-title":"ECOOP\u201998 \u2014 Object-Oriented Programming","author":"J Noble","year":"1998","unstructured":"Noble, J., Vitek, J., Potter, J.: Flexible alias protection. In: Jul, E. (ed.) ECOOP 1998. LNCS, vol. 1445, pp. 158\u2013185. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0054091"},{"key":"15_CR126","unstructured":"Oracle: OpenJDK (2021). http:\/\/openjdk.java.net\/. Accessed Sept 2021"},{"key":"15_CR127","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"748","DOI":"10.1007\/3-540-55602-8_217","volume-title":"Automated Deduction\u2014CADE-11","author":"S Owre","year":"1992","unstructured":"Owre, S., Rushby, J.M., Shankar, N.: PVS: a prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748\u2013752. Springer, Heidelberg (1992). https:\/\/doi.org\/10.1007\/3-540-55602-8_217"},{"key":"15_CR128","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"104","DOI":"10.1007\/978-3-642-19861-8_7","volume-title":"Compiler Construction","author":"DJ Pearce","year":"2011","unstructured":"Pearce, D.J.: JPure: a modular purity system for java. In: Knoop, J. (ed.) CC 2011. LNCS, vol. 6601, pp. 104\u2013123. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19861-8_7"},{"key":"15_CR129","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"238","DOI":"10.1007\/978-3-319-02654-1_13","volume-title":"Software Language Engineering","author":"DJ Pearce","year":"2013","unstructured":"Pearce, D.J., Groves, L.: Whiley: a platform for research in software verification. In: Erwig, M., Paige, R.F., Van Wyk, E. (eds.) SLE 2013. LNCS, vol. 8225, pp. 238\u2013248. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-02654-1_13"},{"key":"15_CR130","doi-asserted-by":"crossref","unstructured":"Poll, E., van den Berg, J., Jacobs, B.: Specification of the JavaCard API in JML. In: Domingo-Ferrer, J., Chan, D., Watson, A. (eds.) Smart Card Research and Advanced Application Conference (CARDIS 2000), pp. 135\u2013154. Kluwer Academic Publishers (2000)","DOI":"10.1007\/978-0-387-35528-3_8"},{"key":"15_CR131","unstructured":"Raghavan, A.D.: Design of a JML documentation generator. Technical report, 00-12, Iowa State University, Department of Computer Science, July 2000. ftp:\/\/ftp.cs.iastate.edu\/pub\/techreports\/TR00-12\/TR.ps.gz"},{"key":"15_CR132","doi-asserted-by":"crossref","unstructured":"Rajan, H., Nguyen, T.N., Leavens, G.T., Dyer, R.: Inferring behavioral specifications from large-scale repositories by leveraging collective intelligence. In: ICSE 2015: The 37th International Conference on Software Engineering: NIER Track, pp. 579\u2013582, May 2015. https:\/\/tinyurl.com\/jpemux34","DOI":"10.1109\/ICSE.2015.339"},{"key":"15_CR133","unstructured":"Reb\u00ealo, H.: AspectJML website (2021). https:\/\/www.cin.ufpe.br\/~hemr\/aspectjml\/. Accessed Sept 2021"},{"key":"15_CR134","doi-asserted-by":"publisher","unstructured":"Reb\u00ealo, H., et al.: AspectJML: modular specification and runtime checking for crosscutting contracts. In: Proceedings of the 13th International Conference on Modularity, MODULARITY 2014, pp. 157\u2013168. ACM, New York (2014). https:\/\/doi.org\/10.1145\/2577080.2577084. http:\/\/doi.acm.org\/10.1145\/2577080.2577084","DOI":"10.1145\/2577080.2577084"},{"key":"15_CR135","doi-asserted-by":"publisher","unstructured":"Reb\u00ealo, H., Leavens, G.T., Lima, R.M.: Client-aware checking and information hiding in interface specifications with JML\/Ajmlc. In: Proceedings of the 2013 Companion Publication for Conference on Systems, Programming, & Applications: Software for Humanity, SPLASH 2013, pp. 11\u201312. ACM, New York (2013). https:\/\/doi.org\/10.1145\/2508075.2514569.. http:\/\/doi.acm.org\/10.1145\/2508075.2514569","DOI":"10.1145\/2508075.2514569."},{"key":"15_CR136","doi-asserted-by":"crossref","unstructured":"Reb\u00ealo, H., Soares, S., Lima, R., Ferreira, L., Corn\u00e9lio, M.: Implementing Java modeling language contracts with AspectJ. In: SAC 2008: Proceedings of the 2008 ACM Symposium on Applied computing, pp. 228\u2013233. ACM, New York (2008). http:\/\/doi.acm.org\/10.1145\/1363686.1363745","DOI":"10.1145\/1363686.1363745"},{"key":"15_CR137","doi-asserted-by":"crossref","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: Proceedings of the Seventeenth Annual IEEE Symposium on Logic in Computer Science, Los Alamitos, California, pp. 55\u201374. IEEE Computer Society Press (2002). http:\/\/dx.doi.org\/10.1109\/LICS.2002.1029817","DOI":"10.1109\/LICS.2002.1029817"},{"key":"15_CR138","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-64354-6_1","volume-title":"Deductive Software Verification: Future Perspectives","author":"PH Schmitt","year":"2020","unstructured":"Schmitt, P.H.: A short history of KeY. In: Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Ulbrich, M. (eds.) Deductive Software Verification: Future Perspectives. LNCS, vol. 12345, pp. 3\u201318. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-64354-6_1https:\/\/tinyurl.com\/3xbrdwbr"},{"key":"15_CR139","unstructured":"Shaner, S.M., Leavens, G.T., Naumann, D.A.: Modular verification of higher-order methods with mandatory calls specified by model programs. In: International Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA), Montreal, Canada, pp. 351\u2013367. ACM, New York (2007). http:\/\/doi.acm.org\/10.1145\/1297027.1297053. http:\/\/doi.acm.org\/10.1145\/1297027.1297053"},{"key":"15_CR140","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"703","DOI":"10.1007\/978-3-642-22110-1_57","volume-title":"Computer Aided Verification","author":"R Sharma","year":"2011","unstructured":"Sharma, R., Dillig, I., Dillig, T., Aiken, A.: Simplifying loop invariant generation using splitter predicates. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 703\u2013719. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_57"},{"key":"15_CR141","doi-asserted-by":"crossref","unstructured":"Singleton, J.L., Leavens, G.T., Rajan, H., Cok, D.: Poster: an algorithm and tool to infer practical postconditions. In: 2018 ACM\/IEEE 40th International Conference on Software Engineering: Companion Proceedings, Gothenburg, Sweden, pp. 313\u2013314. ACM (2018). https:\/\/doi.org\/10.1145\/3183440.3194986","DOI":"10.1145\/3183440.3194986"},{"key":"15_CR142","unstructured":"Smans, J., Jacobs, B., Piessens, F.: Implicit dynamic frames. In: Huisman, M. (ed.) Formal Techniques for Java-like Programs (FTfJP 2008), pp. 1\u201312. Radboud University, Nijmegen, Technical report ICIS-R08013, Radboud University (2008)"},{"key":"15_CR143","doi-asserted-by":"crossref","unstructured":"Svendsen, K., Birkedal, L., Parkinson, M.: Verifying generics and delegates. ECOOP 2010 - Object-oriented Programming, p. 175 (2010)","DOI":"10.1007\/978-3-642-14107-2_9"},{"key":"15_CR144","doi-asserted-by":"crossref","unstructured":"Wills, A.: Capsules and types in fresco: program validation in smalltalk. In: America, P. (ed.) ECOOP 1991: European Conference on Object Oriented Programming. LNCS, vol. 512, pp. 59\u201376. Springer, New York (1991). http:\/\/dx.doi.org\/10.1007\/BFb0057015","DOI":"10.1007\/BFb0057015"},{"key":"15_CR145","doi-asserted-by":"crossref","unstructured":"Wills, A.: Specification in fresco. In: Stepney, S., Barden, R., Cooper, D. (eds.) Object Orientation in Z, chap. 11, pp. 127\u2013135. Workshops in Computing, Springer, Cambridge CB2 1LQ, UK (1992)","DOI":"10.1007\/978-1-4471-3552-4_11"},{"key":"15_CR146","unstructured":"Wills, A.: Refinement in fresco. In: Lano, K., Houghton, H. (eds.) Object-Oriented Specification Case Studies, chap. 9, pp. 184\u2013201. The Object-Oriented Series. Prentice-Hall, Englewood Cliffs (1994)"},{"key":"15_CR147","unstructured":"Wing, J.M.: A two-tiered approach to specifying programs. Technical report, TR-299, Massachusetts Institute of Technology, Laboratory for Computer Science (1983)"},{"key":"15_CR148","doi-asserted-by":"crossref","unstructured":"Wolff, F., B\u00edl\u00fd, A., Matheja, C., M\u00fcller, P., Summers, A.J.: Modular specification and verification of closures in Rust. Proc. ACM Program. Lang. 5(OOPSLA) (2021). https:\/\/doi.org\/10.1145\/3485522","DOI":"10.1145\/3485522"}],"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_15","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,10]],"date-time":"2023-02-10T18:16:40Z","timestamp":1676053000000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-08166-8_15"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031081651","9783031081668"],"references-count":148,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-08166-8_15","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"}}]}}