{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,20]],"date-time":"2026-01-20T11:21:26Z","timestamp":1768908086606,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":32,"publisher":"ACM","license":[{"start":{"date-parts":[[2017,5,14]],"date-time":"2017-05-14T00:00:00Z","timestamp":1494720000000},"content-version":"vor","delay-in-days":365,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["4504789784"],"award-info":[{"award-number":["4504789784"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000104","name":"National Aeronautics and Space Administration","doi-asserted-by":"publisher","award":["NNA13AA21C"],"award-info":[{"award-number":["NNA13AA21C"]}],"id":[{"id":"10.13039\/100000104","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CNS-1035715"],"award-info":[{"award-number":["CNS-1035715"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,5,14]]},"DOI":"10.1145\/2897667.2897675","type":"proceedings-article","created":{"date-parts":[[2016,5,18]],"date-time":"2016-05-18T10:28:05Z","timestamp":1463567285000},"page":"36-41","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Towards synthesis from assume-guarantee contracts involving infinite theories"],"prefix":"10.1145","author":[{"given":"Andreas","family":"Katis","sequence":"first","affiliation":[{"name":"University of Minnesota, Minneapolis, MN"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Gacek","sequence":"additional","affiliation":[{"name":"Rockwell Collins Advanced Technology Center, Cedar Rapids, IA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael W.","family":"Whalen","sequence":"additional","affiliation":[{"name":"University of Minnesota, Minneapolis, MN"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2016,5,14]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1836089.1836091"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_13"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2012.173"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2527269.2527272"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-17524-9_7"},{"key":"e_1_3_2_1_6_1","first-page":"173","volume-title":"Towards realizability checking of contracts using theories,\" in NASA Formal Methods","author":"Gacek A.","year":"2015","unstructured":"A. Gacek, A. Katis, M. W. Whalen, J. Backes, and D. Cofer, \"Towards realizability checking of contracts using theories,\" in NASA Formal Methods. Springer, 2015, pp. 173--187."},{"key":"e_1_3_2_1_7_1","volume-title":"Machine-checked proofs for realizability checking algorithms","author":"Katis A.","year":"2015","unstructured":"A. Katis, A. Gacek, and M. W. Whalen, \"Machine-checked proofs for realizability checking algorithms,\" 2015, submitted http:\/\/arxiv.org\/abs\/1502.01292."},{"key":"e_1_3_2_1_8_1","unstructured":"SAE-AS5506 \"Architecture analysis and design language \" Nov 2004."},{"key":"e_1_3_2_1_9_1","unstructured":"A. Reynolds M. Deters V. Kuncak C. Tinelli and C. Barrett \"Counterexample-guided quantifier instantiation for synthesis in smt.\""},{"key":"e_1_3_2_1_10_1","unstructured":"G. Fedyukovich A. Gurfinkel and N. Sharygina \"Ae-val: Horn clause-based skolemizer for ∀∃-formulas.\""},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"crossref","unstructured":"G. Fedyukovich A. Gurfinkel and N. Sharygina \"Automated discovery of simulation between programs \" submitted also available as Technical Report USI vol. 5 2014.","DOI":"10.21236\/ADA613949"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_2"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/36.5.450"},{"key":"e_1_3_2_1_14_1","unstructured":"A. Gacek \"JKind -- an infinite-state model checker for safety properties in Lustre \" http:\/\/loonwerks.com\/tools\/jkind.html 2016."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/362566.362568"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/1987082.1987098"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_45"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1226781.1226805"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/1763507.1763535"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-27660-6_45"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/1998496.1998517"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/224841.225124"},{"issue":"5","key":"e_1_3_2_1_24_1","first-page":"6","article-title":"Template-based program verification and program synthesis","volume":"15","author":"Srivastava S.","year":"2013","unstructured":"S. Srivastava, S. Gulwani, and J. S. Foster, \"Template-based program verification and program synthesis,\" International Journal on Software Tools for Technology Transfer, vol. 15, no. 5--6, pp. 497--518, 2013.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008797606116"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/2900728.2900793"},{"key":"e_1_3_2_1_27_1","first-page":"248","article-title":"Solving temporal problems using SMT: Strong controllability","author":"Cimatti A.","year":"2012","unstructured":"A. Cimatti, A. Micheli, and M. Roveri, \"Solving temporal problems using SMT: Strong controllability,\" in CP, 2012, pp. 248--264.","journal-title":"CP"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10601-014-9167-5"},{"key":"e_1_3_2_1_29_1","doi-asserted-by":"publisher","unstructured":"A. Bradley \"SAT-based model checking without unrolling \" VMCAI 2011.","DOI":"10.5555\/1946284.1946291"},{"key":"e_1_3_2_1_30_1","first-page":"46","volume-title":"Ic3 modulo theories via implicit predicate abstraction,\" in Tools and Algorithms for the Construction and Analysis of Systems","author":"Cimatti A.","year":"2014","unstructured":"A. Cimatti, A. Griggio, S. Mover, and S. Tonetta, \"Ic3 modulo theories via implicit predicate abstraction,\" in Tools and Algorithms for the Construction and Analysis of Systems. Springer, 2014, pp. 46--61."},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.5555\/2157654.2157675"},{"key":"e_1_3_2_1_32_1","volume-title":"Passau (Germany)","author":"Halbwachs N.","year":"1991","unstructured":"N. Halbwachs, P. Raymond, and C. Ratel, \"Generating efficient code from data-flow programs,\" in Third Int'l Symposium on Programming Language Implementation and Logic Programming, Passau (Germany), August 1991."}],"event":{"name":"ICSE '16: 38th International Conference on Software Engineering","location":"Austin Texas","acronym":"ICSE '16","sponsor":["ACM Association for Computing Machinery","SIGSOFT ACM Special Interest Group on Software Engineering","IEEE-CS\\DATC IEEE Computer Society","TCSE IEEE Computer Society's Tech. Council on Software Engin."]},"container-title":["Proceedings of the 4th FME Workshop on Formal Methods in Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2897667.2897675","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2897667.2897675","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2897667.2897675","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T09:29:14Z","timestamp":1763458154000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2897667.2897675"}},"subtitle":["a preliminary report"],"short-title":[],"issued":{"date-parts":[[2016,5,14]]},"references-count":32,"alternative-id":["10.1145\/2897667.2897675","10.1145\/2897667"],"URL":"https:\/\/doi.org\/10.1145\/2897667.2897675","relation":{},"subject":[],"published":{"date-parts":[[2016,5,14]]},"assertion":[{"value":"2016-05-14","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}