{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T03:41:08Z","timestamp":1742960468884,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031198489"},{"type":"electronic","value":"9783031198496"}],"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-19849-6_3","type":"book-chapter","created":{"date-parts":[[2022,10,19]],"date-time":"2022-10-19T15:03:32Z","timestamp":1666191812000},"page":"29-44","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Abstraction in\u00a0Deductive Verification: Model Fields and\u00a0Model Methods"],"prefix":"10.1007","author":[{"given":"David R.","family":"Cok","sequence":"first","affiliation":[]},{"given":"Gary T.","family":"Leavens","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,10,17]]},"reference":[{"key":"3_CR1","unstructured":"ACSL. ANSI-C Specification Language (2021). https:\/\/github.com\/acsl-language\/acsl\/"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M.: Deductive software verification - The KeY Book. In: LNCS, Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"3_CR3","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":"3_CR4","unstructured":"Barrett, C., et al.: CVC5 web site (2022). https:\/\/cvc5.github.io\/"},{"key":"3_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-22438-6_15","volume-title":"Automated Deduction \u2013 CADE-23","author":"S B\u00f6hme","year":"2011","unstructured":"B\u00f6hme, S., Moskal, M.: Heaps and data structures: a challenge for automated provers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 177\u2013191. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_15"},{"key":"3_CR6","unstructured":"Cok, D.R.: (2021)"},{"key":"3_CR7","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, NY (2021). https:\/\/www.openjml.org","DOI":"10.1145\/3464971.3468417"},{"key":"3_CR8","doi-asserted-by":"publisher","first-page":"207","DOI":"10.3233\/SAT190109","volume":"9","author":"DR Cok","year":"2014","unstructured":"Cok, D.R., D\u00e9harbe, D., Weber, T.: The 2014 SMT competition. J. Satisfiability Boolean Model. Comput. 9, 207\u2013242 (2014)","journal-title":"J. Satisfiability Boolean Model. Comput."},{"key":"3_CR9","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":"3_CR10","unstructured":"Cok, D.R., Leavens, G.T., Ulbrich, M.: Java Modeling Language (JML) Reference Manual, 2nd edn (2022). www.openjml.org\/documentation\/JML_Reference_Manual.pdf"},{"key":"3_CR11","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"},{"key":"3_CR12","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation (PLDI 2002), vol. 37(5), pp. 234\u2013245. SIGPLAN, NY. ACM (2002)","DOI":"10.1145\/543552.512558"},{"key":"3_CR13","unstructured":"Frama-C: (2021). https:\/\/frama-c.com"},{"key":"3_CR14","unstructured":"KeY: The KeY project (2021). www.key-project.org"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: Preliminary design of JML: a behavioral interface specification language for Java. Technical Report 98-06-rev29, Iowa State University, Department of Computer Science (2006). Also ACM SIGSOFT Softw. Eng. Notes 31(3), 1\u201338 (2006)","DOI":"10.1145\/1127878.1127884"},{"issue":"10","key":"3_CR16","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1145\/286942.286953","volume":"33","author":"KRM Leino","year":"1998","unstructured":"Leino, K.R.M.: Data groups: specifying the modification of extended state. SIGPLAN Not. 33(10), 144\u2013153 (1998)","journal-title":"SIGPLAN Not."},{"key":"3_CR17","unstructured":"Leino, K.R.M.: This is boogie 2 (2008)"},{"key":"3_CR18","unstructured":"Leino, K.R.M., et al.: Dafny github site (2021). https:\/\/github.com\/dafny-lang\/dafny. Accessed Sept 2021"},{"key":"3_CR19","unstructured":"Leino, K.R.M., Ford, R.L., Cok, D.R.: Dafny reference manual. https:\/\/github.com\/dafny-lang\/dafny\/blob\/master\/docs\/DafnyRef\/out\/DafnyRef.pdf. Accessed Jul 2021"},{"key":"3_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-642-12002-2_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"KRM Leino","year":"2010","unstructured":"Leino, K.R.M., R\u00fcmmer, P.: A polymorphic intermediate verification language: design and logical encoding. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 312\u2013327. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_26"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Mostowski, W., Ulbrich, M.: Dynamic dispatch for method contracts through abstract predicates. In: Proceedings of the 14th International Conference on Modularity (MODULARITY 2015), pp. 109\u2013116. Association for Computing Machinery, NY (2015)","DOI":"10.1145\/2724525.2724574"},{"key":"3_CR22","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1007\/3-540-45651-1_5","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, pp. 143\u2013194. Springer-Verlag, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45651-1_5"},{"key":"3_CR23","unstructured":"SMTCOMP: Smtcomp competition (2022). https:\/\/smt-comp.github.io\/2022\/"},{"key":"3_CR24","unstructured":"Tinelli, C., et al.: SMT-LIB web site (2003). https:\/\/smtlib.cs.uiowa.edu\/"},{"issue":"1","key":"3_CR25","first-page":"221","volume":"11","author":"T Weber","year":"2019","unstructured":"Weber, T., Conchon, S., D\u00e9harbe, D., Heizmann, M., Niemetz, A., Reger, G.: The SMT competition 2015\u20132018. J. Satisf. Boolean Model. Comput. 11(1), 221\u2013259 (2019)","journal-title":"J. Satisf. Boolean Model. Comput."},{"key":"3_CR26","unstructured":"Wei\u00df, B.: Deductive verification of object-oriented software: dynamic frames, dynamic logic and predicate abstraction. PhD thesis, KIT (2011)"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation. Verification Principles"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-19849-6_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,10,20]],"date-time":"2022-10-20T00:06:05Z","timestamp":1666224365000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-19849-6_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031198489","9783031198496"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-19849-6_3","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":"17 October 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22 October 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.isola-conference.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}