{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:11:09Z","timestamp":1763467869132},"reference-count":15,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008,6]]},"DOI":"10.1109\/acc.2008.4586906","type":"proceedings-article","created":{"date-parts":[[2008,8,12]],"date-time":"2008-08-12T10:28:20Z","timestamp":1218536900000},"page":"2734-2740","source":"Crossref","is-referenced-by-count":10,"title":["Model checking in-the-loop: Finding counterexamples by systematic simulation"],"prefix":"10.1109","author":[{"given":"Flavio","family":"Lerda","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"James","family":"Kapinski","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hitashyam","family":"Maka","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Edmund M.","family":"Clarke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bruce H.","family":"Krogh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"15","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1109\/TCST.2004.824340"},{"key":"14","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-11494-7_22","article-title":"specification and verification of concurrent systems in cesar","author":"queille","year":"1982","journal-title":"Proc of the 5th International Symposium On Programming"},{"key":"11","doi-asserted-by":"publisher","DOI":"10.2514\/6.2007-6461"},{"key":"12","doi-asserted-by":"publisher","DOI":"10.1016\/S0005-1098(98)00179-4"},{"key":"3","article-title":"bebop: a symbolic model checker for boolean programs","author":"ball","year":"2000","journal-title":"Proc of the 7th International SPIN Workshop"},{"journal-title":"Using Simulink","year":"2007","key":"2"},{"journal-title":"Simulink Design Verifier User's Guide","year":"2007","key":"1"},{"key":"10","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"7","article-title":"synthesis of synchronization skeletons for branching time temporal logic","author":"clarke","year":"1981","journal-title":"Proc of Workshop on Logic of Programs"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1109\/9.948467"},{"year":"0","key":"5"},{"key":"4","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-46430-1_10","article-title":"verification of hybrid systems with linear differential inclusions using ellipsoidal approximations","author":"botchkarev","year":"2000","journal-title":"Proc of the 3rd International Workshop on Hybrid Systems Computation and Control"},{"key":"9","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1996.561342"},{"journal-title":"Model checking","year":"2000","author":"clarke","key":"8"}],"event":{"name":"2008 American Control Conference (ACC '08)","start":{"date-parts":[[2008,6,11]]},"location":"Seattle, WA","end":{"date-parts":[[2008,6,13]]}},"container-title":["2008 American Control Conference"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/4547420\/4586444\/04586906.pdf?arnumber=4586906","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T03:34:07Z","timestamp":1557718447000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/4586906\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,6]]},"references-count":15,"URL":"https:\/\/doi.org\/10.1109\/acc.2008.4586906","relation":{},"subject":[],"published":{"date-parts":[[2008,6]]}}}