{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:09:41Z","timestamp":1750306181091,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":14,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,8,25]],"date-time":"2016-08-25T00:00:00Z","timestamp":1472083200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,8,25]]},"DOI":"10.1145\/2970276.2970292","type":"proceedings-article","created":{"date-parts":[[2016,8,26]],"date-time":"2016-08-26T12:40:09Z","timestamp":1472215209000},"page":"846-851","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["The interactive verification debugger: effective understanding of interactive proof attempts"],"prefix":"10.1145","author":[{"given":"Martin","family":"Hentschel","sequence":"first","affiliation":[{"name":"TU Darmstadt, Germany"}]},{"given":"Reiner","family":"H\u00e4hnle","sequence":"additional","affiliation":[{"name":"TU Darmstadt, Germany"}]},{"given":"Richard","family":"Bubel","sequence":"additional","affiliation":[{"name":"TU Darmstadt, Germany"}]}],"member":"320","published-online":{"date-parts":[[2016,8,25]]},"reference":[{"key":"e_1_3_2_1_1_1","series-title":"LNCS","first-page":"71","volume-title":"Verified Software: Theories, Tools and Experiments","author":"Ahrendt W.","unstructured":"W. Ahrendt , B. Beckert , D. Bruns , R. Bubel , C. Gladisch , S. Grebing , R. H\u00e4hnle , M. Hentschel , M. Herda , V. Klebanov , W. Mostowski , C. Scheben , P. Schmitt , and M. Ulbrich . The KeY Platform for Verification and Analysis of Java Programs . In D. Giannakopoulou and D. Kroening, editors, Verified Software: Theories, Tools and Experiments , volume 8471 of LNCS , pages 55\u2013 71 . Springer, 2014. W. Ahrendt, B. Beckert, D. Bruns, R. Bubel, C. Gladisch, S. Grebing, R. H\u00e4hnle, M. Hentschel, M. Herda, V. Klebanov, W. Mostowski, C. Scheben, P. Schmitt, and M. Ulbrich. The KeY Platform for Verification and Analysis of Java Programs. In D. Giannakopoulou and D. Kroening, editors, Verified Software: Theories, Tools and Experiments, volume 8471 of LNCS, pages 55\u201371. Springer, 2014."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/390016.808445"},{"key":"e_1_3_2_1_3_1","volume-title":"Elsevier\/North-Holland","author":"Burstall R. M.","year":"1974","unstructured":"R. M. Burstall . Program proving as hand simulation with a little induction. In Information Processing \u201974, pages 308\u2013312 . Elsevier\/North-Holland , 1974 . R. M. Burstall. Program proving as hand simulation with a little induction. In Information Processing \u201974, pages 308\u2013312. Elsevier\/North-Holland, 1974."},{"key":"e_1_3_2_1_5_1","series-title":"LNCS","first-page":"262","volume-title":"Runtime Verification, 14th International Conference","author":"Hentschel M.","unstructured":"M. Hentschel , R. Bubel , and R. H\u00e4hnle . Symbolic Execution Debugger (SED) . In B. Bonakdarpour and S. A. Smolka, editors, Runtime Verification, 14th International Conference , RV , Toronto, Canada , volume 8734 of LNCS , pages 255\u2013 262 . Springer, 2014. M. Hentschel, R. Bubel, and R. H\u00e4hnle. Symbolic Execution Debugger (SED). In B. Bonakdarpour and S. A. Smolka, editors, Runtime Verification, 14th International Conference, RV, Toronto, Canada, volume 8734 of LNCS, pages 255\u2013262. Springer, 2014."},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970303"},{"key":"e_1_3_2_1_7_1","series-title":"LNCS","first-page":"70","volume-title":"Integrated Formal Methods","author":"Hentschel M.","unstructured":"M. Hentschel , S. K\u00e4sdorf , R. H\u00e4hnle , and R. Bubel . An Interactive Verification Tool Meets an IDE . In E. Albert and E. Sekerinski, editors, Integrated Formal Methods , volume 8739 of LNCS , pages 55\u2013 70 . Springer, 2014. M. Hentschel, S. K\u00e4sdorf, R. H\u00e4hnle, and R. Bubel. An Interactive Verification Tool Meets an IDE. In E. Albert and E. Sekerinski, editors, Integrated Formal Methods, volume 8739 of LNCS, pages 55\u201370. Springer, 2014."},{"key":"e_1_3_2_1_9_1","series-title":"LNCS","first-page":"311","volume-title":"Programming Languages and Systems","author":"Jacobs B.","unstructured":"B. Jacobs , J. Smans , and F. Piessens . A Quick Tour of the VeriFast Program Verifier . In K. Ueda, editor, Programming Languages and Systems , volume 6461 of LNCS , pages 304\u2013 311 . Springer, 2010. B. Jacobs, J. Smans, and F. Piessens. A Quick Tour of the VeriFast Program Verifier. In K. Ueda, editor, Programming Languages and Systems, volume 6461 of LNCS, pages 304\u2013311. Springer, 2010."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/800027.808434"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360252"},{"key":"e_1_3_2_1_12_1","first-page":"414","volume-title":"Proceedings of the 9th International Conference on Software Engineering and Formal Methods, SEFM\u201911","author":"Le Goues C.","year":"2011","unstructured":"C. Le Goues , K. R. M. Leino , and M. Moskal . The Boogie Verification Debugger . In Proceedings of the 9th International Conference on Software Engineering and Formal Methods, SEFM\u201911 , pages 407\u2013 414 , Berlin, Heidelberg , 2011 . Springer-Verlag. C. Le Goues, K. R. M. Leino, and M. Moskal. The Boogie Verification Debugger. In Proceedings of the 9th International Conference on Software Engineering and Formal Methods, SEFM\u201911, pages 407\u2013414, Berlin, Heidelberg, 2011. Springer-Verlag."},{"key":"e_1_3_2_1_13_1","first-page":"2344","author":"Leavens G. T.","year":"2013","unstructured":"G. T. Leavens , E. Poll , C. Clifton , Y. Cheon , C. Ruby , D. Cok , P. M\u00fcller , J. Kiniry , P. Chalin , D. M. Zimmerman , and W. Dietl . JML Reference Manual , May 31, 2013 . Draft Revision 2344 . G. T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby, D. Cok, P. M\u00fcller, J. Kiniry, P. Chalin, D. M. Zimmerman, and W. Dietl. JML Reference Manual, May 31, 2013. Draft Revision 2344.","journal-title":"JML Reference Manual"},{"key":"e_1_3_2_1_14_1","volume-title":"Usable Verification Workshop (UV)","author":"Leino K. R. M.","year":"2010","unstructured":"K. R. M. Leino and M. Moskal . Usable Auto-Active verification. In T. Ball, L. Zuck, and N. Shankar, editors , Usable Verification Workshop (UV) , Redmond, WA, USA , 2010 . K. R. M. Leino and M. Moskal. Usable Auto-Active verification. In T. Ball, L. Zuck, and N. Shankar, editors, Usable Verification Workshop (UV), Redmond, WA, USA, 2010."},{"key":"e_1_3_2_1_15_1","series-title":"Applied Logic Series","first-page":"39","volume-title":"Automated Deduction \u2014 A Basis for Applications","author":"Reif W.","unstructured":"W. Reif , G. Schellhorn , K. Stenzel , and M. Balser . Structured specifications and interactive proofs with KIV . In W. Bibel and P. Schmitt, editors, Automated Deduction \u2014 A Basis for Applications , volume 9 of Applied Logic Series , pages 13\u2013 39 . Springer, 1998. W. Reif, G. Schellhorn, K. Stenzel, and M. Balser. Structured specifications and interactive proofs with KIV. In W. Bibel and P. Schmitt, editors, Automated Deduction \u2014 A Basis for Applications, volume 9 of Applied Logic Series, pages 13\u201339. Springer, 1998."},{"key":"e_1_3_2_1_16_1","unstructured":"Introduction Creating and Managing Proofs Inspecting Proofs Completing Proofs Related Work Conclusion Acknowledgments References  Introduction Creating and Managing Proofs Inspecting Proofs Completing Proofs Related Work Conclusion Acknowledgments References"}],"event":{"name":"ASE'16: ACM\/IEEE International Conference on Automated Software Engineering","sponsor":["SIGAI ACM Special Interest Group on Artificial Intelligence","SIGSOFT ACM Special Interest Group on Software Engineering","IEEE-CS Computer Society"],"location":"Singapore Singapore","acronym":"ASE'16"},"container-title":["Proceedings of the 31st IEEE\/ACM International Conference on Automated Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2970276.2970292","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2970276.2970292","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T03:50:00Z","timestamp":1750218600000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2970276.2970292"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,8,25]]},"references-count":14,"alternative-id":["10.1145\/2970276.2970292","10.1145\/2970276"],"URL":"https:\/\/doi.org\/10.1145\/2970276.2970292","relation":{},"subject":[],"published":{"date-parts":[[2016,8,25]]},"assertion":[{"value":"2016-08-25","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}