{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,18]],"date-time":"2025-05-18T18:21:05Z","timestamp":1747592465325},"reference-count":11,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2015,5,7]],"date-time":"2015-05-07T00:00:00Z","timestamp":1430956800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2015,6]]},"DOI":"10.1007\/s10817-015-9328-2","type":"journal-article","created":{"date-parts":[[2015,5,6]],"date-time":"2015-05-06T08:11:31Z","timestamp":1430899891000},"page":"61-90","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["The 2013 Evaluation of SMT-COMP and SMT-LIB"],"prefix":"10.1007","volume":"55","author":[{"given":"David R.","family":"Cok","sequence":"first","affiliation":[]},{"given":"Aaron","family":"Stump","sequence":"additional","affiliation":[]},{"given":"Tjark","family":"Weber","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,5,7]]},"reference":[{"key":"9328_CR1","unstructured":"Aziz, M.A.: A novel portfolio solver for satisfiability modulo theory problems (2013)"},{"key":"9328_CR2","unstructured":"Aziz, M.A., Wassal, A., Darwish, N.: A machine learning technique for hardness estimation of QFBV SMT problems (work in progress). In: SMT Workshop 2012 10th International Workshop on Satisfiability Modulo Theories SMT-COMP 2012, p. 56 (2012)"},{"key":"9328_CR3","doi-asserted-by":"crossref","unstructured":"Barrett, C., Deters, M., de Moura, L., Oliveras, A.: A stump. 6 years of SMT-COMP (2012)","DOI":"10.1007\/s10817-012-9246-5"},{"key":"9328_CR4","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. In: Gupta, A, Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, England) (2010)"},{"key":"9328_CR5","doi-asserted-by":"crossref","unstructured":"Le Berre, D., Simon, L.: The essentials of the SAT 2003 competition. In: Sixth international conference on theory and applications of satisfiability testing, vol. 2919 of LNCS, pp. 452\u2013467. Springer (2003)","DOI":"10.1007\/978-3-540-24605-3_34"},{"issue":"2\u20133","key":"9328_CR6","first-page":"79","volume":"15","author":"FJ Pelletier","year":"2002","unstructured":"Pelletier, F.J., Sutcliffe, G., Suttner, C.B.: The Development of CASC. AI Communications 15(2\u20133), 79\u201390 (2002)","journal-title":"AI Communications"},{"key":"9328_CR7","doi-asserted-by":"crossref","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: StarExec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Proceedings of the 7th international joint conference on automated reasoning, Lecture Notes in Artificial Intelligence. Springer (2014)","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"9328_CR8","unstructured":"Sutcliffe, G.: The CADE ATP System Competition Design and Organization., http:\/\/www.cs.miami.edu\/tptp\/CASC\/24\/Design.html#Evaluation"},{"key":"9328_CR9","unstructured":"Federated logic conference (FLoC) olympic games. http:\/\/vsl2014.at\/olympics\/"},{"key":"9328_CR10","unstructured":"The SMT-COMP web site provides results of the SMT competition and links to the system descriptions of the participants., http:\/\/smtcomp.org"},{"key":"9328_CR11","unstructured":"StarExec web site., http:\/\/www.starexec.org"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9328-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-015-9328-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-015-9328-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,8,24]],"date-time":"2019-08-24T16:54:25Z","timestamp":1566665665000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-015-9328-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,5,7]]},"references-count":11,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2015,6]]}},"alternative-id":["9328"],"URL":"https:\/\/doi.org\/10.1007\/s10817-015-9328-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,5,7]]}}}