{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:23:15Z","timestamp":1779074595971,"version":"3.51.4"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319899626","type":"print"},{"value":"9783319899633","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89963-3_10","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T14:53:00Z","timestamp":1523631180000},"page":"176-193","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":20,"title":["Validity-Guided Synthesis of Reactive Systems from Assume-Guarantee Contracts"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7013-1100","authenticated-orcid":false,"given":"Andreas","family":"Katis","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1727-4043","authenticated-orcid":false,"given":"Grigory","family":"Fedyukovich","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Huajun","family":"Guo","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Gacek","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"John","family":"Backes","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arie","family":"Gurfinkel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael W.","family":"Whalen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"key":"10_CR1","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016). \n                      www.SMT-LIB.org"},{"key":"10_CR2","doi-asserted-by":"crossref","unstructured":"Beyene, T., Chaudhuri, S., Popeea, C., Rybalchenko, A.: A constraint-based approach to solving games on infinite graphs. In: POPL, pp. 221\u2013233. ACM (2014)","DOI":"10.1145\/2535838.2535860"},{"key":"10_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/978-3-642-33475-7_5","volume-title":"Theoretical Computer Science","author":"MHL Bodlaender","year":"2012","unstructured":"Bodlaender, M.H.L., Hurkens, C.A.J., Kusters, V.J.J., Staals, F., Woeginger, G.J., Zantema, H.: Cinderella versus the wicked stepmother. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 57\u201371. Springer, Heidelberg (2012). \n                      https:\/\/doi.org\/10.1007\/978-3-642-33475-7_5"},{"key":"10_CR4","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). \n                      https:\/\/doi.org\/10.1007\/978-3-642-18275-4_7"},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: Parameter synthesis with IC3. In: FMCAD, pp. 165\u2013168. IEEE (2013)","DOI":"10.1109\/FMCAD.2013.6679406"},{"key":"10_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"52","DOI":"10.1007\/978-3-662-46681-0_4","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2015","unstructured":"Cimatti, A., Griggio, A., Mover, S., Tonetta, S.: HyComp: an SMT-based model checker for hybrid systems. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 52\u201367. Springer, Heidelberg (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-662-46681-0_4"},{"key":"10_CR7","unstructured":"Claessen, K., S\u00f6rensson, N.: A liveness checking algorithm that counts. In: Formal Methods in Computer-Aided Design (FMCAD), 2012, pp. 52\u201359. IEEE (2012)"},{"issue":"10","key":"10_CR8","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1145\/2544173.2509511","volume":"48","author":"Isil Dillig","year":"2013","unstructured":"Dillig, I., Dillig, T., Li, B., McMillan, K.: Inductive invariant generation via abductive inference. In: OOPSLA, pp. 443\u2013456. ACM (2013)","journal-title":"ACM SIGPLAN Notices"},{"key":"10_CR9","unstructured":"Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: FMCAD, pp. 125\u2013134. IEEE (2011)"},{"key":"10_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"606","DOI":"10.1007\/978-3-662-48899-7_42","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G Fedyukovich","year":"2015","unstructured":"Fedyukovich, G., Gurfinkel, A., Sharygina, N.: Automated discovery of simulation between\u00a0programs. In: Davis, M., Fehnker, A., McIver, A., Voronkov, A. (eds.) LPAR 2015. LNCS, vol. 9450, pp. 606\u2013621. Springer, Heidelberg (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-662-48899-7_42"},{"key":"10_CR11","doi-asserted-by":"publisher","first-page":"62","DOI":"10.4204\/EPTCS.260.7","volume":"260","author":"Elizabeth Firman","year":"2017","unstructured":"Firman, E., Maoz, S., Ringert, J.O.: Performance heuristics for GR(1) synthesis and related algorithms. In: SYNT@CAV. EPTCS, vol. 260, pp. 62\u201380. Open Publishing Association (2017)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"issue":"2","key":"10_CR12","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1023\/A:1008797606116","volume":"8","author":"P Flener","year":"2001","unstructured":"Flener, P., Partridge, D.: Inductive programming. Autom. Softw. Eng. 8(2), 131\u2013137 (2001)","journal-title":"Autom. Softw. Eng."},{"key":"10_CR13","unstructured":"Gacek, A.: JKind - an infinite-state model checker for safety properties in Lustre (2016). \n                      http:\/\/loonwerks.com\/tools\/jkind.html"},{"key":"10_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-319-17524-9_13","volume-title":"NASA Formal Methods","author":"A Gacek","year":"2015","unstructured":"Gacek, A., Katis, A., Whalen, M.W., Backes, J., Cofer, D.: Towards realizability checking of contracts using theories. In: Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp. 173\u2013187. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-17524-9_13"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Gulwani, S.: Dimensions in program synthesis. In: PPDP, pp. 13\u201324. ACM (2010)","DOI":"10.1145\/1836089.1836091"},{"key":"10_CR16","doi-asserted-by":"crossref","unstructured":"Hagen, G., Tinelli, C.: Scaling up the formal verification of Lustre programs with SMT-based techniques. In: FMCAD, pp. 1\u20139. IEEE (2008)","DOI":"10.1109\/FMCAD.2008.ECP.19"},{"key":"10_CR17","doi-asserted-by":"publisher","first-page":"112","DOI":"10.4204\/EPTCS.229.10","volume":"229","author":"Swen Jacobs","year":"2016","unstructured":"Jacobs, S., Klein, F., Schirmer, S.: A high-level LTL synthesis format: TLSF v1.1. In: SYNT@CAV. EPTCS, vol. 229, pp. 112\u2013132 (2016)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"10_CR18","unstructured":"Jahier, E., Raymond, P., Halbwachs, N.: The Lustre V6 reference manual. \n                      http:\/\/www-verimag.imag.fr\/Lustre-V6.html"},{"key":"10_CR19","unstructured":"Katis, A., Fedyukovich, G., Gacek, A., Backes, J.D., Gurfinkel, A., Whalen, M.W.: Synthesis from assume-guarantee contracts using Skolemized Proofs of Realizability. CoRR abs\/1610.05867 (2016). \n                      http:\/\/arxiv.org\/abs\/1610.05867"},{"key":"10_CR20","doi-asserted-by":"publisher","unstructured":"Katis, A., Fedyukovich, G., Guo, H., Gacek, A., Backes, J., Gurfinkel, A., Whalen, M.W.: Validity-guided synthesis of reactive systems from assume-guarantee contracts. Figshare (2018). \n                      https:\/\/doi.org\/10.6084\/m9.figshare.5904904.v1","DOI":"10.6084\/m9.figshare.5904904.v1"},{"key":"10_CR21","doi-asserted-by":"crossref","unstructured":"Katis, A., Gacek, A., Whalen, M.W.: Towards synthesis from assume-guarantee contracts involving infinite theories: a preliminary report. In: FormaliSE, pp. 36\u201341. IEEE (2016)","DOI":"10.1145\/2897667.2897675"},{"issue":"5\u20136","key":"10_CR22","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/s10009-011-0217-7","volume":"15","author":"V Kuncak","year":"2013","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Functional synthesis for linear arithmetic and sets. STTT 15(5\u20136), 455\u2013474 (2013)","journal-title":"STTT"},{"key":"10_CR23","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":"2005","unstructured":"Piterman, N., Pnueli, A., Sa\u0160ar, Y.: Synthesis of reactive(1) designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 364\u2013380. Springer, Heidelberg (2005). \n                      https:\/\/doi.org\/10.1007\/11609773_24"},{"key":"10_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1007\/978-3-662-54577-5_15","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Preiner","year":"2017","unstructured":"Preiner, M., Niemetz, A., Biere, A.: Counterexample-guided model synthesis. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 264\u2013280. Springer, Heidelberg (2017). \n                      https:\/\/doi.org\/10.1007\/978-3-662-54577-5_15"},{"key":"10_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"198","DOI":"10.1007\/978-3-319-21668-3_12","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2015","unstructured":"Reynolds, A., Deters, M., Kuncak, V., Tinelli, C., Barrett, C.: Counterexample-guided quantifier instantiation for synthesis in SMT. In: Kroening, D., P\u0103s\u0103reanu, C.S. (eds.) CAV 2015, Part II. LNCS, vol. 9207, pp. 198\u2013216. Springer, Cham (2015). \n                      https:\/\/doi.org\/10.1007\/978-3-319-21668-3_12"},{"key":"10_CR26","doi-asserted-by":"crossref","unstructured":"Ryzhyk, L., Walker, A.: Developing a practical reactive synthesis tool: experience and lessons learned. arXiv preprint \n                      arXiv:1611.07624\n                      \n                     (2016)","DOI":"10.4204\/EPTCS.229.8"},{"key":"10_CR27","unstructured":"Ryzhyk, L., Walker, A., Keys, J., Legg, A., Raghunath, A., Stumm, M., Vij, M.: User-guided device driver synthesis. In: OSDI, pp. 661\u2013676 (2014)"},{"issue":"5\u20136","key":"10_CR28","doi-asserted-by":"publisher","first-page":"497","DOI":"10.1007\/s10009-012-0223-4","volume":"15","author":"S Srivastava","year":"2013","unstructured":"Srivastava, S., Gulwani, S., Foster, J.S.: Template-based program verification and program synthesis. STTT 15(5\u20136), 497\u2013518 (2013)","journal-title":"STTT"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89963-3_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,3,3]],"date-time":"2020-03-03T03:16:18Z","timestamp":1583205378000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89963-3_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319899626","9783319899633"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89963-3_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"14 April 2018","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Thessaloniki","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14 April 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 April 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/index.php\/2018\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}