{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T21:29:17Z","timestamp":1729632557682,"version":"3.28.0"},"reference-count":35,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011,7]]},"DOI":"10.1109\/memcod.2011.5970518","type":"proceedings-article","created":{"date-parts":[[2011,8,3]],"date-time":"2011-08-03T22:16:29Z","timestamp":1312409789000},"page":"119-129","source":"Crossref","is-referenced-by-count":9,"title":["Efficient deadlock detection for concurrent systems"],"prefix":"10.1109","author":[{"given":"Saddek","family":"Bensalem","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Griesmayer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Axel","family":"Legay","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thanh-Hung","family":"Nguyen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Doron","family":"Peled","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"year":"0","key":"ref33","article-title":"D-Finder tool"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0023716"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57568-5_270"},{"key":"ref30","doi-asserted-by":"crossref","first-page":"266","DOI":"10.1145\/157485.164888","article-title":"reducing bdd size by exploiting functional dependencies","author":"hu","year":"1993","journal-title":"30th ACM\/IEEE Design Automation Conference"},{"key":"ref35","doi-asserted-by":"crossref","first-page":"276","DOI":"10.1145\/196244.196377","article-title":"new techniques for efficient verification with implicitly conjoined bdds","author":"hu","year":"1994","journal-title":"31st Design Automation Conference"},{"key":"ref34","doi-asserted-by":"publisher","DOI":"10.1109\/MS.1985.230351"},{"key":"ref10","article-title":"SLAM and static driver verifier: Technology transfer of formal methods inside Microsoft","author":"ball","year":"2004","journal-title":"IFM"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_7"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1109\/SEFM.2006.27"},{"key":"ref13","article-title":"Incremental component-based construction and verification of a robotic system","author":"basu","year":"2008","journal-title":"ECAI"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1109\/MEMCOD.2004.1459856"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1002\/(SICI)1097-024X(199906)29:7<577::AID-SPE246>3.0.CO;2-V"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1007\/s100090050046"},{"key":"ref17","first-page":"639","article-title":"Hints to accelerate symbolic traversal","author":"ravi","year":"1999","journal-title":"Correct Hardware Design and Verification Methods"},{"key":"ref18","doi-asserted-by":"crossref","first-page":"122","DOI":"10.1145\/1047659.1040316","article-title":"Proof-guided underapproximation-widening for multiprocess systems","volume":"40","author":"grumberg","year":"2005","journal-title":"ACM SIGPLAN Notices"},{"key":"ref19","doi-asserted-by":"crossref","first-page":"505","DOI":"10.1007\/s10009-007-0044-z","article-title":"The software model checker BLAST: Applications to software engineering","volume":"9","author":"beyer","year":"2007","journal-title":"STTT"},{"key":"ref28","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08921-7_95"},{"key":"ref4","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/3-540-57208-2_17","article-title":"Partial-order methods for temporal verification","volume":"715","author":"wolper","year":"1993","journal-title":"CONCUR"},{"key":"ref27","first-page":"75","article-title":"Automatic generation of invariants","volume":"15","author":"bensalem","year":"1999","journal-title":"FMSD"},{"key":"ref3","first-page":"409","article-title":"All from one, one for all: on model checking using representatives","author":"peled","year":"1993","journal-title":"CAV"},{"key":"ref6","first-page":"193","article-title":"Symbolic model checking without BDDs","author":"biere","year":"1999","journal-title":"TACAS"},{"article-title":"JavaBDD java binary decision diagram library","year":"0","author":"whaley","key":"ref29"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"ref8","article-title":"Incremental component-based construction and verification using invariants","author":"bensalem","year":"2010","journal-title":"FMCAD"},{"key":"ref7","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-20398-5_32","article-title":"D-Finder 2: Towards efficient correctness of incremental design","author":"bensalem","year":"2011","journal-title":"Proceedings of the Nasa Formal Methods Symposium"},{"journal-title":"SPIN Model Checker The Primer and Reference Manual","year":"2003","author":"holzmann","key":"ref2"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"key":"ref1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01383879"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1145\/503272.503279"},{"key":"ref22","article-title":"The algebra of connectors &#x2014; structuring interaction in BIP","author":"bliudze","year":"2007","journal-title":"VERIMAG Tech Rep TR-2007&#x2013;3"},{"year":"0","key":"ref21","article-title":"BIP"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1109\/TASE.2010.23"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1109\/SIES.2009.5196211"},{"key":"ref26","first-page":"614","article-title":"D-Finder: A tool for compositional deadlock detection and verificationn","author":"bensalem","year":"2009","journal-title":"CAV"},{"key":"ref25","first-page":"64","article-title":"Compositional verification for component-based systems and application","author":"bensalem","year":"2008","journal-title":"ATVA"}],"event":{"name":"2011 9th IEEE\/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE 2011)","start":{"date-parts":[[2011,7,11]]},"location":"Cambridge, United Kingdom","end":{"date-parts":[[2011,7,13]]}},"container-title":["Ninth ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMPCODE2011)"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/5959846\/5970502\/05970518.pdf?arnumber=5970518","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,13]],"date-time":"2019-06-13T15:02:53Z","timestamp":1560438173000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/5970518\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,7]]},"references-count":35,"URL":"https:\/\/doi.org\/10.1109\/memcod.2011.5970518","relation":{},"subject":[],"published":{"date-parts":[[2011,7]]}}}