{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:37:25Z","timestamp":1759639045209},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642540127"},{"type":"electronic","value":"9783642540134"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54013-4_1","type":"book-chapter","created":{"date-parts":[[2014,1,3]],"date-time":"2014-01-03T01:08:09Z","timestamp":1388711289000},"page":"1-20","source":"Crossref","is-referenced-by-count":57,"title":["SAT-Based Synthesis Methods for Safety Specs"],"prefix":"10.1007","author":[{"given":"Roderick","family":"Bloem","sequence":"first","affiliation":[]},{"given":"Robert","family":"K\u00f6nighofer","sequence":"additional","affiliation":[]},{"given":"Martina","family":"Seidl","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"370","DOI":"10.1007\/978-3-642-33386-6_29","volume-title":"Automated Technology for Verification and Analysis","author":"B. Becker","year":"2012","unstructured":"Becker, B., Ehlers, R., Lewis, M., Marin, P.: ALLQBF solving by computational learning. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol.\u00a07561, pp. 370\u2013384. Springer, Heidelberg (2012)"},{"key":"1_CR2","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.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"1_CR3","unstructured":"Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): Handbook of Satisfiability. FAIA, vol. 185. IOS Press (2009)"},{"issue":"4","key":"1_CR4","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2007.09.004","volume":"190","author":"R. Bloem","year":"2007","unstructured":"Bloem, R., Galler, S.J., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: Hardware from PSL. Electronic Notes in Theoretical Computer Science\u00a0190(4), 3\u201316 (2007)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"1_CR5","unstructured":"Bloem, R., K\u00f6nighofer, R., Seidl, M.: SAT-based synthesis methods for safety specs. CoRR, abs\/1311.3530 (2013), \n                  \n                    http:\/\/arxiv.org\/abs\/1311.3530"},{"key":"1_CR6","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":"A.R. Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R. Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: An academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 24\u201340. Springer, Heidelberg (2010)"},{"key":"1_CR8","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.\u00a06174, pp. 365\u2013379. Springer, Heidelberg (2010)"},{"key":"1_CR9","unstructured":"Ehlers, R., K\u00f6nighofer, R., Hofferek, G.: Symbolically synthesizing small circuits. In: FMCAD 2012, pp. 91\u2013100. IEEE (2012)"},{"issue":"1-3","key":"1_CR10","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1016\/j.scico.2007.01.015","volume":"69","author":"M.D. Ernst","year":"2007","unstructured":"Ernst, M.D., Perkins, J.H., Guo, P.J., McCamant, S., Pacheco, C., Tschantz, M.S., Xiao, C.: The Daikon system for dynamic detection of likely invariants. Sci. Comput. Program.\u00a069(1-3), 35\u201345 (2007)","journal-title":"Sci. Comput. Program."},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-02658-4_22","volume-title":"Computer Aided Verification","author":"E. Filiot","year":"2009","unstructured":"Filiot, E., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 263\u2013277. Springer, Heidelberg (2009)"},{"key":"1_CR12","unstructured":"Fr\u00f6hlich, A., Kovasznai, G., Biere, A.: A DPLL algorithm for solving DQBF. In: Pragmatics of SAT (PoS 2012, aff. to SAT 2012) (2012)"},{"key":"1_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-21581-0_19","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"M. Janota","year":"2011","unstructured":"Janota, M., Marques-Silva, J.: Abstraction-based algorithm for 2QBF. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 230\u2013244. Springer, Heidelberg (2011)"},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Jiang, J.-H.R., Lin, H.-P., Hung, W.-L.: Interpolating functions from large boolean relations. In: International Conference on Computer-Aided Design (ICCAD 2009), pp. 779\u2013784. IEEE (2009)","DOI":"10.1145\/1687399.1687544"},{"key":"1_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-642-02777-2_5","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"A. Kojevnikov","year":"2009","unstructured":"Kojevnikov, A., Kulikov, A.S., Yaroslavtsev, G.: Finding efficient circuits using SAT-solvers. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol.\u00a05584, pp. 32\u201344. Springer, Heidelberg (2009)"},{"key":"1_CR16","unstructured":"K\u00f6nighofer, R., Bloem, R.: Automated error localization and correction for imperative programs. In: FMCAD 2011, pp. 91\u2013100. IEEE (2011)"},{"key":"1_CR17","series-title":"LNAI","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K. Korovin","year":"2008","unstructured":"Korovin, K.: iProver \u2013 an instantiation-based theorem prover for first-order logic (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 292\u2013298. Springer, Heidelberg (2008)"},{"issue":"3","key":"1_CR18","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1016\/0022-0000(80)90027-6","volume":"21","author":"H.R. Lewis","year":"1980","unstructured":"Lewis, H.R.: Complexity results for classes of quantificational formulas. J. Comput. Syst. Sci.\u00a021(3), 317\u2013353 (1980)","journal-title":"J. Comput. Syst. Sci."},{"issue":"2-3","key":"1_CR19","first-page":"71","volume":"7","author":"F. Lonsing","year":"2010","unstructured":"Lonsing, F., Biere, A.: DepQBF: A dependency-aware QBF solver. JSAT\u00a07(2-3), 71\u201376 (2010)","journal-title":"JSAT"},{"key":"1_CR20","unstructured":"Moon, I., Kukula, J.H., Shiple, T.R., Somenzi, F.: Least fixpoint approximations for reachability analysis. In: ICCAD 1999, pp. 41\u201344. IEEE (1999)"},{"key":"1_CR21","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.\u00a07940, pp. 177\u2013191. Springer, Heidelberg (2013)"},{"key":"1_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"430","DOI":"10.1007\/978-3-642-31612-8_33","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2012","author":"A. Niemetz","year":"2012","unstructured":"Niemetz, A., Preiner, M., Lonsing, F., Seidl, M., Biere, A.: Resolution-based certificate extraction for QBF (tool presentation). In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol.\u00a07317, pp. 430\u2013435. Springer, Heidelberg (2012)"},{"issue":"3","key":"1_CR23","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1016\/S0747-7171(86)80028-1","volume":"2","author":"D.A. Plaisted","year":"1986","unstructured":"Plaisted, D.A., Greenbaum, S.: A structure-preserving clause form translation. J. Symb. Comput.\u00a02(3), 293\u2013304 (1986)","journal-title":"J. Symb. Comput."},{"issue":"1","key":"1_CR24","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/0004-3702(87)90062-2","volume":"32","author":"R. Reiter","year":"1987","unstructured":"Reiter, R.: A theory of diagnosis from first principles. Artif. Intell.\u00a032(1), 57\u201395 (1987)","journal-title":"Artif. Intell."},{"key":"1_CR25","unstructured":"Seidl, M., K\u00f6nighofer, R.: Partial witnesses from preprocessed quantified Boolean formulas. In: DATE 2014 (to appear, 2014)"},{"key":"1_CR26","unstructured":"Seidl, M., Lonsing, F., Biere, A.: qbf2epr: A tool for generating EPR formulas from QBF. In: Workshop on Practical Aspects of Automated Reasoning (2012)"},{"key":"1_CR27","doi-asserted-by":"crossref","unstructured":"Sohail, S., Somenzi, F.: Safety first: A two-stage algorithm for LTL games. In: FMCAD 2009, pp. 77\u201384. IEEE (2009)","DOI":"10.1109\/FMCAD.2009.5351138"},{"key":"1_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-10672-9_3","volume-title":"Programming Languages and Systems","author":"A. Solar-Lezama","year":"2009","unstructured":"Solar-Lezama, A.: The sketching approach to program synthesis. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol.\u00a05904, pp. 4\u201313. Springer, Heidelberg (2009)"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-72788-0_34","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2007","author":"S. Staber","year":"2007","unstructured":"Staber, S., Bloem, R.: Fault localization and correction with QBF. In: Marques-Silva, J., Sakallah, K.A. (eds.) SAT 2007. LNCS, vol.\u00a04501, pp. 355\u2013368. Springer, Heidelberg (2007)"},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-59042-0_57","volume-title":"STACS 95","author":"W. Thomas","year":"1995","unstructured":"Thomas, W.: On the synthesis of strategies in infinite games. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol.\u00a0900, pp. 1\u201313. Springer, Heidelberg (1995)"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54013-4_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,25]],"date-time":"2019-05-25T23:44:03Z","timestamp":1558827843000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54013-4_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642540127","9783642540134"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54013-4_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}