{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,23]],"date-time":"2024-10-23T01:42:27Z","timestamp":1729647747340,"version":"3.28.0"},"reference-count":35,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013,5]]},"DOI":"10.1109\/formalise.2013.6612272","type":"proceedings-article","created":{"date-parts":[[2013,10,1]],"date-time":"2013-10-01T14:41:05Z","timestamp":1380638465000},"page":"15-21","source":"Crossref","is-referenced-by-count":1,"title":["Functional SMT solving with Z3 and racket"],"prefix":"10.1109","author":[{"given":"Siddharth","family":"Agarwal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Amey","family":"Karkare","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"journal-title":"Numbermind","year":"0","author":"agarwal","key":"19"},{"key":"35","article-title":"Structure and interpretation of computer programs","author":"abelson","year":"1996","journal-title":"The MIT Press 2nd Edition"},{"key":"17","first-page":"25","article-title":"Mastermind is NP-Complete","volume":"5","author":"stuckman","year":"2006","journal-title":"INFOCOMP Journal of Computer Science"},{"journal-title":"Problem 185-Project Euler","year":"0","author":"hughes","key":"18"},{"journal-title":"Gecode Generic Constraint Development Environment","year":"0","key":"33"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993514"},{"journal-title":"JaCoP - Java Constraint Programming Solver","year":"0","key":"34"},{"key":"16","first-page":"1","article-title":"The Computer as a Master Mind","volume":"9","author":"knuth","year":"1976","journal-title":"Journal of Recreational Mathematics"},{"key":"13","article-title":"The SMT-lib standard: Version 2.0","author":"barrett","year":"2010","journal-title":"Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh England)"},{"journal-title":"Reference Racket","year":"2010","author":"flatt","key":"14"},{"key":"11","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1007\/s10009-008-0091-0","article-title":"Bounded model checking of software using SMT solvers instead of SAT solvers","volume":"11","author":"armando","year":"2009","journal-title":"STTT"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73368-3_34"},{"key":"21","article-title":"Fifth revised report on the algorithmic language scheme","volume":"33","author":"kelsey","year":"1998","journal-title":"ACM SIGPLAN Notices"},{"journal-title":"The Racket Foreign Interface","year":"0","author":"barzilay","key":"20"},{"journal-title":"Web Applications in Racket","year":"0","author":"mccarthy","key":"22"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291178"},{"key":"24","first-page":"306","article-title":"Complete instantiation for quantified formulas in satisfiability modulo theories","author":"ge","year":"2009","journal-title":"CAV"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.2307\/2274706"},{"key":"26","first-page":"183","article-title":"Efficient e-matching for smt solvers","author":"de moura","year":"2007","journal-title":"CADE-21"},{"key":"27","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_23"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22438-6_30"},{"journal-title":"Z3Py-Python Interface for the Z3 Theorem Prover","year":"0","author":"research","key":"29"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1145\/378795.378846"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4684-2001-2_9"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2008.109"},{"key":"1","doi-asserted-by":"publisher","DOI":"10.1145\/800157.805047"},{"journal-title":"Symbolic Bit Vectors Bit-precise Verification and Automatic C-code Generation","year":"0","author":"erkok","key":"30"},{"year":"0","key":"7"},{"key":"6","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","article-title":"Cvc4","author":"barrett","year":"2011","journal-title":"Proceedings of the 23rd International Conference on Computer Aided Verification Ser CAV'11"},{"journal-title":"Racklog Prolog-Style Logic Programming","year":"0","author":"sitaram","key":"32"},{"key":"5","article-title":"The yices smt solver","author":"dutertre","year":"2006","journal-title":"SRI International"},{"journal-title":"Yices-painless An Embedded Language for Programming the Yices SMT Solver","year":"0","author":"stewart","key":"31"},{"key":"4","article-title":"Z3: An efficient SMT Solver","volume":"4963","author":"de moura","year":"2008","journal-title":"TACAS Ser LNCS"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375616"},{"key":"8","first-page":"175","article-title":"DPLL(T): Fast decision procedures","volume":"3114","author":"ganzinger","year":"2004","journal-title":"CAV Ser LNCS"}],"event":{"name":"2013 1st FME Workshop on Formal Methods in Software Engineering (FormaliSE)","start":{"date-parts":[[2013,5,25]]},"location":"San Francisco, CA, USA","end":{"date-parts":[[2013,5,25]]}},"container-title":["2013 1st FME Workshop on Formal Methods in Software Engineering (FormaliSE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6596468\/6612266\/06612272.pdf?arnumber=6612272","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,7,27]],"date-time":"2019-07-27T22:13:21Z","timestamp":1564265601000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6612272\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,5]]},"references-count":35,"URL":"https:\/\/doi.org\/10.1109\/formalise.2013.6612272","relation":{},"subject":[],"published":{"date-parts":[[2013,5]]}}}