{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,30]],"date-time":"2022-03-30T06:50:24Z","timestamp":1648623024798},"reference-count":30,"publisher":"Oxford University Press (OUP)","issue":"5","license":[{"start":{"date-parts":[[2017,7,28]],"date-time":"2017-07-28T00:00:00Z","timestamp":1501200000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/about_us\/legal\/notices"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018,5,1]]},"DOI":"10.1093\/comjnl\/bxx069","type":"journal-article","created":{"date-parts":[[2017,6,28]],"date-time":"2017-06-28T15:10:17Z","timestamp":1498662617000},"page":"658-671","source":"Crossref","is-referenced-by-count":0,"title":["A True-Concurrency Encoding for BMC of Compositional Systems"],"prefix":"10.1093","volume":"61","author":[{"given":"Liangze","family":"Yin","sequence":"first","affiliation":[{"name":"School of Computer, National University of Defense Technology, Changsha, Hunan, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wei","family":"Dong","sequence":"additional","affiliation":[{"name":"School of Computer, National University of Defense Technology, Changsha, Hunan, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fei","family":"He","sequence":"additional","affiliation":[{"name":"School of Software, Tsinghua University, Beijing, China"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ji","family":"Wang","sequence":"additional","affiliation":[{"name":"School of Computer, National University of Defense Technology, Changsha, Hunan, China"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2017,7,28]]},"reference":[{"key":"key\n\t\t\t\t20180425035430_bxx069C1","author":"Biere","year":"1999"},{"key":"key\n\t\t\t\t20180425035430_bxx069C2","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1011276507260","article-title":"Bounded model checking using satisfiability solving","volume":"19","author":"Clarke","year":"2001","journal-title":"Formal Methods Syst. Des."},{"key":"key\n\t\t\t\t20180425035430_bxx069C3","author":"Grumberg","year":"2005"},{"key":"key\n\t\t\t\t20180425035430_bxx069C4","author":"Vineet","year":"2006"},{"key":"key\n\t\t\t\t20180425035430_bxx069C5","author":"Kahlon","year":"2009"},{"key":"key\n\t\t\t\t20180425035430_bxx069C6","author":"Alglave","year":"2013"},{"key":"key\n\t\t\t\t20180425035430_bxx069C7","author":"Burckhardt","year":"2007"},{"key":"key\n\t\t\t\t20180425035430_bxx069C8","author":"Ganai","year":"2008"},{"key":"key\n\t\t\t\t20180425035430_bxx069C9","author":"Sheeran","year":"2000"},{"key":"key\n\t\t\t\t20180425035430_bxx069C10","doi-asserted-by":"crossref","first-page":"543","DOI":"10.1016\/S1571-0661(05)82542-3","article-title":"Temporal induction by incremental SAT solving","volume":"89","author":"E\u00e9n","year":"2003","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"key\n\t\t\t\t20180425035430_bxx069C11","author":"Donaldson","year":"2011"},{"key":"key\n\t\t\t\t20180425035430_bxx069C12","author":"Brain","year":"2015"},{"key":"key\n\t\t\t\t20180425035430_bxx069C13","author":"Clarke","year":"2003"},{"key":"key\n\t\t\t\t20180425035430_bxx069C14","author":"Kurshan","year":"1998"},{"key":"key\n\t\t\t\t20180425035430_bxx069C15","doi-asserted-by":"crossref","first-page":"1095","DOI":"10.1016\/j.scico.2011.07.005","article-title":"Exploiting step semantics for efficient bounded model checking of asynchronous systems","volume":"77","author":"Dubrovin","year":"2012","journal-title":"Sci. Comput. Programming"},{"key":"key\n\t\t\t\t20180425035430_bxx069C16","author":"Basu","year":"2006"},{"key":"key\n\t\t\t\t20180425035430_bxx069C17","author":"Wang","year":"2012"},{"key":"key\n\t\t\t\t20180425035430_bxx069C18","volume-title":"Formal Analysis and Design of Network Protocols","author":"Gu","year":"2003"},{"key":"key\n\t\t\t\t20180425035430_bxx069C19","author":"Alur","year":"2000"},{"key":"key\n\t\t\t\t20180425035430_bxx069C20","author":"Alur","year":"2000"},{"key":"key\n\t\t\t\t20180425035430_bxx069C21","author":"Alur","year":"2001"},{"key":"key\n\t\t\t\t20180425035430_bxx069C22","author":"Dong","year":"1999"},{"key":"key\n\t\t\t\t20180425035430_bxx069C23","author":"Holzmann","year":"1999"},{"key":"key\n\t\t\t\t20180425035430_bxx069C24","author":"Jussila","year":"2005"},{"key":"key\n\t\t\t\t20180425035430_bxx069C25","author":"Kurshan","year":"2002"},{"key":"key\n\t\t\t\t20180425035430_bxx069C26","author":"Yorav","year":"2000"},{"key":"key\n\t\t\t\t20180425035430_bxx069C27","doi-asserted-by":"crossref","first-page":"89","DOI":"10.1007\/s10009-004-0178-1","article-title":"BMC via on-the-fly determinization","volume":"7","author":"Jussila","year":"2005","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"key\n\t\t\t\t20180425035430_bxx069C28","author":"Flanagan","year":"2003"},{"key":"key\n\t\t\t\t20180425035430_bxx069C29","author":"Malkis","year":"2010"},{"key":"key\n\t\t\t\t20180425035430_bxx069C30","author":"Forejt","year":"2014"}],"container-title":["The Computer Journal"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/academic.oup.com\/comjnl\/article-pdf\/61\/5\/658\/24724551\/bxx069.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2018,4,25]],"date-time":"2018-04-25T03:54:36Z","timestamp":1524628476000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/comjnl\/article\/61\/5\/658\/4055636"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,28]]},"references-count":30,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2017,7,28]]},"published-print":{"date-parts":[[2018,5,1]]}},"URL":"https:\/\/doi.org\/10.1093\/comjnl\/bxx069","relation":{},"ISSN":["0010-4620","1460-2067"],"issn-type":[{"value":"0010-4620","type":"print"},{"value":"1460-2067","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2018,5]]},"published":{"date-parts":[[2017,7,28]]}}}