{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,12,29]],"date-time":"2022-12-29T21:08:22Z","timestamp":1672348102836},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2010,9,18]],"date-time":"2010-09-18T00:00:00Z","timestamp":1284768000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2012,4]]},"DOI":"10.1007\/s10817-010-9206-x","type":"journal-article","created":{"date-parts":[[2010,9,17]],"date-time":"2010-09-17T07:49:25Z","timestamp":1284709765000},"page":"419-439","source":"Crossref","is-referenced-by-count":4,"title":["Proof Pearl: A Formal Proof of Dally and Seitz\u2019 Necessary and Sufficient Condition for Deadlock-Free Routing in Interconnection Networks"],"prefix":"10.1007","volume":"48","author":[{"given":"Freek","family":"Verbeek","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"Schmaltz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2010,9,18]]},"reference":[{"key":"9206_CR1","doi-asserted-by":"crossref","unstructured":"Borrione, D., Helmy, A., Pierre, L., Schmaltz, J.: A formal approach to the verification of networks on chip. In: EURASIP Journal on Embedded Systems, 2009(Article ID 548324), 14 pp. doi: 10.1155\/2009\/548324 (2009)","DOI":"10.1155\/2009\/548324"},{"issue":"2","key":"9206_CR2","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1007\/BF00244392","volume":"4","author":"RS Boyer","year":"1988","unstructured":"Boyer, R.S., Strother Moore, J.: The addition of bounded quantification and partial functions to a computational logic and its theorem prover. J. Autom. Reason. 4(2), 117\u2013172 (1988)","journal-title":"J. Autom. Reason."},{"key":"9206_CR3","unstructured":"Boyer, R.S., Strother Moore, J.: A Computation Logic Handbook. Academic Press (1988)"},{"key":"9206_CR4","doi-asserted-by":"crossref","first-page":"306","DOI":"10.1145\/800182.810417","volume-title":"ACM 74: Proceedings of the 1974 Annual Conference","author":"RC Chen","year":"1974","unstructured":"Chen, R.C.: Deadlock prevention in message switched networks. In: ACM 74: Proceedings of the 1974 Annual Conference, pp. 306\u2013310. ACM, New York, NY, USA (1974)"},{"key":"9206_CR5","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L.: Introduction to Algorithms. MIT Press and McGraw Hill (1990)"},{"issue":"5","key":"9206_CR6","doi-asserted-by":"crossref","first-page":"547","DOI":"10.1109\/TC.1987.1676939","volume":"36","author":"WJ Dally","year":"1987","unstructured":"Dally, W.J., Seitz, C.L.: Deadlock-free message routing in multiprocessor interconnection networks. IEEE Trans. Comput. 36(5), 547\u2013553 (1987)","journal-title":"IEEE Trans. Comput."},{"key":"9206_CR7","unstructured":"Dally, W.J., Towles, B.: Principles and Practices of Interconnection Networks. Morgan Kaufmann (2004)"},{"issue":"10","key":"9206_CR8","doi-asserted-by":"crossref","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. Parallel Distrib. Syst. 6(10), 1055\u20131067 (1995)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"9206_CR9","volume-title":"Interconnection Networks: an Engineering Approach","author":"J Duato","year":"1997","unstructured":"Duato, J., Yalamanchili, S., Ni, L.: Interconnection Networks: an Engineering Approach. IEEE Computer Society Press, Los Alamitos, CA, USA (1997)"},{"issue":"7","key":"9206_CR10","doi-asserted-by":"crossref","first-page":"626","DOI":"10.1109\/71.707539","volume":"9","author":"E Fleury","year":"1998","unstructured":"Fleury, E., Fraigniaud, P.: A general theory for deadlock avoidance in wormhole-routed networks. IEEE Trans. Parallel Distrib. Syst. 9(7), 626\u2013638 (1998)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"issue":"4","key":"9206_CR11","doi-asserted-by":"crossref","first-page":"203","DOI":"10.1109\/32.588534","volume":"23","author":"M Kaufmann","year":"1997","unstructured":"Kaufmann, M., Strother Moore, J.: An industrial strengh theorem prover of a logic based on common lisp. IEEE Trans. Softw. Eng. 23(4), 203\u2013213 (1997)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"9206_CR12","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1023\/A:1026517200045","volume":"26","author":"M Kaufmann","year":"1997","unstructured":"Kaufmann, M., Strother Moore, J.: Structured theory development for a mechanized logic. J. Autom. Reason. 26(2), 161\u2013203 (1997)","journal-title":"J. Autom. Reason."},{"key":"9206_CR13","doi-asserted-by":"crossref","unstructured":"Kaufmann, M., Manolios, P., Strother Moore, J.: ACL2 Computer-Aided Reasoning: an Approach. Kluwer Academic Press (2000)","DOI":"10.1007\/978-1-4757-3188-0"},{"issue":"2","key":"9206_CR14","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1023\/B:JARS.0000009505.07087.34","volume":"31","author":"P Manolios","year":"2003","unstructured":"Manolios, P., Strother Moore, J.: Partial functions in ACL2. J. Autom. Reason. 31(2), 107\u2013127 (2003)","journal-title":"J. Autom. Reason."},{"key":"9206_CR15","first-page":"62","volume":"26","author":"LM Ni","year":"1993","unstructured":"Ni, L.M., Mckinley, P.K.: A survey of wormhole routing techniques in direct networks. IEEE Comput. 26, 62\u201376 (1993)","journal-title":"IEEE Comput."},{"key":"9206_CR16","series-title":"ACM International Conference Series","doi-asserted-by":"crossref","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). ACM International Conference Series, vol. 205, pp. 95\u201398. ACM, Seattle, WA (2006)"},{"key":"9206_CR17","volume-title":"Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, part of FloC\u201906, 14\u201315 August 2006","author":"J Schmaltz","year":"2006","unstructured":"Schmaltz, J., Borrione, D.: Towards a formal theory of on chip communications in the ACL2 logic. In: Proceedings of the Sixth International Workshop on the ACL2 Theorem Prover and its Applications, part of FloC\u201906, 14\u201315 August 2006. ACM, Seattle, WA (2006)"},{"key":"9206_CR18","doi-asserted-by":"crossref","first-page":"241","DOI":"10.1007\/s00165-007-0049-0","volume":"20","author":"J Schmaltz","year":"2008","unstructured":"Schmaltz, J., Borrione, D.: A functional formalization of on chip communications. Form. Asp. Comput. 20, 241\u2013258 (2008)","journal-title":"Form. Asp. Comput."},{"key":"9206_CR19","doi-asserted-by":"crossref","unstructured":"Schwiebert, L., Jayasimha, D.N.: A universal proof technique for deadlock-free routing in interconnection networks. In: 7th Annual ACM Symposium on Parallel Algorithms and Architectures, pp. 175\u2013184 (1995)","DOI":"10.1145\/215399.215440"},{"key":"9206_CR20","doi-asserted-by":"crossref","unstructured":"Verbeek, F., Schmaltz, J.: Formal validation of deadlock prevention in networks-on-chips. In: Ray, S., Russinoff, D. (eds.) Eighth International Workshop on the ACL2 Theorem Prover and its Application, pp. 135\u2013145, 11\u201312 May 2009. Northeastern University, Boston MA, USA. ACM (2009)","DOI":"10.1145\/1637837.1637858"},{"key":"9206_CR21","doi-asserted-by":"crossref","unstructured":"Verbeek, F., Schmaltz, J.: Formal specification of networks-on-chips: deadlock and evacuation. In: Proc. of Design, Automation, and Test in Europe (DATE\u201910), pp. 1701\u20131706 (2010)","DOI":"10.1109\/DATE.2010.5457089"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9206-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-010-9206-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-010-9206-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,4]],"date-time":"2019-06-04T21:19:25Z","timestamp":1559683165000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-010-9206-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010,9,18]]},"references-count":21,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,4]]}},"alternative-id":["9206"],"URL":"https:\/\/doi.org\/10.1007\/s10817-010-9206-x","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010,9,18]]}}}