{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T04:18:26Z","timestamp":1749010706176,"version":"3.41.0"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319415390"},{"type":"electronic","value":"9783319415406"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-41540-6_20","type":"book-chapter","created":{"date-parts":[[2016,7,12]],"date-time":"2016-07-12T09:34:07Z","timestamp":1468316047000},"page":"364-382","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":8,"title":["A SAT-Based Counterexample Guided Method for Unbounded Synthesis"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Legg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nina","family":"Narodytska","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leonid","family":"Ryzhyk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,7,13]]},"reference":[{"key":"20_CR1","unstructured":"Syntcomp 2015 results. http:\/\/syntcomp.cs.unisaarland.de\/syntcomp2015\/experiments\/ . Accessed 29 Jan 2016"},{"key":"20_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"197","DOI":"10.1007\/978-3-319-09284-3_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2014","author":"G Audemard","year":"2014","unstructured":"Audemard, G., Simon, L.: Lazy clause exchange policy for parallel SAT solvers. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 197\u2013205. Springer, Heidelberg (2014)"},{"key":"20_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"20_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-54013-4_1","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Bloem","year":"2014","unstructured":"Bloem, R., K\u00f6nighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 1\u201320. Springer, Heidelberg (2014)"},{"key":"20_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"AR Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"key":"20_CR6","doi-asserted-by":"crossref","first-page":"100","DOI":"10.4204\/EPTCS.157.11","volume":"157","author":"Romain Brenguier","year":"2014","unstructured":"Brenguier, R., P\u00e9rez, G.A., Raskin, J., Sankur, O.: AbsSynthe: abstract synthesis from succinct safety specifications. In: Workshop on Synthesis, SYNT, pp. 100\u2013116 (2014)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"20_CR7","doi-asserted-by":"crossref","unstructured":"Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: $$10^{20}$$ states and beyond. In: Symposium on Logic in Computer Science, pp. 428\u2013439 (1990)","DOI":"10.1109\/LICS.1990.113767"},{"key":"20_CR8","doi-asserted-by":"crossref","unstructured":"Chiang, T.W., Jiang, J.H.R.: Property-directed synthesis of reactive systems from safety specifications. In: Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design, ICCAD 2015, pp. 794\u2013801 (2015)","DOI":"10.1109\/ICCAD.2015.7372652"},{"issue":"3","key":"20_CR9","doi-asserted-by":"publisher","first-page":"250","DOI":"10.2307\/2963593","volume":"22","author":"W Craig","year":"1957","unstructured":"Craig, W.: Linear reasoning. A new form of the Herbrand-Gentzen theorem. J. Symb. Log. 22(3), 250\u2013268 (1957)","journal-title":"J. Symb. Log."},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"E\u00e8n, N., Legg, A., Narodytska, N., Ryzhyk, L.: SAT-based strategy extraction in reachability games. In: AAAI Conference on Artificial Intelligences, AAAI, pp. 3738\u20133745 (2015)","DOI":"10.1609\/aaai.v29i1.9752"},{"key":"20_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-642-14295-6_33","volume-title":"Computer Aided Verification","author":"R Ehlers","year":"2010","unstructured":"Ehlers, R.: Symbolic bounded synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 365\u2013379. Springer, Heidelberg (2010)"},{"key":"20_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-642-27940-9_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Finkbeiner","year":"2012","unstructured":"Finkbeiner, B., Jacobs, S.: Lazy synthesis. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 219\u2013234. Springer, Heidelberg (2012)"},{"issue":"5\u20136","key":"20_CR13","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. Softw. Tools Technol. Transf. STTT 15(5\u20136), 519\u2013539 (2013)","journal-title":"Softw. Tools Technol. Transf. STTT"},{"key":"20_CR14","unstructured":"Jacobs, S., Bloem, R., Brenguier, R., Ehlers, R., Hell, T., K\u00f6nighofer, R., P\u00e9rez, G.A., Raskin, J., Ryzhyk, L., Sankur, O., Seidl, M., Tentrup, L., Walker, A.: The first reactive synthesis competition (SYNTCOMP 2014). Computing Research Repository, CoRR abs\/1506.08726 (2015). http:\/\/arxiv.org\/abs\/1506.08726"},{"key":"20_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/3-540-45657-0_19","volume-title":"Computer Aided Verification","author":"KL McMillan","year":"2002","unstructured":"McMillan, K.L.: Applying SAT methods in unbounded symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 250\u2013264. Springer, Heidelberg (2002)"},{"key":"20_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-24605-3_1","volume-title":"Theory and Applications of Satisfiability Testing","author":"MR Dransfield","year":"2004","unstructured":"Dransfield, M.R., Marek, V.W., Truszczy\u0144ski, M.: Satisfiability and computing van der Waerden numbers. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 1\u201313. Springer, Heidelberg (2004)"},{"key":"20_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1007\/978-3-642-38613-8_13","volume-title":"Integrated Formal Methods","author":"A Morgenstern","year":"2013","unstructured":"Morgenstern, A., Gesell, M., Schneider, K.: Solving games using incremental induction. In: Johnsen, E.B., Petre, L. (eds.) IFM 2013. LNCS, vol. 7940, pp. 177\u2013191. Springer, Heidelberg (2013)"},{"key":"20_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"533","DOI":"10.1007\/978-3-319-08867-9_35","volume-title":"Computer Aided Verification","author":"N Narodytska","year":"2014","unstructured":"Narodytska, N., Legg, A., Bacchus, F., Ryzhyk, L., Walker, A.: Solving games without controllable predecessor. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 533\u2013540. Springer, Heidelberg (2014)"},{"key":"20_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11609773_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N Piterman","year":"2006","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364\u2013380. Springer, Heidelberg (2006)"},{"issue":"3","key":"20_CR20","doi-asserted-by":"publisher","first-page":"981","DOI":"10.2307\/2275583","volume":"62","author":"P Pudl\u00e1k","year":"1997","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log. 62(3), 981\u2013998 (1997)","journal-title":"J. Symb. Log."},{"key":"20_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"683","DOI":"10.1007\/978-3-642-45221-5_45","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"SF Rollini","year":"2013","unstructured":"Rollini, S.F., Alt, L., Fedyukovich, G., Hyv\u00e4rinen, A.E.J., Sharygina, N.: PeRIPLO: a framework for producing effective interpolants in SAT-based software verification. In: McMillan, K., Middeldorp, A., Voronkov, A. (eds.) LPAR-19 2013. LNCS, vol. 8312, pp. 683\u2013693. Springer, Heidelberg (2013)"},{"key":"20_CR22","doi-asserted-by":"crossref","unstructured":"Walker, A., Ryzhyk, L.: Predicate abstraction for reactive synthesis. In: Formal Methods in Computer-Aided Design FMCAD, pp. 219\u2013226 (2014)","DOI":"10.1109\/FMCAD.2014.6987617"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-41540-6_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,4]],"date-time":"2025-06-04T00:41:29Z","timestamp":1748997689000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-41540-6_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319415390","9783319415406"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-41540-6_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]},"assertion":[{"value":"13 July 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Toronto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2016","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17 July 2016","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 July 2016","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2016","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}