{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:09:40Z","timestamp":1750306180779,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":13,"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.2970303","type":"proceedings-article","created":{"date-parts":[[2016,8,26]],"date-time":"2016-08-26T12:40:09Z","timestamp":1472215209000},"page":"403-413","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["An empirical evaluation of two user interfaces of an interactive program verifier"],"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","series-title":"LNCS","first-page":"101","volume-title":"Post Conf. Proc. 5th International Symposium on Formal Methods for Components and Objects (FMCO)","author":"Ahrendt W.","unstructured":"W. Ahrendt , B. Beckert , R. H\u00e4hnle , P. R\u00fcmmer , and P. H. Schmitt . Verifying object-oriented programs with KeY: a tutorial . In F. de Boer, M. M. Bonsangue, S. Graf, and W. de Roever, editors, Post Conf. Proc. 5th International Symposium on Formal Methods for Components and Objects (FMCO) , volume 4709 of LNCS , pages 70\u2013 101 . Springer-Verlag, 2007. W. Ahrendt, B. Beckert, R. H\u00e4hnle, P. R\u00fcmmer, and P. H. Schmitt. Verifying object-oriented programs with KeY: a tutorial. In F. de Boer, M. M. Bonsangue, S. Graf, and W. de Roever, editors, Post Conf. Proc. 5th International Symposium on Formal Methods for Components and Objects (FMCO), volume 4709 of LNCS, pages 70\u2013101. Springer-Verlag, 2007."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1006\/jsco.1997.0175"},{"key":"e_1_3_2_1_4_1","volume-title":"Software Engineering and Formal Methods - SEFM 2014 Collocated Workshops: HOFM, SAFOME, OpenCert, MoKMaSD, WS-FMDS","author":"Beckert B.","year":"2014","unstructured":"B. Beckert , S. Grebing , and F. B\u00f6hl . A Usability Evaluation of Interactive Theorem Provers Using Focus Groups . In Software Engineering and Formal Methods - SEFM 2014 Collocated Workshops: HOFM, SAFOME, OpenCert, MoKMaSD, WS-FMDS , Grenoble, France , September 1-2, 2014 , Revised Selected Papers, pages 3\u2013 19, 2014. B. Beckert, S. Grebing, and F. B\u00f6hl. A Usability Evaluation of Interactive Theorem Provers Using Focus Groups. In Software Engineering and Formal Methods - SEFM 2014 Collocated Workshops: HOFM, SAFOME, OpenCert, MoKMaSD, WS-FMDS, Grenoble, France, September 1-2, 2014, Revised Selected Papers, pages 3\u2013 19, 2014."},{"key":"e_1_3_2_1_5_1","volume-title":"Report of project COMM 641","author":"Cheney J.","year":"2001","unstructured":"J. Cheney . Project Report: Theorem Prover Usability. Technical report , Report of project COMM 641 , 2001 . J. Cheney. Project Report: Theorem Prover Usability. Technical report, Report of project COMM 641, 2001."},{"issue":"1","key":"e_1_3_2_1_6_1","doi-asserted-by":"crossref","first-page":"50","DOI":"10.1080\/00031305.1989.10475612","volume":"43","author":"Frigge M.","year":"1989","unstructured":"M. Frigge , D. C. Hoaglin , and B. Iglewicz . Some Implementations of the Boxplot. The American Statistician , 43 ( 1 ): 50 \u2013 54 , 1989 . M. Frigge, D. C. Hoaglin, and B. Iglewicz. Some Implementations of the Boxplot. The American Statistician, 43(1):50\u201354, 1989.","journal-title":"Some Implementations of the Boxplot. The American Statistician"},{"key":"e_1_3_2_1_8_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_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2970276.2970292"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001650050052"},{"key":"e_1_3_2_1_11_1","volume-title":"Proc. 11th Annual Workshop of the Psychology of Programming Interest Group","author":"Kadoda G.","year":"1996","unstructured":"G. Kadoda , R. Stone , and D. Diaper . Desirable features of educational theorem provers - a Cognitive Dimensions viewpoint . In Proc. 11th Annual Workshop of the Psychology of Programming Interest Group , 1996 . G. Kadoda, R. Stone, and D. Diaper. Desirable features of educational theorem provers - a Cognitive Dimensions viewpoint. In Proc. 11th Annual Workshop of the Psychology of Programming Interest Group, 1996."},{"key":"e_1_3_2_1_12_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_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/1791547"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/2349018"}],"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.2970303","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2970276.2970303","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.2970303"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,8,25]]},"references-count":13,"alternative-id":["10.1145\/2970276.2970303","10.1145\/2970276"],"URL":"https:\/\/doi.org\/10.1145\/2970276.2970303","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"}}]}}