{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,9,12]],"date-time":"2023-09-12T22:46:07Z","timestamp":1694558767053},"reference-count":42,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","license":[{"start":{"date-parts":[[2014,1,1]],"date-time":"2014-01-01T00:00:00Z","timestamp":1388534400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IEEE Trans. Comput."],"published-print":{"date-parts":[[2014]]},"DOI":"10.1109\/tc.2014.2329701","type":"journal-article","created":{"date-parts":[[2014,7,17]],"date-time":"2014-07-17T18:26:59Z","timestamp":1405621619000},"page":"1-1","source":"Crossref","is-referenced-by-count":3,"title":["Compositional Model Checking of Concurrent Systems"],"prefix":"10.1109","author":[{"given":"Hao","family":"Zheng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhen","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Chris J.","family":"Myers","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emmanuel","family":"Rodriguez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yingying","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1109\/ASYNC.1996.494447"},{"key":"ref38","doi-asserted-by":"crossref","first-page":"433","DOI":"10.1109\/TCAD.2009.2012531","article-title":"Automated interface refinement for compositional verification","volume":"28","author":"yao","year":"2009","journal-title":"IEEE Trans Comput -Aided Des Integr Circuits Syst"},{"key":"ref33","author":"myers","year":"1995","journal-title":"Computer-aided synthesis and verification of gate-level timed circuits"},{"key":"ref32","first-page":"279","volume":"37","author":"mcmillan","year":"2000","journal-title":"A methodology for hardware verification using compositional model checking"},{"key":"ref31","doi-asserted-by":"crossref","DOI":"10.21236\/ADA442970","author":"martin","year":"1986","journal-title":"Self-timed FIFO An exercise in compiling programs into VLSI circuits"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1142\/S0129054113500123"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39958-2_17"},{"key":"ref36","first-page":"527","article-title":"Learning component interfaces with may and must abstractions","author":"singh","year":"0","journal-title":"Proc 22nd Int Conf Comput Aided Verification"},{"key":"ref35","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73370-6_17"},{"key":"ref34","first-page":"170","article-title":"Learning based symbolic assume-guarantee reasoning with automatic decomposition","author":"nam","year":"0","journal-title":"Proc of the Int Symp of Aut Tech for Verification and Analysis"},{"key":"ref10","first-page":"534","article-title":"Automated assume-guarantee reasoning for simulation conformance","author":"chaki","year":"0","journal-title":"Proc Int Conf Comput Aided Verification"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/TCAD.2009.2035544"},{"key":"ref11","doi-asserted-by":"publisher","DOI":"10.1145\/235321.235323"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1145\/295558.295570"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39190"},{"key":"ref14","first-page":"331","article-title":"Learning assumptions for compositional verification","author":"cobleigh","year":"0","journal-title":"Proc Int Conf Tools Algorithms Construction Anal Syst"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_47"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1109\/ACSD.2010.28"},{"key":"ref17","first-page":"111","article-title":"Smart reduction","author":"crouzen","year":"0","journal-title":"Proc 14th Int Conf Fundam Approaches Softw Eng Part Joint Eur Conf Theory Practice Softw"},{"key":"ref18","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49213-5_25"},{"key":"ref19","year":"0"},{"key":"ref28","first-page":"197","article-title":"An improvement in formal verification","author":"holzmann","year":"0","journal-title":"Proc 7th IFIP WG6 1 Int Conf Formal Description Techniques"},{"key":"ref4","first-page":"614","article-title":"D-finder: A tool for compositional deadlock detection and verification","author":"bensalem","year":"0","journal-title":"Proc 21st Int Conf Comput Aided Verification"},{"key":"ref27","first-page":"440","article-title":"You assume, we guarantee: Methodology and case studies","author":"henzinger","year":"0","journal-title":"Proc Int Conf Comput Aided Verification"},{"key":"ref3","author":"baier","year":"2008","journal-title":"Principles of Model Checking"},{"key":"ref6","first-page":"135","article-title":"Automated assume-guarantee reasoning by abstraction refinement","author":"bobaru","year":"0","journal-title":"Proc Int Conf Comput Aided Verification"},{"key":"ref29","first-page":"239","article-title":"Compositional state space generation from lotos programs","author":"krimm","year":"0","journal-title":"Proc Int Conf Tools Algorithms Construction Anal Syst"},{"key":"ref5","first-page":"81","article-title":"Compositional reasoning in model checking","author":"berezin","year":"0","journal-title":"Revised Lectures Int'l Symp Compositionality The Significant Difference"},{"key":"ref8","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-75596-8_31"},{"key":"ref7","doi-asserted-by":"publisher","DOI":"10.1109\/DSN.2008.4630122"},{"key":"ref2","first-page":"226","article-title":"Visual specifications for modular reasoning about asynchronous systems","author":"amla","year":"0","journal-title":"Proc 22nd IFIP WG 6 1 Int Conf Houston Formal Tech Netw Distrib Syst"},{"key":"ref9","first-page":"163","article-title":"Modular minimization of deterministic finite-state machines","author":"bustan","year":"0","journal-title":"Proc 16th Int Workshop Formal Methods Ind Critical Syst"},{"key":"ref1","first-page":"548","article-title":"Symbolic compositional verification by learning assumptions","author":"alur","year":"0","journal-title":"Proc Int Conf Comput Aided Verification"},{"key":"ref20","author":"dill","year":"1988","journal-title":"Trace theory for automatic hierarchical verification of speed independent circuits"},{"key":"ref22","first-page":"410","article-title":"On combining functional verification and performance evaluation using CADP","author":"garavel","year":"0","journal-title":"Proc of Formal Methods International Symposium of Formal Methods Europe"},{"key":"ref21","author":"clarke","year":"2000","journal-title":"Model checking"},{"key":"ref42","first-page":"509","article-title":"Compositionality and concurrent networks: Soundness and completeness of a proof system","author":"zwiers","year":"0","journal-title":"Proc 17th Colloquium on Automata Languages and Programming"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-005-2641-y"},{"key":"ref41","first-page":"62","article-title":"A compositional minimization approach for large asynchronous design verification","author":"zheng","year":"0","journal-title":"Proc 19th Int Conf Model Checking Softw"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-71209-1_23"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177725"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211911"}],"container-title":["IEEE Transactions on Computers"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/12\/7104223\/06858024.pdf?arnumber=6858024","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,12]],"date-time":"2022-01-12T16:41:57Z","timestamp":1642005717000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/6858024\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"references-count":42,"URL":"https:\/\/doi.org\/10.1109\/tc.2014.2329701","relation":{},"ISSN":["0018-9340"],"issn-type":[{"value":"0018-9340","type":"print"}],"subject":[],"published":{"date-parts":[[2014]]}}}