{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T11:07:02Z","timestamp":1770289622783,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642214363","type":"print"},{"value":"9783642214370","type":"electronic"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-21437-0_8","type":"book-chapter","created":{"date-parts":[[2011,6,18]],"date-time":"2011-06-18T07:33:16Z","timestamp":1308382396000},"page":"73-87","source":"Crossref","is-referenced-by-count":25,"title":["Using Debuggers to Understand Failed Verification Attempts"],"prefix":"10.1007","author":[{"given":"Peter","family":"M\u00fcller","sequence":"first","affiliation":[]},{"given":"Joseph N.","family":"Ruskiewicz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"8_CR1","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1145\/604131.604140","volume-title":"POPL","author":"T. Ball","year":"2003","unstructured":"Ball, T., Naik, M., Rajamani, S.K.: From symptom to cause: Localizing errors in counterexample traces. In: POPL, pp. 97\u2013105. ACM, New York (2003)"},{"key":"8_CR2","first-page":"326","volume-title":"ICSE","author":"D. Beyer","year":"2004","unstructured":"Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., Majumbar, R.: Generating tests from counterexamples. In: ICSE, pp. 326\u2013335. IEEE, Los Alamitos (2004)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"168","DOI":"10.1007\/978-3-540-24730-2_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.M. Clarke","year":"2004","unstructured":"Clarke, E.M., Kroening, D., Lerda, F.: A tool for checking ANSI C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 168\u2013176. Springer, Heidelberg (2004)"},{"key":"8_CR4","first-page":"422","volume-title":"ICSE","author":"C. Csallner","year":"2005","unstructured":"Csallner, C., Smaragdakis, Y.: Check \u2019n\u2019 Crash: Combining static checking and testing. In: ICSE, pp. 422\u2013431. ACM, New York (2005)"},{"issue":"5","key":"8_CR5","doi-asserted-by":"publisher","first-page":"59","DOI":"10.5381\/jot.2006.5.5.a3","volume":"5","author":"\u00c1. Darvas","year":"2006","unstructured":"Darvas, \u00c1., M\u00fcller, P.: Reasoning about method calls in interface specifications. Journal of Object Technology\u00a05(5), 59\u201385 (2006)","journal-title":"Journal of Object Technology"},{"key":"8_CR6","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.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"8_CR7","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Technical Report HPL-2003-148, HP Laboratories, Palo Alto (2003)"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-24730-2_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Groce","year":"2004","unstructured":"Groce, A.: Error explanation with distance metrics. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 108\u2013122. Springer, Heidelberg (2004)"},{"key":"8_CR9","first-page":"143","volume-title":"ASE","author":"R. H\u00e4hnle","year":"2010","unstructured":"H\u00e4hnle, R., Baum, M., Bubel, R., Rothe, M.: A visual interactive debugger based on symbolic execution. In: ASE, pp. 143\u2013146. ACM, New York (2010)"},{"key":"8_CR10","first-page":"56","volume-title":"ASE","author":"R.J. Hall","year":"2004","unstructured":"Hall, R.J., Zisman, A.: Validating personal requirements by assisted symbolic behavior browsing. In: ASE, pp. 56\u201366. IEEE, Los Alamitos (2004)"},{"key":"8_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/978-3-642-13010-6_4","volume-title":"Advanced Lectures on Software Engineering","author":"K.R.M. Leino","year":"2010","unstructured":"Leino, K.R.M., M\u00fcller, P.: Using the spec# language, methodology, and tools to write bug-free programs. In: M\u00fcller, P. (ed.) LASER Summer School 2007\/2008. LNCS, vol.\u00a06029, pp. 91\u2013139. Springer, Heidelberg (2010)"},{"key":"8_CR12","unstructured":"Rayside, D., Chang, F.S.-H., Dennis, G., Seater, R., Jackson, D.: Automatic visualization of relational logic models. ECEASST\u00a07 (2007)"},{"key":"8_CR13","first-page":"365","volume-title":"ASE","author":"N. Tillman","year":"2006","unstructured":"Tillman, N., Schulte, W.: Mock-object generation with behavior. In: ASE, pp. 365\u2013368. IEEE, Los Alamitos (2006)"},{"key":"8_CR14","unstructured":"Tip, F.: A survey of program slicing techniques. Journal of Programming Languages\u00a03(3) (1995)"},{"issue":"1","key":"8_CR15","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1145\/249094.249108","volume":"31","author":"A. Zeller","year":"1996","unstructured":"Zeller, A., L\u00fctkehaus, D.: DDD\u2014a free graphical front-end for UNIX debuggers. SIGPLAN Notices\u00a031(1), 22\u201327 (1996)","journal-title":"SIGPLAN Notices"}],"container-title":["Lecture Notes in Computer Science","FM 2011: Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-21437-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,7]],"date-time":"2023-06-07T13:31:14Z","timestamp":1686144674000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-21437-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642214363","9783642214370"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-21437-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011]]}}}