{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T03:09:31Z","timestamp":1725937771215},"reference-count":18,"publisher":"Open Publishing Association","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Electron. Proc. Theor. Comput. Sci.","EPTCS"],"DOI":"10.4204\/eptcs.296.7","type":"journal-article","created":{"date-parts":[[2019,7,8]],"date-time":"2019-07-08T11:33:15Z","timestamp":1562585595000},"page":"42-47","source":"Crossref","is-referenced-by-count":10,"title":["Ultimate TreeAutomizer (CHC-COMP Tool Description)"],"prefix":"10.4204","volume":"296","author":[{"given":"Daniel","family":"Dietsch","sequence":"first","affiliation":[{"name":"University of Freiburg"}]},{"given":"Matthias","family":"Heizmann","sequence":"additional","affiliation":[{"name":"University of Freiburg"}]},{"given":"Jochen","family":"Hoenicke","sequence":"additional","affiliation":[{"name":"University of Freiburg"}]},{"given":"Alexander","family":"Nutz","sequence":"additional","affiliation":[{"name":"University of Freiburg"}]},{"given":"Andreas","family":"Podelski","sequence":"additional","affiliation":[{"name":"University of Freiburg"}]}],"member":"2720","published-online":{"date-parts":[[2019,7,9]]},"reference":[{"key":"DBLP:conf\/wia\/AbdullaKH06","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1137\/0216062","article-title":"Bisimulation Minimization of Tree Automata","volume-title":"CIAA","volume":"4094","author":"Abdulla","year":"2006"},{"key":"DBLP:conf\/cav\/BarrettCDHJKRT11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/3-540-45657-0_40","article-title":"CVC4","volume-title":"CAV","volume":"6806","author":"Barrett","year":"2011"},{"key":"DBLP:conf\/birthday\/BjornerGMR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-319-19249-9","article-title":"Horn Clause Solvers for Program Verification","volume-title":"Fields of Logic and Computation II","volume":"9300","author":"Bj\u00f8rner","year":"2015"},{"key":"DBLP:conf\/spin\/ChristHN12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/11532231_26","article-title":"SMTInterpol: An Interpolating SMT Solver","volume-title":"SPIN","volume":"7385","author":"Christ","year":"2012"},{"key":"DBLP:conf\/tacas\/CimattiGSS13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-31365-3_38","article-title":"The MathSAT5 SMT Solver","volume-title":"TACAS","volume":"7795","author":"Cimatti","year":"2013"},{"key":"DBLP:conf\/cav\/ClarkeGJLV00","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/3-540-49519-3_18","article-title":"Counterexample-Guided Abstraction Refinement","volume-title":"CAV","volume":"1855","author":"Clarke","year":"2000"},{"key":"DBLP:conf\/sigsoft\/DietschHMNP17","doi-asserted-by":"publisher","first-page":"487","DOI":"10.1145\/3106237.3106307","article-title":"Craig vs. Newton in software model checking","volume-title":"ESEC\/SIGSOFT FSE","author":"Dietsch","year":"2017"},{"key":"DBLP:conf\/fmcad\/EenMB11","first-page":"125","article-title":"Efficient implementation of property directed reachability","volume-title":"FMCAD","author":"E\u00e9n","year":"2011"},{"key":"DBLP:conf\/tacas\/GrebenshchikovGLPR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"549","DOI":"10.1007\/978-3-540-69611-7_16","article-title":"HSF(C): A Software Verifier Based on Horn Clauses - (Competition Contribution)","volume-title":"TACAS","volume":"7214","author":"Grebenshchikov","year":"2012"},{"key":"DBLP:conf\/pldi\/GrebenshchikovLPR12","doi-asserted-by":"publisher","first-page":"405","DOI":"10.1145\/2254064.2254112","article-title":"Synthesizing software verifiers from proof rules","volume-title":"PLDI","author":"Grebenshchikov","year":"2012"},{"key":"DBLP:conf\/sas\/HeizmannHP09","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-540-73368-3_46","article-title":"Refinement of Trace Abstraction","volume-title":"SAS","volume":"5673","author":"Heizmann","year":"2009"},{"key":"DBLP:conf\/popl\/HeizmannHP10","doi-asserted-by":"publisher","first-page":"471","DOI":"10.1145\/1706299.1706353","article-title":"Nested interpolants","volume-title":"POPL","author":"Heizmann","year":"2010"},{"key":"DBLP:conf\/sat\/HoderB12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"157","DOI":"10.1007\/3-540-49481-2_26","article-title":"Generalized Property Directed Reachability","volume-title":"SAT","volume":"7317","author":"Hoder","year":"2012"},{"key":"DBLP:conf\/popl\/HoenickeMP17","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1145\/3009837.3009893","article-title":"Thread modularity at many levels: a pearl in compositional verification","volume-title":"POPL","author":"Hoenicke","year":"2017"},{"key":"DBLP:conf\/vmcai\/KafleG15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-52753-2_52","article-title":"Tree Automata-Based Refinement with Application to Horn Clause Verification","volume-title":"VMCAI","volume":"8931","author":"Kafle","year":"2015"},{"key":"DBLP:conf\/cav\/KafleGM16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1016\/j.jsc.2010.06.005","article-title":"Rahft: A Tool for Verifying Horn Clauses Using Abstract Interpretation and Finite Tree Automata","volume-title":"CAV (1)","volume":"9779","author":"Kafle","year":"2016"},{"key":"DBLP:conf\/tacas\/MouraB08","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1109\/MS.2006.117","article-title":"Z3: An Efficient SMT Solver","volume-title":"TACAS","volume":"4963","author":"de Moura","year":"2008"},{"issue":"8","key":"DBLP:journals\/cj\/WangJ16","doi-asserted-by":"publisher","first-page":"1236","DOI":"10.1145\/69575.69577","article-title":"Trace Abstraction Refinement for Solving Horn Clauses","volume":"59","author":"Wang","year":"2016","journal-title":"Comput. J."}],"container-title":["Electronic Proceedings in Theoretical Computer Science"],"original-title":[],"language":"en","deposited":{"date-parts":[[2019,7,11]],"date-time":"2019-07-11T01:24:00Z","timestamp":1562808240000},"score":1,"resource":{"primary":{"URL":"http:\/\/arxiv.org\/abs\/1907.03998v1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,9]]},"references-count":18,"URL":"https:\/\/doi.org\/10.4204\/eptcs.296.7","relation":{},"ISSN":["2075-2180"],"issn-type":[{"value":"2075-2180","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,9]]}}}