{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T18:00:42Z","timestamp":1725559242725},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642140518"},{"type":"electronic","value":"9783642140525"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-14052-5_7","type":"book-chapter","created":{"date-parts":[[2010,7,12]],"date-time":"2010-07-12T14:23:14Z","timestamp":1278944594000},"page":"67-82","source":"Crossref","is-referenced-by-count":3,"title":["A Formal Proof of a Necessary and Sufficient Condition for Deadlock-Free Adaptive Networks"],"prefix":"10.1007","author":[{"given":"Freek","family":"Verbeek","sequence":"first","affiliation":[]},{"given":"Julien","family":"Schmaltz","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","volume-title":"Operating Systems, Internals and Design Principles","author":"W. Stalling","year":"2009","unstructured":"Stalling, W.: Operating Systems, Internals and Design Principles. Pearson Education International, London (2009)"},{"doi-asserted-by":"crossref","unstructured":"Dally, W., Seitz, C.: Deadlock-free message routing in multiprocessor interconnection networks. IEEE Transactions on Computers\u00a0(36), 547\u2013553 (1987)","key":"7_CR2","DOI":"10.1109\/TC.1987.1676939"},{"issue":"10","key":"7_CR3","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 Transactions on Parallel and Distributed Systems\u00a06(10), 1055\u20131067 (1995)","journal-title":"IEEE Transactions on Parallel and Distributed Systems"},{"key":"7_CR4","volume-title":"Interconnection Networks, an engeneering approach","author":"J. Duato","year":"2003","unstructured":"Duato, J., Yalamanchili, S., Ni, L.: Interconnection Networks, an engeneering approach. Morgan Kaufmann Publishers, San Francisco (2003)"},{"doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: ACL2 Computer-Aided Reasoning: An Approach (2000)","key":"7_CR5","DOI":"10.1007\/978-1-4757-3188-0"},{"doi-asserted-by":"crossref","unstructured":"Verbeek, F., Schmaltz, J.: Proof pearl: A formal proof of dally and seitz\u2019 necessary and sufficient condition for deadlock-free routing in interconnection networks. J. Autom. Reasoning (2009) (submitted to publication), http:\/\/www.cs.ru.nl\/~julien\/Julien_at_Nijmegen\/JAR09.html","key":"7_CR6","DOI":"10.1007\/s10817-010-9206-x"},{"key":"7_CR7","volume-title":"ACL2 Computer Aided Reasoning: An Approach","author":"M. Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: ACL2 Computer Aided Reasoning: An Approach. Kluwer Academic Press, Dordrecht (2000)"},{"key":"7_CR8","series-title":"ACM International Conference Series","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1145\/1217975.1217995","volume-title":"Proceedings of the 6th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006)","author":"S. Ray","year":"2006","unstructured":"Ray, S.: Quantification in Tail-recursive Function Definitions. In: Manolios, P., Wilding, M. (eds.) Proceedings of the 6th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006), Seattle, WA, August 2006. ACM International Conference Series, vol.\u00a0205, pp. 95\u201398. ACM Press, New York (2006)"},{"issue":"2","key":"7_CR9","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1023\/A:1026517200045","volume":"26","author":"M. Kaufmann","year":"1997","unstructured":"Kaufmann, M., Moore, J.S.: Structured Theory Development for a Mechanized Logic. Journal of Automated Reasoning\u00a026(2), 161\u2013203 (1997)","journal-title":"Journal of Automated Reasoning"},{"doi-asserted-by":"crossref","unstructured":"Verbeek, F., Schmaltz, J.: Formal specification of networks-on-chip: deadlock, livelock, and evacuation. In: Proceedings of Design, Automation & Test in Europe 2010 (DATE\u201910) (March 2010)","key":"7_CR10","DOI":"10.1109\/DATE.2010.5457089"},{"issue":"4","key":"7_CR11","doi-asserted-by":"publisher","first-page":"678","DOI":"10.1145\/69622.357190","volume":"4","author":"J. Misra","year":"1982","unstructured":"Misra, J., Chandy, K.: A distributed graph algorithm: knot detection. ACM Transactions on Programming Languages and Systems\u00a04(4), 678\u2013686 (1982)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"8","key":"7_CR12","doi-asserted-by":"publisher","first-page":"841","DOI":"10.1109\/71.532115","volume":"7","author":"J. Duato","year":"1996","unstructured":"Duato, J.: A necessary and sufficient condition for deadlock-free adaptive routing in cut-through and store-and-forward networks. IEEE Transactions on Parallel and Distributed Systems\u00a07(8), 841\u20131067 (1996)","journal-title":"IEEE Transactions on Parallel and Distributed Systems"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-14052-5_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,31]],"date-time":"2021-10-31T08:34:49Z","timestamp":1635669289000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-14052-5_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642140518","9783642140525"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-14052-5_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}