{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T17:12:13Z","timestamp":1760202733148},"publisher-location":"Cham","reference-count":18,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319522333"},{"type":"electronic","value":"9783319522340"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-52234-0_4","type":"book-chapter","created":{"date-parts":[[2017,1,11]],"date-time":"2017-01-11T04:52:06Z","timestamp":1484110326000},"page":"55-72","source":"Crossref","is-referenced-by-count":10,"title":["Synthesizing Non-Vacuous Systems"],"prefix":"10.1007","author":[{"given":"Roderick","family":"Bloem","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hana","family":"Chockler","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Masoud","family":"Ebrahimi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ofer","family":"Strichman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,1,12]]},"reference":[{"key":"4_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-540-45069-6_35","volume-title":"Computer Aided Verification","author":"R Armoni","year":"2003","unstructured":"Armoni, R., Fix, L., Flaisher, A., Grumberg, O., Piterman, N., Tiemeyer, A., Vardi, M.Y.: Enhanced vacuity detection in linear temporal logic. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 368\u2013380. Springer, Heidelberg (2003). doi: 10.1007\/978-3-540-45069-6_35"},{"issue":"2","key":"4_CR2","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1023\/A:1008779610539","volume":"18","author":"I Beer","year":"2001","unstructured":"Beer, I., Ben-David, S., Eisner, C., Rodeh, Y.: Efficient detection of vacuity in ACTL formulas. Formal Methods Syst. Des. 18(2), 141\u2013163 (2001)","journal-title":"Formal Methods Syst. Des."},{"key":"4_CR3","doi-asserted-by":"crossref","first-page":"193","DOI":"10.1007\/s00236-013-0191-5","volume":"51","author":"R Bloem","year":"2014","unstructured":"Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T.A., Hofferek, G., Jobstmann, B., K\u00f6nighofer, B., K\u00f6nighofer, R.: Synthesizing robust systems. Acta Inf. 51, 193\u2013220 (2014)","journal-title":"Acta Inf."},{"key":"4_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02658-4_14","volume-title":"Computer Aided Verification","author":"R Bloem","year":"2009","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140\u2013156. Springer, Berlin (2009). doi: 10.1007\/978-3-642-02658-4_14"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/11560548_16","volume-title":"Correct Hardware Design and Verification Methods","author":"D Bustan","year":"2005","unstructured":"Bustan, D., Flaisher, A., Grumberg, O., Kupferman, O., Vardi, M.Y.: Regular vacuity. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol. 3725, pp. 191\u2013206. Springer, Heidelberg (2005). doi: 10.1007\/11560548_16"},{"key":"4_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-540-30494-4_22","volume-title":"Formal Methods in Computer-Aided Design","author":"A Gurfinkel","year":"2004","unstructured":"Gurfinkel, A., Chechik, M.: Extending extended vacuity. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 306\u2013321. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-30494-4_22"},{"issue":"3","key":"4_CR7","doi-asserted-by":"crossref","first-page":"552","DOI":"10.1007\/s10703-013-0192-6","volume":"43","author":"H Chockler","year":"2013","unstructured":"Chockler, H., Gurfinkel, A., Strichman, O.: Beyond vacuity: towards the strongest passing formula. Formal Methods Syst. Des. 43(3), 552\u2013571 (2013)","journal-title":"Formal Methods Syst. Des."},{"key":"4_CR8","unstructured":"Church, A.: Logic, arithmetics, and automata. In: ICM (1963)"},{"issue":"5","key":"4_CR9","first-page":"519","volume":"15","author":"B Finkbeiner","year":"2012","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transfer 15(5), 519\u2013539 (2012)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"4_CR10","doi-asserted-by":"crossref","unstructured":"Jacobs, S., Bloem, R., Brenguier, R., K\u00f6nighofer, R., P\u00e9rez, G.A., Raskin, J., Ryzhyk, L., Sankur, O., Seidl, M., Tentrup, L., Walker, A.: The second reactive synthesis competition. In: SYNT (2015)","DOI":"10.1007\/s10009-016-0416-3"},{"issue":"2","key":"4_CR11","doi-asserted-by":"crossref","first-page":"441","DOI":"10.1016\/j.jcss.2011.05.005","volume":"78","author":"B Jobstmann","year":"2012","unstructured":"Jobstmann, B., Staber, S., Griesmayer, A., Bloem, R.: Finding and fixing faults. J. Comput. Syst. Sci. 78(2), 441\u2013460 (2012)","journal-title":"J. Comput. Syst. Sci."},{"key":"4_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"928","DOI":"10.1007\/978-3-642-39799-8_66","volume-title":"Computer Aided Verification","author":"A Khalimov","year":"2013","unstructured":"Khalimov, A., Jacobs, S., Bloem, R.: PARTY parameterized synthesis of token rings. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 928\u2013933. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-39799-8_66"},{"issue":"2","key":"4_CR13","doi-asserted-by":"crossref","first-page":"224","DOI":"10.1007\/s100090100062","volume":"4","author":"O Kupferman","year":"2003","unstructured":"Kupferman, O., Vardi, M.: Vacuity detection in temporal model checking. J. Softw. Tools Technol. Transfer 4(2), 224\u2013233 (2003)","journal-title":"J. Softw. Tools Technol. Transfer"},{"key":"4_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-540-27813-9_5","volume-title":"Computer Aided Verification","author":"KS Namjoshi","year":"2004","unstructured":"Namjoshi, K.S.: An efficiently checkable, proof-based formulation of vacuity in model checking. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 57\u201369. Springer, Heidelberg (2004). doi: 10.1007\/978-3-540-27813-9_5"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL (1989)","DOI":"10.1145\/75277.75293"},{"key":"4_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/978-3-642-35873-9_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Samanta","year":"2013","unstructured":"Samanta, R., Deshmukh, J.V., Chaudhuri, S.: Robustness analysis of networked systems. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 229\u2013247. Springer, Heidelberg (2013). doi: 10.1007\/978-3-642-35873-9_15"},{"issue":"1","key":"4_CR18","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M Vardi","year":"1994","unstructured":"Vardi, M., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."}],"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-319-52234-0_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,21]],"date-time":"2022-07-21T06:33:06Z","timestamp":1658385186000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-52234-0_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319522333","9783319522340"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-52234-0_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}