{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,5,21]],"date-time":"2025-05-21T05:52:56Z","timestamp":1747806776693},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642182747"},{"type":"electronic","value":"9783642182754"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2011]]},"DOI":"10.1007\/978-3-642-18275-4_16","type":"book-chapter","created":{"date-parts":[[2011,1,17]],"date-time":"2011-01-17T05:06:38Z","timestamp":1295240798000},"page":"214-231","source":"Crossref","is-referenced-by-count":20,"title":["Verifying Deadlock-Freedom of Communication Fabrics"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Gotmanov","sequence":"first","affiliation":[]},{"given":"Satrajit","family":"Chatterjee","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Kishinevsky","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"16_CR1","unstructured":"NuSMV home page, http:\/\/nusmv.irst.itc.it\/"},{"key":"16_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/3-540-56863-8_41","volume-title":"Application and Theory of Petri Nets 1993","author":"K. Barkaoui","year":"1993","unstructured":"Barkaoui, K., Dutheillet, C., Haddad, S.: An efficient algorithm for finding structural deadlocks in colored Petri nets. In: Ajmone Marsan, M. (ed.) ICATPN 1993. LNCS, vol.\u00a0691, pp. 69\u201388. Springer, Heidelberg (1993)"},{"key":"16_CR3","unstructured":"Berkeley Logic Synthesis and Verification Group: ABC: A system for sequential synthesis and verification, http:\/\/www.eecs.berkeley.edu\/~alanmi\/abc\/"},{"issue":"2","key":"16_CR4","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1016\/S1571-0661(04)80410-9","volume":"66","author":"A. Biere","year":"2002","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electronic Notes in Theoretical Computer Science\u00a066(2), 160\u2013177 (2002)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"321","DOI":"10.1007\/978-3-642-14295-6_29","volume-title":"Computer Aided Verification","author":"S. Chatterjee","year":"2010","unstructured":"Chatterjee, S., Kishinevsky, M.: Automatic generation of inductive invariants from high-level microarchitectural models of communication fabrics. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 321\u2013338. Springer, Heidelberg (2010)"},{"key":"16_CR6","doi-asserted-by":"crossref","unstructured":"Chatterjee, S., Kishinevsky, M., Ogras, U.Y.: Quick formal modeling of communication fabrics to enable verification. In: Proc. IEEE High Level Design Validation and Test Workshop (HLDVT), pp. 42\u201349 (2010)","DOI":"10.1109\/HLDVT.2010.5496662"},{"key":"16_CR7","volume-title":"Principles and Practices of Interconnection Networks","author":"W. Dally","year":"2004","unstructured":"Dally, W., Towles, B.: Principles and Practices of Interconnection Networks. Morgan Kaufmann, San Francisco (2004)"},{"issue":"10","key":"16_CR8","doi-asserted-by":"publisher","first-page":"1055","DOI":"10.1109\/71.473515","volume":"6","author":"J. Duato","year":"1995","unstructured":"Duato, J.: A necessary and sufficient condition for deadlock-free adaptive routing in wormhole networks. IEEE Trans. Paral. Distrib. Syst.\u00a06(10), 1055\u20131067 (1995)","journal-title":"IEEE Trans. Paral. Distrib. Syst."},{"key":"16_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/11560548_28","volume-title":"Correct Hardware Design and Verification Methods","author":"B. Gebremichael","year":"2005","unstructured":"Gebremichael, B., Vaandrager, F.W., Zhang, M., Goossens, K.G.W., Rijpkema, E., R\u0103dulescu, A.: Deadlock prevention in the \u00e6thereal protocol. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 345\u2013348. Springer, Heidelberg (2005)"},{"key":"16_CR10","doi-asserted-by":"crossref","unstructured":"Ghafari, N., Gurfinkel, A., Klarlund, N., Trefler, R.J.: Algorithmic analysis of piecewise fifo systems. In: FMCAD, pp. 45\u201352 (2007)","DOI":"10.1109\/FAMCAD.2007.18"},{"key":"16_CR11","first-page":"16","volume-title":"POPL 2009: Proc. of Symp. on Principles of Prog. Lang.","author":"A. Gotsman","year":"2009","unstructured":"Gotsman, A., Cook, B., Parkinson, M., Vafeiadis, V.: Proving that non-blocking algorithms don\u2019t block. In: POPL 2009: Proc. of Symp. on Principles of Prog. Lang., pp. 16\u201328. ACM, New York (2009)"},{"key":"16_CR12","doi-asserted-by":"crossref","unstructured":"Hansson, A., Goossens, K., R\u0103dulescu, A.: Avoiding message-dependent deadlock in network-based systems on chip. VLSI Design 2007 (May 2007)","DOI":"10.1155\/2007\/95859"},{"issue":"3","key":"16_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1367045.1367054","volume":"13","author":"P. Manolios","year":"2008","unstructured":"Manolios, P., Srinivasan, S.K.: Automatic verification of safety and liveness for pipelined machines using web refinement. ACM Trans. Des. Autom. Electron. Syst.\u00a013(3), 1\u201319 (2008)","journal-title":"ACM Trans. Des. Autom. Electron. Syst."},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"342","DOI":"10.1007\/3-540-48153-2_30","volume-title":"Correct Hardware Design and Verification Methods","author":"K.L. McMillan","year":"1999","unstructured":"McMillan, K.L.: Circular compositional reasoning about liveness. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol.\u00a01703, pp. 342\u2013345. Springer, Heidelberg (1999)"},{"key":"16_CR15","doi-asserted-by":"crossref","unstructured":"Taktak, S., Desbarbieux, J.L., Encrenaz, E.: A tool for automatic detection of deadlock in wormhole networks on chip. ACM Trans. Design Autom. Electr. Syst.\u00a013(1) (1995)","DOI":"10.1145\/1297666.1297672"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Verbeek, F., Schmaltz, J.: Formal specification of networks-on-chips: deadlock and evacuation. In: DATE 2010, pp. 1701\u20131706 (2010)","DOI":"10.1109\/DATE.2010.5457089"}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-18275-4_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,7]],"date-time":"2019-06-07T22:39:34Z","timestamp":1559947174000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-18275-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642182747","9783642182754"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-18275-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}