{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:16:43Z","timestamp":1785543403448,"version":"3.56.0"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642141065","type":"print"},{"value":"9783642141072","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14107-2_26","type":"book-chapter","created":{"date-parts":[[2010,6,29]],"date-time":"2010-06-29T12:10:14Z","timestamp":1277813414000},"page":"552-576","source":"Crossref","is-referenced-by-count":22,"title":["Falling Back on Executable Specifications"],"prefix":"10.1007","author":[{"given":"Hesam","family":"Samimi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ei Darli","family":"Aung","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Todd","family":"Millstein","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"26_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Post Conference Proceedings of CASSIS: 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.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"26_CR2","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1145\/949305.949314","volume-title":"OOPSLA \u201903: Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications","author":"B. Demsky","year":"2003","unstructured":"Demsky, B., Rinard, M.: Automatic detection and repair of errors in data structures. In: OOPSLA \u201903: Proceedings of the 18th annual ACM SIGPLAN conference on Object-oriented programing, systems, languages, and applications, pp. 78\u201395. ACM, New York (2003)"},{"key":"26_CR3","first-page":"176","volume-title":"ICSE","author":"B. Demsky","year":"2005","unstructured":"Demsky, B., Rinard, M.C.: Data structure repair using goal-directed reasoning. In: Roman, G.-C., Griswold, W.G., Nuseibeh, B. (eds.) ICSE, pp. 176\u2013185. ACM, New York (2005)"},{"key":"26_CR4","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1145\/1146238.1146251","volume-title":"ISSTA \u201906: Proceedings of the 2006 international symposium on Software testing and analysis","author":"G. Dennis","year":"2006","unstructured":"Dennis, G., Chang, F.S.-H., Jackson, D.: Modular verification of code with sat. In: ISSTA \u201906: Proceedings of the 2006 international symposium on Software testing and analysis, pp. 109\u2013120. ACM, New York (2006)"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-540-87873-5_13","volume-title":"Verified Software: Theories, Tools, Experiments","author":"G. Dennis","year":"2008","unstructured":"Dennis, G., Yessenov, K., Jackson, D.: Bounded verification of voting software. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 130\u2013145. Springer, Heidelberg (2008)"},{"key":"26_CR6","unstructured":"Een, N., Sorensson, N.: MiniSat, \n                    \n                      http:\/\/minisat.se"},{"key":"26_CR7","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1145\/1321631.1321643","volume-title":"ASE","author":"B. Elkarablieh","year":"2007","unstructured":"Elkarablieh, B., Garcia, I., Suen, Y.L., Khurshid, S.: Assertion-based repair of complex data structures. In: Stirewalt, R.E.K., Egyed, A. (eds.) ASE, pp. 64\u201373. ACM, New York (2007)"},{"key":"26_CR8","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1145\/1368088.1368222","volume-title":"ICSE \u201908: Proceedings of the 30th international conference on Software engineering","author":"B. Elkarablieh","year":"2008","unstructured":"Elkarablieh, B., Khurshid, S.: Juzi: a tool for repairing complex data structures. In: ICSE \u201908: Proceedings of the 30th international conference on Software engineering, pp. 855\u2013858. ACM, New York (2008)"},{"key":"26_CR9","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1145\/1297027.1297056","volume-title":"OOPSLA \u201907: Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications","author":"B. Elkarablieh","year":"2007","unstructured":"Elkarablieh, B., Khurshid, S., Vu, D., McKinley, K.S.: Starc: static analysis for efficient repair of complex data. In: OOPSLA \u201907: Proceedings of the 22nd annual ACM SIGPLAN conference on Object-oriented programming systems and applications, pp. 387\u2013404. ACM, New York (2007)"},{"key":"26_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/504282.504283","volume-title":"OOPSLA \u201901: Proceedings of the 16th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications","author":"R.B. Findler","year":"2001","unstructured":"Findler, R.B., Felleisen, M.: Contract soundness for object-oriented languages. In: OOPSLA \u201901: Proceedings of the 16th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, pp. 1\u201315. ACM, New York (2001)"},{"key":"26_CR11","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1145\/512529.512558","volume-title":"PLDI \u201902: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation","author":"C. Flanagan","year":"2002","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: PLDI \u201902: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, pp. 234\u2013245. ACM, New York (2002)"},{"key":"26_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/BFb0053042","volume-title":"ECOOP \u201992 European Conference on Object-Oriented Programming","author":"B.N. Freeman-Benson","year":"1992","unstructured":"Freeman-Benson, B.N., Borning, A.: Integrating constraints with an object-oriented language. In: Lehrmann Madsen, O. (ed.) ECOOP 1992. LNCS, vol.\u00a0615, pp. 268\u2013286. Springer, Heidelberg (1992)"},{"key":"26_CR13","volume-title":"Java(TM) Language Specification","author":"J. Gosling","year":"2005","unstructured":"Gosling, J., Joy, B., Steele, G., Bracha, G.: Java(TM) Language Specification, 3rd edn. Addison-Wesley, Reading (2005)","edition":"3"},{"issue":"2","key":"26_CR14","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1145\/505145.505149","volume":"11","author":"D. Jackson","year":"2002","unstructured":"Jackson, D.: Alloy: a lightweight object modelling notation. ACM Trans. Softw. Eng. Methodol.\u00a011(2), 256\u2013290 (2002)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"26_CR15","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1145\/347324.383378","volume-title":"ISSTA \u201900: Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis","author":"D. Jackson","year":"2000","unstructured":"Jackson, D., Vaziri, M.: Finding bugs with a constraint solver. In: ISSTA \u201900: Proceedings of the 2000 ACM SIGSOFT international symposium on Software testing and analysis, pp. 14\u201325. ACM, New York (2000)"},{"key":"26_CR16","unstructured":"JChessBoard, \n                    \n                      http:\/\/jchessboard.sourceforge.net"},{"issue":"4","key":"26_CR17","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1023\/B:AUSE.0000038938.10589.b9","volume":"11","author":"S. Khurshid","year":"2004","unstructured":"Khurshid, S., Marinov, D.: Testera: Specification-based testing of java programs using sat. Autom. Softw. Eng.\u00a011(4), 403\u2013434 (2004)","journal-title":"Autom. Softw. Eng."},{"key":"26_CR18","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1145\/582419.582441","volume-title":"OOPSLA \u201902: Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications","author":"S. Khurshid","year":"2002","unstructured":"Khurshid, S., Marinov, D., Jackson, D.: An analyzable annotation language. In: OOPSLA \u201902: Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, pp. 231\u2013245. ACM, New York (2002)"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"King, J.C.: Symbolic execution and program testing. Commun. ACM\u00a019(7) (1976)","DOI":"10.1145\/360248.360252"},{"key":"26_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/978-3-540-70952-7_19","volume-title":"Formal Methods: Applications and Technology","author":"B. Krause","year":"2007","unstructured":"Krause, B., Wahls, T.: jmle: A tool for executing jml specifications via constraint programming. In: Brim, L., Haverkort, B.R., Leucker, M., van de Pol, J. (eds.) FMICS 2006 and PDMC 2006. LNCS, vol.\u00a04346, pp. 293\u2013296. Springer, Heidelberg (2007)"},{"issue":"3","key":"26_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1127878.1127884","volume":"31","author":"G.T. 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\u00a031(3), 1\u201338 (2006)","journal-title":"SIGSOFT Softw. Eng. Notes"},{"key":"26_CR22","first-page":"360","volume-title":"TOOLS","author":"B. Meyer","year":"1997","unstructured":"Meyer, B.: Design by contract: Making object-oriented programs that work. In: TOOLS (25), p. 360. IEEE Computer Society, Los Alamitos (1997)"},{"issue":"3","key":"26_CR23","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/44501.44503","volume":"10","author":"C. Morgan","year":"1988","unstructured":"Morgan, C.: The specification statement. ACM Trans. Program. Lang. Syst.\u00a010(3), 403\u2013419 (1988)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"26_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/3-540-36579-6_11","volume-title":"Compiler Construction","author":"N. Nystrom","year":"2003","unstructured":"Nystrom, N., Clarkson, M.R., Myers, A.C.: Polyglot: An extensible compiler framework for java. In: Hedin, G. (ed.) CC 2003. LNCS, vol.\u00a02622, pp. 138\u2013152. Springer, Heidelberg (2003)"},{"key":"26_CR25","doi-asserted-by":"publisher","first-page":"999","DOI":"10.1145\/1639950.1640070","volume-title":"OOPSLA \u201909: Proceeding of the 24th ACM SIGPLAN conference companion on Object oriented programming systems languages and applications","author":"D. Rayside","year":"2009","unstructured":"Rayside, D., Milicevic, A., Yessenov, K., Dennis, G., Jackson, D.: Agile specifications. In: OOPSLA \u201909: Proceeding of the 24th ACM SIGPLAN conference companion on Object oriented programming systems languages and applications, pp. 999\u20131006. ACM, New York (2009)"},{"key":"26_CR26","unstructured":"SweetHome3D, \n                    \n                      http:\/\/www.sweethome3d.eu"},{"key":"26_CR27","unstructured":"Torlak, E.: A constraint solver for software engineering: Finding models and cores of large relational specifications. Ph.D. dissertation, Massachusetts Institute of Technology (2009)"},{"key":"26_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/3-540-36577-X_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Vaziri","year":"2003","unstructured":"Vaziri, M., Jackson, D.: Checking properties of heap-manipulating procedures with a constraint solver. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol.\u00a02619, pp. 505\u2013520. Springer, Heidelberg (2003)"},{"issue":"4","key":"26_CR29","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1023\/A:1026554217992","volume":"7","author":"T. Wahls","year":"2000","unstructured":"Wahls, T., Leavens, G.T., Baker, A.L.: Executing formal specifications with concurrent constraint programming. Automated Software Engg.\u00a07(4), 315\u2013343 (2000)","journal-title":"Automated Software Engg."},{"key":"26_CR30","doi-asserted-by":"publisher","first-page":"349","DOI":"10.1145\/1375581.1375624","volume-title":"PLDI \u201908: Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"K. Zee","year":"2008","unstructured":"Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: PLDI \u201908: Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 349\u2013361. ACM, New York (2008)"},{"key":"26_CR31","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1145\/1542476.1542514","volume-title":"PLDI \u201909: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation","author":"K. Zee","year":"2009","unstructured":"Zee, K., Kuncak, V., Rinard, M.C.: An integrated proof language for imperative programs. In: PLDI \u201909: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 338\u2013351. ACM, New York (2009)"}],"container-title":["Lecture Notes in Computer Science","ECOOP 2010 \u2013 Object-Oriented Programming"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14107-2_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:18:59Z","timestamp":1619785139000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14107-2_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642141065","9783642141072"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14107-2_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}