{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:19:42Z","timestamp":1750220382749,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":19,"publisher":"ACM","license":[{"start":{"date-parts":[[2021,7,11]],"date-time":"2021-07-11T00:00:00Z","timestamp":1625961600000},"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":[[2021,7,13]]},"DOI":"10.1145\/3464971.3468421","type":"proceedings-article","created":{"date-parts":[[2021,7,8]],"date-time":"2021-07-08T22:07:03Z","timestamp":1625782023000},"page":"24-31","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Reconstructing z3 proofs in KeY: there and back again"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9478-9641","authenticated-orcid":false,"given":"Wolfram","family":"Pfeifer","sequence":"first","affiliation":[{"name":"KIT, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9882-8177","authenticated-orcid":false,"given":"Jonas","family":"Schiffl","sequence":"additional","affiliation":[{"name":"KIT, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2350-1831","authenticated-orcid":false,"given":"Mattias","family":"Ulbrich","sequence":"additional","affiliation":[{"name":"KIT, Germany"}]}],"member":"320","published-online":{"date-parts":[[2021,7,11]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-49812-6"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-25379-9_12"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22110-1_14"},{"volume-title":"The SMT-LIB Standard: Version 2.6. Department of Computer Science","author":"Barrett Clark","key":"e_1_3_2_1_4_1","unstructured":"Clark Barrett , Pascal Fontaine , and Cesare Tinelli . 2017. The SMT-LIB Standard: Version 2.6. Department of Computer Science , The University of Iowa . Available at www.smt-lib.org Clark Barrett, Pascal Fontaine, and Cesare Tinelli. 2017. The SMT-LIB Standard: Version 2.6. Department of Computer Science, The University of Iowa. Available at www.smt-lib.org"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_34"},{"key":"e_1_3_2_1_6_1","unstructured":"Fr\u00e9d\u00e9ric Besson Pascal Fontaine and Laurent Th\u00e9ry. 2011. A flexible proof format for SMT: A proposal.  Fr\u00e9d\u00e9ric Besson Pascal Fontaine and Laurent Th\u00e9ry. 2011. A flexible proof format for SMT: A proposal."},{"key":"e_1_3_2_1_7_1","volume-title":"7th International Workshop on Satisfiability Modulo Theories (SMT\u201909)","author":"B\u00f6hme Sascha","year":"2009","unstructured":"Sascha B\u00f6hme . 2009 . Proof reconstruction for Z3 in Isabelle\/HOL . In 7th International Workshop on Satisfiability Modulo Theories (SMT\u201909) . Sascha B\u00f6hme. 2009. Proof reconstruction for Z3 in Isabelle\/HOL. In 7th International Workshop on Satisfiability Modulo Theories (SMT\u201909)."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_12"},{"volume-title":"Proving Theorems of Higher-Order Logic with SMT Solvers. Technische Universit\u00e4t M\u00fcnchen","author":"B\u00f6hme Sascha","key":"e_1_3_2_1_9_1","unstructured":"Sascha B\u00f6hme . 2012. Proving Theorems of Higher-Order Logic with SMT Solvers. Technische Universit\u00e4t M\u00fcnchen . M\u00fcnchen . Sascha B\u00f6hme. 2012. Proving Theorems of Higher-Order Logic with SMT Solvers. Technische Universit\u00e4t M\u00fcnchen. M\u00fcnchen."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_1_11_1","volume-title":"LPAR Workshops. CEUR Workshop Proceedings, 418","author":"de Moura Leonardo Mendon\u00e7a","year":"2008","unstructured":"Leonardo Mendon\u00e7a de Moura and Nikolaj Bj\u00f8rner . 2008 . Proofs and Refutations, and Z3 . In LPAR Workshops. CEUR Workshop Proceedings, 418 , 123\u2013132. Leonardo Mendon\u00e7a de Moura and Nikolaj Bj\u00f8rner. 2008. Proofs and Refutations, and Z3. In LPAR Workshops. CEUR Workshop Proceedings, 418, 123\u2013132."},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_11"},{"key":"e_1_3_2_1_13_1","volume-title":"Formal Underpinnings of Java Workshop (at OOPSLA\u201998)","author":"Leavens Gary T.","year":"1998","unstructured":"Gary T. Leavens , Albert L. Baker , and Clyde Ruby . 1998 . JML: a Java modeling language . In Formal Underpinnings of Java Workshop (at OOPSLA\u201998) . 404\u2013420. Gary T. Leavens, Albert L. Baker, and Clyde Ruby. 1998. JML: a Java modeling language. In Formal Underpinnings of Java Workshop (at OOPSLA\u201998). 404\u2013420."},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_26"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5445\/IR\/1000131835"},{"key":"e_1_3_2_1_16_1","unstructured":"Andrew Reynolds Cesare Tinelli Aaron Stump Liana Hadarean Yeting Ge and Clark Barrett. 2010. CVC3 Proof Conversion to LFSC.  Andrew Reynolds Cesare Tinelli Aaron Stump Liana Hadarean Yeting Ge and Clark Barrett. 2010. CVC3 Proof Conversion to LFSC."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89439-1_20"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.12.121"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0163-3"}],"event":{"name":"ISSTA '21: 30th ACM SIGSOFT International Symposium on Software Testing and Analysis","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Virtual Denmark","acronym":"ISSTA '21"},"container-title":["Proceedings of the 23rd ACM International Workshop on Formal Techniques for Java-like Programs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3464971.3468421","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3464971.3468421","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:25Z","timestamp":1750191505000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3464971.3468421"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,11]]},"references-count":19,"alternative-id":["10.1145\/3464971.3468421","10.1145\/3464971"],"URL":"https:\/\/doi.org\/10.1145\/3464971.3468421","relation":{},"subject":[],"published":{"date-parts":[[2021,7,11]]},"assertion":[{"value":"2021-07-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}