{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,13]],"date-time":"2026-01-13T15:22:30Z","timestamp":1768317750635,"version":"3.49.0"},"reference-count":24,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015,9]]},"DOI":"10.1109\/memcod.2015.7340481","type":"proceedings-article","created":{"date-parts":[[2015,12,3]],"date-time":"2015-12-03T16:13:03Z","timestamp":1449159183000},"page":"148-157","source":"Crossref","is-referenced-by-count":4,"title":["Model and program repair via SAT solving"],"prefix":"10.1109","author":[{"given":"Paul","family":"Attie","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ali","family":"Cherri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kinan","family":"Dak Al Bab","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mohamad","family":"Sakr","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jad","family":"Saklawi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(98)00239-4"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/138873.138877"},{"key":"ref12","doi-asserted-by":"crossref","first-page":"59","DOI":"10.3233\/SAT190075","article-title":"The sat4j library, release 2.2, system description","volume":"7","author":"berre","year":"2010","journal-title":"Journal on Satisfiability Boolean Modeling and Computation"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1145\/383043.383044"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(99)00039-9"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1145\/217474.217565"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56922-7_5"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90110-4"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_28"},{"key":"ref19","article-title":"Symbolic model checking without BDDs","author":"biere","year":"1999","journal-title":"TACAS LNCS"},{"key":"ref4","article-title":"Synthesis of large dynamic concurrent programs from dynamic specifications","author":"attie","year":"0","journal-title":"American University of Beirut Beirut Lebanon Tech Rep 2015 to appear in Formal Methods in System Design"},{"key":"ref3","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48320-9_11"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1145\/5397.5399"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90017-5"},{"key":"ref8","first-page":"72","article-title":"Construction of abstract state graphs with pvs","volume":"1254","author":"graf","year":"1997","journal-title":"CAV Ser LNCS"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1145\/186025.186051"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1145\/271510.271519"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1145\/503502.503503"},{"key":"ref9","author":"dijkstra","year":"1976","journal-title":"A Discipline of Programming"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_23"},{"key":"ref22","article-title":"Diagnosis is repair","author":"staber","year":"2005","journal-title":"5th Int Workshop Principles of Diagnosis"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1007\/11560548_6"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28891-3_32"},{"key":"ref23","first-page":"113","article-title":"CTL model update for system modifications","volume":"31","author":"zhang","year":"2008","journal-title":"J Artif Int Res"}],"event":{"name":"2015 ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)","location":"Austin, TX, USA","start":{"date-parts":[[2015,9,21]]},"end":{"date-parts":[[2015,9,23]]}},"container-title":["2015 ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/7329076\/7340456\/07340481.pdf?arnumber=7340481","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,12]],"date-time":"2020-09-12T02:17:36Z","timestamp":1599877056000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/7340481\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,9]]},"references-count":24,"URL":"https:\/\/doi.org\/10.1109\/memcod.2015.7340481","relation":{},"subject":[],"published":{"date-parts":[[2015,9]]}}}