{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T16:51:49Z","timestamp":1725987109282},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319989372"},{"type":"electronic","value":"9783319989389"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-98938-9_3","type":"book-chapter","created":{"date-parts":[[2018,8,8]],"date-time":"2018-08-08T15:08:34Z","timestamp":1533740914000},"page":"30-46","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Reasoning About JML: Differences Between KeY and OpenJML"],"prefix":"10.1007","author":[{"given":"Jan","family":"Boerman","sequence":"first","affiliation":[]},{"given":"Marieke","family":"Huisman","sequence":"additional","affiliation":[]},{"given":"Sebastiaan","family":"Joosten","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,8,9]]},"reference":[{"key":"3_CR1","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, LNCS, vol. 10001. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-319-49812-6","DOI":"10.1007\/978-3-319-49812-6"},{"key":"3_CR2","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. 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":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/3-540-44555-2_4","volume-title":"Object-Oriented Technology","author":"S Drossopoulou","year":"2000","unstructured":"Drossopoulou, S., Eisenbach, S., Jacobs, B., Leavens, G.T., M\u00fcller, P., Poetzsch-Heffter, A.: Formal techniques for Java programs. In: Goos, G., Hartmanis, J., van Leeuwen, J., Malenfant, J., Moisan, S., Moreira, A. (eds.) ECOOP 2000. LNCS, vol. 1964, pp. 41\u201354. Springer, Heidelberg (2000). https:\/\/doi.org\/10.1007\/3-540-44555-2_4"},{"issue":"6","key":"3_CR4","doi-asserted-by":"publisher","first-page":"729","DOI":"10.1007\/s10009-013-0293-y","volume":"17","author":"D Bruns","year":"2015","unstructured":"Bruns, D., Mostowski, W., Ulbrich, M.: Implementation-level verification of algorithms with KeY. STTT 17(6), 729\u2013744 (2015)","journal-title":"STTT"},{"issue":"3","key":"3_CR5","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/s10009-004-0167-4","volume":"7","author":"L Burdy","year":"2005","unstructured":"Burdy, L., et al.: An overview of JML tools and applications. STTT 7(3), 212\u2013232 (2005)","journal-title":"STTT"},{"key":"3_CR6","unstructured":"Chalin, P.: Reassessing JML\u2019s logical foundation. In: Proceedings of the 7th Workshop on Formal Techniques for Java-like Programs (FTfJP 2005), Glasgow, Scotland (2005)"},{"key":"3_CR7","unstructured":"Cheon, Y.: A Runtime assertion checker for the java modeling language. Ph.D. thesis, Department of Computer Science, Iowa State University, Ames (2003). Technical Report 03\u201309"},{"key":"3_CR8","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_CR9","series-title":"LNCS","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":"3_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/BFb0055133","volume-title":"Theorem Proving in Higher Order Logics","author":"D Griffioen","year":"1998","unstructured":"Griffioen, D., Huisman, M.: A comparison of PVS and Isabelle\/HOL. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 123\u2013142. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055133"},{"issue":"6","key":"3_CR11","doi-asserted-by":"publisher","first-page":"647","DOI":"10.1007\/s10009-015-0396-8","volume":"17","author":"M Huisman","year":"2015","unstructured":"Huisman, M., Klebanov, V., Monahan, R.: VerifyThis 2012 - a program verification competition. STTT 17(6), 647\u2013657 (2015). https:\/\/doi.org\/10.1007\/s10009-015-0396-8","journal-title":"STTT"},{"key":"3_CR12","unstructured":"JML support in KeY. https:\/\/www.key-project.org\/jml-support-in-key\/"},{"key":"3_CR13","unstructured":"Currently supported features, April 2018. http:\/\/www.openjml.org\/documentation\/features.shtml"},{"key":"3_CR14","unstructured":"Kirsten, M.: Proving well-definedness of JML specifications with KeY. Master\u2019s thesis, ITI Schmitt, Karlsruhe Institute of Technology, November 2013"},{"key":"3_CR15","doi-asserted-by":"crossref","unstructured":"Kn\u00fcppel, A., Th\u00fcm, T., Padylla, C., Schaefer, I.: Scalability of deductive verification depends on method call treatment. In: 8th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation (ISoLA). LNCS, Springer, Heidelberg (2018, to appear)","DOI":"10.1007\/978-3-030-03427-6_15"},{"key":"3_CR16","series-title":"SECS","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-1-4615-5229-1_12","volume-title":"Behavioral Specifications of Businesses and Systems","author":"GT Leavens","year":"1999","unstructured":"Leavens, G.T., Baker, A.L., Ruby, C.: JML: a notation for detailed design. In: Kilov, H., Rumpe, B., Simmonds, I. (eds.) Behavioral Specifications of Businesses and Systems. SECS, vol. 523, pp. 175\u2013188. Springer, Boston (1999). https:\/\/doi.org\/10.1007\/978-1-4615-5229-1_12"},{"issue":"3","key":"3_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"GT Leavens","year":"2006","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)","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"key":"3_CR18","unstructured":"Leavens, G., et al.: JML Reference Manual, Department of Computer Science, Iowa State University, February 2007. http:\/\/www.jmlspecs.org"},{"key":"3_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/3-540-47764-0_11","volume-title":"Static Analysis","author":"K Rustan","year":"2001","unstructured":"Rustan, K., Leino, M.: Applications of extended static checking. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 185\u2013193. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-47764-0_11"},{"key":"3_CR20","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 Moura de","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_CR21","doi-asserted-by":"crossref","unstructured":"Th\u00fcm, T., Meinicke, J., Benduhn, F., Hentschel, M., von Rhein, A., Saake, G.: Potential synergies of theorem proving and model checking for software product lines. In: Proceedings of the 18th International Software Product Line Conference, SPLC 2014, vol. 1, pp. 177\u2013186. ACM (2014)","DOI":"10.1145\/2648511.2648530"},{"key":"3_CR22","unstructured":"Wei\u00df, B.: Deductive verification of object-oriented software: dynamic frames, dynamic logic and predicate abstraction. Ph.D. thesis, Karlsruhe Institute of Technology (2011)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-98938-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,22]],"date-time":"2019-10-22T01:01:20Z","timestamp":1571706080000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-98938-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319989372","9783319989389"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-98938-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]}}}