{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T16:48:01Z","timestamp":1755794881854},"reference-count":26,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013,9]]},"DOI":"10.1109\/emsoft.2013.6658591","type":"proceedings-article","created":{"date-parts":[[2013,11,21]],"date-time":"2013-11-21T15:52:14Z","timestamp":1385049134000},"source":"Crossref","is-referenced-by-count":14,"title":["On composing and proving the correctness of reactive behavior"],"prefix":"10.1109","author":[{"given":"David","family":"Harel","sequence":"first","affiliation":[]},{"given":"Amir","family":"Kantor","sequence":"additional","affiliation":[]},{"given":"Guy","family":"Katz","sequence":"additional","affiliation":[]},{"given":"Assaf","family":"Marron","sequence":"additional","affiliation":[]},{"given":"Lior","family":"Mizrahi","sequence":"additional","affiliation":[]},{"given":"Gera","family":"Weiss","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","article-title":"You assume, we guarantee: Methodology and case studies","author":"henzinger","year":"1998","journal-title":"CAV"},{"key":"17","doi-asserted-by":"publisher","DOI":"10.1145\/2187671.2187678"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1145\/97946.97967"},{"key":"15","doi-asserted-by":"publisher","DOI":"10.1145\/2038642.2038686"},{"key":"16","doi-asserted-by":"publisher","DOI":"10.1145\/2209249.2209270"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2004.1317443"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177725"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.1109\/FOSE.2007.6"},{"key":"12","article-title":"Thread-modular model checking","author":"flanagan","year":"2003","journal-title":"SPIN"},{"key":"21","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(80)90123-4"},{"key":"20","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"22","doi-asserted-by":"publisher","DOI":"10.1145\/41840.41852"},{"key":"23","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(99)00030-1"},{"key":"24","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1981.230844"},{"key":"25","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-82453-1_5"},{"key":"26","year":"0","journal-title":"Esterel Technologies"},{"key":"3","article-title":"Symbolic compositional verification by learning assumptions","author":"alur","year":"2005","journal-title":"CAV"},{"key":"2","year":"0","journal-title":"Supplementary Material"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1145\/2304736.2304754"},{"key":"1","year":"0","journal-title":"Behavioral Programming"},{"key":"7","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503226"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146250"},{"key":"5","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39190"},{"key":"4","article-title":"A notion of glue expressiveness for component-based systems","author":"bliudze","year":"2008","journal-title":"CONCUR"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1145\/2162049.2162063"},{"key":"8","article-title":"Z3: An efficient smt solver","author":"de moura","year":"2008","journal-title":"TACAS"}],"event":{"name":"2013 International \u00a0Conference on Embedded \u00a0Software (EMSOFT)","location":"Montreal, QC, Canada","start":{"date-parts":[[2013,9,29]]},"end":{"date-parts":[[2013,10,4]]}},"container-title":["2013 Proceedings of the International Conference on Embedded Software (EMSOFT)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/6648479\/6658572\/06658591.pdf?arnumber=6658591","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,3,23]],"date-time":"2017-03-23T01:38:11Z","timestamp":1490233091000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6658591\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9]]},"references-count":26,"URL":"https:\/\/doi.org\/10.1109\/emsoft.2013.6658591","relation":{},"subject":[],"published":{"date-parts":[[2013,9]]}}}