{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T03:23:33Z","timestamp":1742959413788,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319999265"},{"type":"electronic","value":"9783319999272"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"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":[[2018]]},"DOI":"10.1007\/978-3-319-99927-2_4","type":"book-chapter","created":{"date-parts":[[2018,9,6]],"date-time":"2018-09-06T17:39:50Z","timestamp":1536255590000},"page":"39-55","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["JMCTest: Automatically Testing Inter-Method Contracts in Java"],"prefix":"10.1007","author":[{"given":"Paul","family":"B\u00f6rding","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan","family":"Haltermann","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marie-Christine","family":"Jakobs","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Heike","family":"Wehrheim","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,9,7]]},"reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-12154-3_4","volume-title":"Verified Software: Theories, Tools and Experiments","author":"W Ahrendt","year":"2014","unstructured":"Ahrendt, W., et al.: The KeY platform for verification and analysis of Java programs. In: Giannakopoulou, D., Kroening, D. (eds.) VSTTE 2014. LNCS, vol. 8471, pp. 55\u201371. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-12154-3_4"},{"issue":"5","key":"4_CR2","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1109\/MS.2008.130","volume":"25","author":"N Ayewah","year":"2008","unstructured":"Ayewah, N., Hovemeyer, D., Morgenthaler, J.D., Penix, J., Pugh, W.: Using static analysis to find bugs. IEEE 25(5), 22\u201329 (2008). https:\/\/doi.org\/10.1109\/MS.2008.130","journal-title":"IEEE"},{"key":"4_CR3","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":"2","key":"4_CR4","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1016\/S1571-0661(04)00247-6","volume":"55","author":"D Bartetzko","year":"2001","unstructured":"Bartetzko, D., Fischer, C., M\u00f6ller, M., Wehrheim, H.: Jass - Java with assertions. Electr. Notes Theor. Comput. Sci. 55(2), 103\u2013117 (2001). https:\/\/doi.org\/10.1016\/S1571-0661(04)00247-6","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-642-22110-1_16","volume-title":"Computer Aided Verification","author":"D Beyer","year":"2011","unstructured":"Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184\u2013190. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_16"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"428","DOI":"10.1007\/11813040_29","volume-title":"FM 2006: Formal Methods","author":"F Bouquet","year":"2006","unstructured":"Bouquet, F., Dadeau, F., Legeard, B.: Automated boundary test generation from JML specifications. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 428\u2013443. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11813040_29"},{"issue":"4","key":"4_CR7","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1145\/566171.566191","volume":"27","author":"Chandrasekhar Boyapati","year":"2002","unstructured":"Boyapati, C., Khurshid, S., Marinov, D.: Korat: automated testing based on Java predicates. In: ISSTA, pp. 123\u2013133. ACM (2002). http:\/\/doi.acm.org\/10.1145\/566172.566191","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"key":"4_CR8","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_16"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-68237-0_18","volume-title":"FM 2008: Formal Methods","author":"P Chalin","year":"2008","unstructured":"Chalin, P., Rioux, F.: JML runtime assertion checking: improved error reporting and efficiency using strong validity. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 246\u2013261. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-68237-0_18"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"320","DOI":"10.1007\/978-3-540-30502-6_23","volume-title":"Advances in Computer Science - ASIAN 2004. Higher-Level Decision Making","author":"TY Chen","year":"2004","unstructured":"Chen, T.Y., Leung, H., Mak, I.K.: Adaptive random testing. In: Maher, M.J. (ed.) ASIAN 2004. LNCS, vol. 3321, pp. 320\u2013329. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30502-6_23"},{"key":"4_CR11","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_10"},{"key":"4_CR12","unstructured":"Cheon, Y.: Automated random testing to detect specification-code inconsistencies. In: Karras, D. (ed.) Conference on Software Engineering Theory and Practice, pp. 112\u2013119. International Society for Research in Science and Technology (2007)"},{"key":"4_CR13","unstructured":"Cheon, Y., Leavens, G.T.: A runtime assertion checker for the Java Modeling Language (JML). In: Conference on Software Engineering Research and Practice, pp. 322\u2013328. CSREA Press (2002)"},{"key":"4_CR14","unstructured":"Cheon, Y., Rubio-Medrano, C.E.: Random test data generation for Java classes annotated with JML specifications. In: Arabnia, H.R., Reza, H. (eds.) Conference on Software Engineering Research and Practice, pp. 385\u2013391. CSREA Press (2007)"},{"issue":"9","key":"4_CR15","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1145\/357766.351266","volume":"35","author":"Koen Claessen","year":"2000","unstructured":"Claessen, K., Hughes, J.: QuickCheck: a lightweight tool for random testing of Haskell programs. In: ICFP, pp. 268\u2013279. ACM (2000). http:\/\/doi.acm.org\/10.1145\/351240.351266","journal-title":"ACM SIGPLAN Notices"},{"issue":"11","key":"4_CR16","doi-asserted-by":"publisher","first-page":"1025","DOI":"10.1002\/spe.602","volume":"34","author":"C Csallner","year":"2004","unstructured":"Csallner, C., Smaragdakis, Y.: JCrasher: an automatic robustness tester for Java. Softw. Pract. Exper. 34(11), 1025\u20131050 (2004). https:\/\/doi.org\/10.1002\/spe.602","journal-title":"Softw. Pract. Exper."},{"key":"4_CR17","doi-asserted-by":"publisher","unstructured":"Dahlweid, M., Moskal, M., Santen, T., Tobies, S., Schulte, W.: VCC: contract-based modular verification of concurrent C. In: ICSE, pp. 429\u2013430. IEEE (2009). https:\/\/doi.org\/10.1109\/ICSE-COMPANION.2009.5071046","DOI":"10.1109\/ICSE-COMPANION.2009.5071046"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-642-24580-0_6","volume-title":"Testing Software and Systems","author":"I Enderlin","year":"2011","unstructured":"Enderlin, I., Dadeau, F., Giorgetti, A., Ben Othman, A.: Praspel: a specification language for contract-based testing in PHP. In: Wolff, B., Za\u00efdi, F. (eds.) ICTSS 2011. LNCS, vol. 7019, pp. 64\u201379. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-24580-0_6"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-15769-1_2","volume-title":"Static Analysis","author":"M F\u00e4hndrich","year":"2010","unstructured":"F\u00e4hndrich, M.: Static verification for code contracts. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 2\u20135. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15769-1_2"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"F\u00e4hndrich, M., Barnett, M., Logozzo, F.: Embedded contract languages. In: SAC, pp. 2103\u20132110. ACM (2010). http:\/\/doi.acm.org\/10.1145\/1774088.1774531","DOI":"10.1145\/1774088.1774531"},{"issue":"1","key":"4_CR21","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1007\/BF00260922","volume":"10","author":"JV Guttag","year":"1978","unstructured":"Guttag, J.V., Horning, J.J.: The algebraic specification of abstract data types. Acta Informatica 10(1), 27\u201352 (1978). https:\/\/doi.org\/10.1007\/BF00260922","journal-title":"Acta Informatica"},{"issue":"12","key":"4_CR22","doi-asserted-by":"publisher","first-page":"92","DOI":"10.1145\/1052883.1052895","volume":"39","author":"D Hovemeyer","year":"2004","unstructured":"Hovemeyer, D., Pugh, W.: Finding bugs is easy. SIGPLAN Not. 39(12), 92\u2013106 (2004). http:\/\/doi.acm.org\/10.1145\/1052883.1052895","journal-title":"SIGPLAN Not."},{"key":"4_CR23","unstructured":"JUnit: Junit4 (2012\u20132017). http:\/\/junit.org\/junit4\/"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/3-540-48443-4_18","volume-title":"Meta-Level Architectures and Reflection","author":"M Karaorman","year":"1999","unstructured":"Karaorman, M., H\u00f6lzle, U., Bruno, J.: jContractor: a reflective java library to support design by contract. In: Cointe, P. (ed.) Reflection 1999. LNCS, vol. 1616, pp. 175\u2013196. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48443-4_18"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Keil, M., Thiemann, P.: TreatJS: higher-order contracts for JavaScripts. In: Boyland, J.T. (ed.) ECOOP. LIPIcs, vol. 37, pp. 28\u201351. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2015). https:\/\/doi.org\/10.4230\/LIPIcs.ECOOP.2015.28","DOI":"10.4230\/LIPIcs.ECOOP.2015.28"},{"issue":"3","key":"4_CR26","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. SIGSOFT Softw. Eng. Notes 31(3), 1\u201338 (2006). http:\/\/doi.acm.org\/10.1145\/1127878.1127884","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Lin, Y., Tang, X., Chen, Y., Zhao, J.: A divergence-oriented approach to adaptive random testing of Java programs. In: ASE, pp. 221\u2013232. IEEE (2009). https:\/\/doi.org\/10.1109\/ASE.2009.13","DOI":"10.1109\/ASE.2009.13"},{"key":"4_CR28","doi-asserted-by":"publisher","unstructured":"Meyer, B.: Design by contract: the Eiffel method. In: TOOLS, p. 446. IEEE (1998). https:\/\/doi.org\/10.1109\/TOOLS.1998.711043","DOI":"10.1109\/TOOLS.1998.711043"},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/11558569_18","volume-title":"Quality of Software Architectures and Software Quality","author":"C Oriat","year":"2005","unstructured":"Oriat, C.: Jartege: a tool for random generation of unit tests for Java classes. In: Reussner, R., Mayer, J., Stafford, J.A., Overhage, S., Becker, S., Schroeder, P.J. (eds.) QoSA\/SOQUA -2005. LNCS, vol. 3712, pp. 242\u2013256. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11558569_18"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Pacheco, C., Lahiri, S.K., Ernst, M.D., Ball, T.: Feedback-directed random test generation. In: ICSE, pp. 75\u201384. IEEE Computer Society (2007). http:\/\/doi.acm.org\/10.1145\/1297846.1297902","DOI":"10.1109\/ICSE.2007.37"},{"key":"4_CR31","doi-asserted-by":"publisher","unstructured":"Ploesch, R.: Design by contract for Python. In: APSEC, pp. 213\u2013219. IEEE (1997). https:\/\/doi.org\/10.1109\/APSEC.1997.640178","DOI":"10.1109\/APSEC.1997.640178"},{"key":"4_CR32","doi-asserted-by":"publisher","unstructured":"Pradel, M., Gross, T.R.: Automatic testing of sequential and concurrent substitutability. In: ICSE, pp. 282\u2013291. IEEE (2013). https:\/\/doi.org\/10.1109\/ICSE.2013.6606574","DOI":"10.1109\/ICSE.2013.6606574"},{"issue":"5","key":"4_CR33","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1145\/1095430.1081749","volume":"30","author":"Nikolai Tillmann","year":"2005","unstructured":"Tillmann, N., Schulte, W.: Parameterized unit tests. In: FSE, pp. 253\u2013262. ACM (2005). http:\/\/doi.acm.org\/10.1145\/1081706.1081749","journal-title":"ACM SIGSOFT Software Engineering Notes"},{"issue":"2","key":"4_CR34","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1023\/A:1022920129859","volume":"10","author":"W Visser","year":"2003","unstructured":"Visser, W., Havelund, K., Brat, G.P., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203\u2013232 (2003). https:\/\/doi.org\/10.1023\/A:1022920129859","journal-title":"Autom. Softw. Eng."},{"issue":"1","key":"4_CR35","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1145\/356596.356598","volume":"4","author":"P Wegner","year":"1972","unstructured":"Wegner, P.: The Vienna definition language. ACM Comput. Surv. 4(1), 5\u201363 (1972). http:\/\/doi.acm.org\/10.1145\/356596.356598","journal-title":"ACM Comput. Surv."},{"key":"4_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-540-24617-6_6","volume-title":"Formal Approaches to Software Testing","author":"G Xu","year":"2004","unstructured":"Xu, G., Yang, Z.: JMLAutoTest: a novel automated testing framework based on JML and JUnit. In: Petrenko, A., Ulrich, A. (eds.) FATES 2003. LNCS, vol. 2931, pp. 70\u201385. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24617-6_6"}],"container-title":["Lecture Notes in Computer Science","Testing Software and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-99927-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T01:11:26Z","timestamp":1659316286000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-99927-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319999265","9783319999272"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-99927-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"7 September 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ICTSS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"IFIP International Conference on Testing Software and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"C\u00e1diz","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Spain","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 October 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 October 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"pts2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ictss2018.uca.es\/ictss","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}