{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T21:08:33Z","timestamp":1725916113852},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319703886"},{"type":"electronic","value":"9783319703893"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"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":[[2017]]},"DOI":"10.1007\/978-3-319-70389-3_11","type":"book-chapter","created":{"date-parts":[[2017,11,11]],"date-time":"2017-11-11T09:42:30Z","timestamp":1510393350000},"page":"163-178","source":"Crossref","is-referenced-by-count":2,"title":["An Interaction Concept for Program Verification Systems with Explicit Proof Object"],"prefix":"10.1007","author":[{"given":"Bernhard","family":"Beckert","sequence":"first","affiliation":[]},{"given":"Sarah","family":"Grebing","sequence":"additional","affiliation":[]},{"given":"Mattias","family":"Ulbrich","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2017,11,12]]},"reference":[{"key":"11_CR1","unstructured":"H\u00e4hnle, R., Huisman, M.: Deductive software verification: From pen-and-paper proofs to industrial tools. LNCS, vol. 10000 (2017)"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Ahrendt, W., Beckert, B., Bubel, R., H\u00e4hnle, R., Schmitt, P.H., Ulbrich, M., eds.: Deductive Software Verification - The KeY Book: From Theory to Practice. LNCS, vol. 10001. Springer, Cham (2016)","DOI":"10.1007\/978-3-319-49812-6"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Beckert, B., Grebing, S., B\u00f6hl, F.: How to put usability into focus: Using focus groups to evaluate the usability of interactive theorem provers. In: Benzm\u00fcller, C., Woltzenlogel Paleo, B. (eds.): UITP 2014. EPTCS , vol. 167, pp. 4\u201313 (July 2014)","DOI":"10.4204\/EPTCS.167.3"},{"key":"11_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-15201-1_1","volume-title":"Software Engineering and Formal Methods","author":"B Beckert","year":"2015","unstructured":"Beckert, B., Grebing, S., B\u00f6hl, F.: A usability evaluation of interactive theorem provers using focus groups. In: Canal, C., Idani, A. (eds.) SEFM 2014. LNCS, vol. 8938, pp. 3\u201319. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-15201-1_1"},{"issue":"3","key":"11_CR5","first-page":"1","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\/SEN 31(3), 1\u201338 (2006)","journal-title":"SIGSOFT\/SEN"},{"key":"11_CR6","doi-asserted-by":"crossref","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M. (eds.) Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer (2002)","DOI":"10.1007\/3-540-45949-9"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Castran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions, 1st edn. Texts in Theoretical Computer Science An EATCS Series. Springer-Verlag, Berlin Heidelberg (2004)","DOI":"10.1007\/978-3-662-07964-5"},{"key":"11_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar \u2014 A generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 167\u2013183. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48256-3_12"},{"issue":"3","key":"11_CR9","doi-asserted-by":"crossref","first-page":"261","DOI":"10.1007\/s10817-015-9360-2","volume":"56","author":"D Matichuk","year":"2016","unstructured":"Matichuk, D., Murray, T., Wenzel, M.: Eisbach: A proof method language for isabelle. Journal of Automated Reasoning 56(3), 261\u2013282 (2016)","journal-title":"Journal of Automated Reasoning"},{"issue":"9","key":"11_CR10","doi-asserted-by":"crossref","first-page":"87","DOI":"10.1145\/2544174.2500579","volume":"48","author":"B Ziliani","year":"2013","unstructured":"Ziliani, B., Dreyer, D., Krishnaswami, N.R., Nanevski, A., Vafeiadis, V.: Mtac: A monad for typed tactic programming in coq. SIGPLAN Not. 48(9), 87\u2013100 (2013)","journal-title":"SIGPLAN Not."},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-319-46750-4_19","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2016","author":"S Obua","year":"2016","unstructured":"Obua, S., Scott, P., Fleuriot, J.: ProofScript: Proof scripting for the masses. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 333\u2013348. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46750-4_19"},{"key":"11_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"573","DOI":"10.1007\/978-3-662-49674-9_37","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"Y Lin","year":"2016","unstructured":"Lin, Y., Le Bras, P., Grov, G.: Developing and debugging proof strategies by tinkering. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 573\u2013579. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49674-9_37"},{"key":"11_CR13","unstructured":"Hentschel, M.: Integrating Symbolic Execution, Debugging and Verification. PhD thesis, Technische Universit\u00e4t Darmstadt (January 2016)"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-70389-3_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,5]],"date-time":"2019-10-05T21:29:35Z","timestamp":1570310975000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-70389-3_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319703886","9783319703893"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-70389-3_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}