{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,1]],"date-time":"2025-02-01T05:25:57Z","timestamp":1738387557521,"version":"3.35.0"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540857617"},{"type":"electronic","value":"9783540857624"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-85762-4_16","type":"book-chapter","created":{"date-parts":[[2008,8,22]],"date-time":"2008-08-22T14:20:29Z","timestamp":1219414829000},"page":"228-242","source":"Crossref","is-referenced-by-count":1,"title":["A New Approach for the Construction of Multiway Decision Graphs"],"prefix":"10.1007","author":[{"given":"Y.","family":"Mokhtari","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sa\u2019ed","family":"Abed","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"O.","family":"Ait Mohamed","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"S.","family":"Tahar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"X.","family":"Song","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"8","key":"16_CR1","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers\u00a035(8), 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"issue":"2","key":"16_CR2","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008663530211","volume":"10","author":"F. Corella","year":"1997","unstructured":"Corella, F., Zhou, Z., Song, X., Langevin, M., Cerny, E.: Multiway Decision Graphs for Automated Hardware Verification. Formal Methods in System Design\u00a010(2), 7\u201346 (1997)","journal-title":"Formal Methods in System Design"},{"issue":"7","key":"16_CR3","doi-asserted-by":"publisher","first-page":"956","DOI":"10.1109\/43.771178","volume":"18","author":"S. Tahar","year":"1999","unstructured":"Tahar, S., Song, X., Cerny, E., Zhou, Z., Langevin, M., Ait Mohamed, O.: Modeling and Verification of the Fairisle ATM Switch Fabric using MDGs. IEEE Transactions on CAD of Integrated Circuits and Systems\u00a018(7), 956\u2013972 (1999)","journal-title":"IEEE Transactions on CAD of Integrated Circuits and Systems"},{"issue":"1","key":"16_CR4","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1093\/comjnl\/47.1.71","volume":"47","author":"Y. Xu","year":"2004","unstructured":"Xu, Y., Cerny, E., Song, X., Corella, F., Ait Mohamed, O.: Model Checking for A First-Order Temporal Logic using Multiway Decision Graphs. The Computer Journal\u00a047(1), 71\u201384 (2004)","journal-title":"The Computer Journal"},{"key":"16_CR5","unstructured":"Zhou, Z.: Mutliway Decision Graphs and Their Applications in Automatic Formal Verification of RTL Designs, PhD thesis, Montr\u00e9al University (1997)"},{"key":"16_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"68","DOI":"10.1007\/3-540-58179-0_44","volume-title":"Computer Aided Verification","author":"J.R. Burch","year":"1994","unstructured":"Burch, J.R., Dill, D.L.: Automatic Verification of Pipelined Microprocessor Control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol.\u00a0818, pp. 68\u201380. Springer, Heidelberg (1994)"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/BFb0055616","volume-title":"CONCUR \u201998 Concurrency Theory","author":"W. Damm","year":"1998","unstructured":"Damm, W., Pnueli, A., Ruah, S.: Herbrand Automata for Hardware Verification. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol.\u00a01466, pp. 67\u201383. Springer, Heidelberg (1998)"},{"key":"16_CR8","first-page":"187","volume":"1522","author":"S. Berezin","year":"1998","unstructured":"Berezin, S., Biere, A., Clarke, E.M., Zhu, Y.: Combining Symbolic Model Checking with Uninterpreted Functions for Out-of-Order Processor Verification. Formal Methods in Computer Aided Design\u00a01522, 187\u2013201 (1998)","journal-title":"Formal Methods in Computer Aided Design"},{"key":"16_CR9","doi-asserted-by":"crossref","unstructured":"Hojati, R., Kuehlmann, A., German, S., Brayton, R.K.: Validity Checking in the Theory of Equality with Uninterpreted Functions using Finite Instantiations. In: The International Workshop on Logic Synthesis (1997)","DOI":"10.1007\/BFb0031810"},{"key":"16_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/BFb0028749","volume-title":"Computer Aided Verification","author":"A. Goel","year":"1998","unstructured":"Goel, A., Sajid, K., Zhou, H., Aziz, A., Singhal, V.: BDD based Procedures for A Theory of Equality with Uninterpreted Functions. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 244\u2013255. Springer, Heidelberg (1998)"},{"issue":"1","key":"16_CR11","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1145\/371282.371364","volume":"2","author":"R.E. Bryant","year":"2001","unstructured":"Bryant, R.E., German, S., Velev, M.N.: Processor Verification Using Efficient Reductions of the Logic of Uninterpreted Functions to Propositional Logic. ACM Transactions on Computational Logic\u00a02(1), 93\u2013134 (2001)","journal-title":"ACM Transactions on Computational Logic"},{"key":"16_CR12","volume-title":"Solvable Cases of the Decision Problem","author":"W. Ackermann","year":"1954","unstructured":"Ackermann, W.: Solvable Cases of the Decision Problem. North-Holland Pub. Co., Amsterdam (1954)"},{"key":"16_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/3-540-48683-6_39","volume-title":"Computer Aided Verification","author":"A. Pnueli","year":"1999","unstructured":"Pnueli, A., Rodeh, Y., Shitrichman, O., Siegel, M.: Deciding Equality Formulas by Small Domain Instantiations. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 455\u2013469. Springer, Heidelberg (1999)"},{"key":"16_CR14","doi-asserted-by":"crossref","unstructured":"Velev, M.N.: Using Rewriting Rules and Positive Equality to Formally VerifyWide-issue Out-of-Order Microprocessors with Reorder Buffer. In: Proc. of DAC, pp. 28\u201335 (2002)","DOI":"10.1109\/DATE.2002.998246"},{"key":"16_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-97005-4","volume-title":"Programming in Prolog","author":"W. Clocksin","year":"1987","unstructured":"Clocksin, W., Mellish, C.: Programming in Prolog, 3rd edn. Springer, Heidelberg (1987)","edition":"3"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Bahar, R., Frohm, E., Gaona, C., Hatchel, G., Macii, E., Pardo, A., Sommenzi, F.: Algebraic Decision Diagrams and their Applications. In: Proc. of International Conference on Computer-Aided Design, pp. 188\u2013191 (1993)","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"16_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_29","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"2002","unstructured":"Cimatti, A., Clarke, E., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, Springer, Heidelberg (2002)"},{"key":"16_CR18","doi-asserted-by":"publisher","first-page":"161","DOI":"10.1016\/S0304-3975(01)00345-0","volume":"300","author":"O. Ait Mohamed","year":"2003","unstructured":"Ait Mohamed, O., Song, X., Cerny, E.: On the Non-termination of MDG-based Abstract State Enumeration. Theoretical Computer Science\u00a0300, 161\u2013179 (2003)","journal-title":"Theoretical Computer Science"},{"key":"16_CR19","unstructured":"Mokhtari, Y., Abed, S., Ait Mohamed, O., Tahar, S., Song, X.: A New Approach for the Construction of Multiway Decision Graphs. Technical Report 2008-3-Abed, ECE Department, Concordia University, Montreal, Canada (June 2008)"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computing - ICTAC 2008"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-85762-4_16.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,31]],"date-time":"2025-01-31T16:48:34Z","timestamp":1738342114000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-85762-4_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540857617","9783540857624"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-85762-4_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[]}}