{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,1]],"date-time":"2025-03-01T17:10:09Z","timestamp":1740849009303,"version":"3.38.0"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. Comput. Sci. Technol."],"published-print":{"date-parts":[[2011,1]]},"DOI":"10.1007\/s11390-011-9421-x","type":"journal-article","created":{"date-parts":[[2011,1,11]],"date-time":"2011-01-11T09:57:38Z","timestamp":1294739858000},"page":"139-152","source":"Crossref","is-referenced-by-count":2,"title":["NuMDG: A New Tool for Multiway Decision Graphs Construction"],"prefix":"10.1007","volume":"26","author":[{"given":"Sa\u2019ed","family":"Abed","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yassine","family":"Mokhtari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Otmane","family":"Ait-Mohamed","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2011,1,11]]},"reference":[{"issue":"8","key":"9421_CR1","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"RE Bryant","year":"1986","unstructured":"Bryant R E. Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers, Aug. 1986, 35(8): 677\u2013691.","journal-title":"IEEE Transactions on Computers"},{"issue":"1","key":"9421_CR2","doi-asserted-by":"crossref","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, Feb. 1997, 10(1): 7\u201346.","journal-title":"Formal Methods in System Design"},{"issue":"17","key":"9421_CR3","first-page":"955","volume":"18","author":"S Tahar","year":"1999","unstructured":"Tahar S, Song X, Cerny E, Zhou Z, Langevin M, Ait Mohamed O. Modelling and automatic verification of the fairisle ATM switch fabric using MDGs. IEEE Transactions on CAD of Integrated Circuits and Systems, Jul. 1999, 18(17): 955\u2013972.","journal-title":"IEEE Transactions on CAD of Integrated Circuits and Systems"},{"issue":"1","key":"9421_CR4","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1093\/comjnl\/47.1.71","volume":"47","author":"Y Xu","year":"2004","unstructured":"Xu Y, Song X, Cerny E, Ait Mohamed O. Model checking for a first-order temporal logic using multiway decision graphs (MDGs). The Computer Journal, 2004, 47(1): 71\u201384.","journal-title":"The Computer Journal"},{"key":"9421_CR5","unstructured":"Zhou Z. Multiway decision graphs and their applications in automatic formal verification of RTL designs [Ph.D. Dissertation]. Universite de Montreal, Canada, 1997."},{"key":"9421_CR6","doi-asserted-by":"crossref","unstructured":"Mokhtari Y, Abed S, Ait Mohamed O, Tahar S, Song X. A new approach for the construction of multiway decision graphs. In Proc. the 5th International Colloquium on Theoretical Aspects of Computing, Istanbul, Turkey, Sept. 1-3, 2008, pp. 228\u2013242.","DOI":"10.1007\/978-3-540-85762-4_16"},{"key":"9421_CR7","doi-asserted-by":"crossref","unstructured":"Fontaine P, Gribomont E P. Using BDDs with combinations of theories. In Proc. the 9th International Conference on Logic for Programming and Automated Reasoning (LPAR), Tbilisi, Geogia, Oct. 14-18, 2002, pp. 190\u2013201.","DOI":"10.1007\/3-540-36078-6_13"},{"issue":"3","key":"9421_CR8","doi-asserted-by":"crossref","first-page":"205","DOI":"10.1023\/A:1022988809947","volume":"22","author":"A Goel","year":"2003","unstructured":"Goel A, Sajid K, Zhou H, Aziz A, Singhal V. BDD based procedures for a theory of equality with uninterpreted functions. Form. Methods Syst. Des., 2003, 22(3): 205\u2013224.","journal-title":"Form. Methods Syst. Des."},{"key":"9421_CR9","doi-asserted-by":"crossref","unstructured":"Burch J R, Dill D L. Automatic verification of pipelined microprocessor control. In Proc. Int. Conf. Computer-Aided Verification, Stanford, USA, Jan. 21-23, 1994, pp. 68\u201380.","DOI":"10.1007\/3-540-58179-0_44"},{"key":"9421_CR10","doi-asserted-by":"crossref","unstructured":"Damm W, Pnueli A, Ruah S. Herbrand automata for hardware verification. In Proc. the 9th International Conference on Concurrency Theory (CONCUR1998), Nice, France, Sept. 8-11, 1998, pp. 67\u201383.","DOI":"10.1007\/BFb0055616"},{"key":"9421_CR11","doi-asserted-by":"crossref","unstructured":"Berezin S, Biere A, Clarke E, Zhu Y. Combining symbolic model checking with uninterpreted functions for out-of-order processor verification. In Proc. the Second International Conference on Formal Methods in Computer-Aided Design (FMCAD1998), Palo Alto, USA, Nov. 4-6, 1998, pp. 369\u2013386.","DOI":"10.1007\/3-540-49519-3_24"},{"key":"9421_CR12","doi-asserted-by":"crossref","unstructured":"Hojati R, Dill D L, Brayton R K. Verifying linear temporal properties of data insensitive controllers using finite instantiations. In Proc. the IFIP TC10 WG10.5 International Conference on Hardware Description Languages and Their Applications : Specification, Modelling, Verification and Synthesis of Microelectronic Systems (CHDL1997), London, UK, 1997, pp. 60\u201373.","DOI":"10.1007\/978-0-387-35064-6_5"},{"issue":"1","key":"9421_CR13","doi-asserted-by":"crossref","first-page":"93","DOI":"10.1145\/371282.371364","volume":"2","author":"R Bryant","year":"2001","unstructured":"Bryant R, German S, Velev M. Processor verification using efficient reductions of the logic of uninterpreted functions to propositional logic. ACM Trans. Comput. Logic, 2001, 2(1): 93\u2013134.","journal-title":"ACM Trans. Comput. Logic"},{"issue":"2","key":"9421_CR14","doi-asserted-by":"crossref","first-page":"73","DOI":"10.1016\/S0747-7171(02)00091-3","volume":"35","author":"MN Velev","year":"2003","unstructured":"Velev M N, Bryant R E. Effective use of Boolean satisfiability procedures in the formal verification of superscalar and VLIW microprocessors. J. Symb. Comput., 2003, 35(2): pp. 73\u2013106.","journal-title":"J. Symb. Comput."},{"key":"9421_CR15","unstructured":"Velev M. Using automatic case splits and efficient CNF translation to guide a SAT-solver when formally verifying out-of-order processors. In Proc. Artificial Intelligence and Mathematics (AI&MATH), Fort Lauderdale, USA, Jan. 4-6, 2004, pp. 242\u2013254."},{"key":"9421_CR16","unstructured":"Ackermann W. Solvable Cases of the Decision Problem. North-Holland Pub. Co., 1954."},{"key":"9421_CR17","doi-asserted-by":"crossref","unstructured":"Pnueli A, Rodeh Y, Shtrichman O, Siegel M. Deciding equality formulas by small domains instantiations. In Proc. the 11th International Conference on Computer Aided Verification (CAV1999), Trento, Italy, Jul. 6-10, 1999, pp. 455\u2013469.","DOI":"10.1007\/3-540-48683-6_39"},{"key":"9421_CR18","doi-asserted-by":"crossref","unstructured":"Rodeh Y, Shtrichman O. Finite instantiations in equivalence logic with uninterpreted functions. In Proc. the 13th International Conference on Computer Aided Verification (CAV2001), Paris, France, Jul. 18-22, 2001, pp. 144\u2013154.","DOI":"10.1007\/3-540-44585-4_13"},{"key":"9421_CR19","doi-asserted-by":"crossref","unstructured":"Bryant R E, German S M, Velev M N. Exploiting positive equality in a logic of equality with uninterpreted functions. In Proc. the 11th International Conference on Computer Aided Verification (CAV 1999), Trento, Italy, Jul. 6-10, 1999, pp. 470\u2013482.","DOI":"10.1007\/3-540-48683-6_40"},{"key":"9421_CR20","doi-asserted-by":"crossref","unstructured":"Lahiri S K, Bryant R E, Bryant A E, Goel A, Talupur M. Revisiting positive equality. In Proc. Tools and Algorithms for the Construction and Analysis of Systems, Barcelona, Spain, Mar. 29-Apr. 2, 2004, pp. 1\u201315.","DOI":"10.1007\/978-3-540-24730-2_1"},{"key":"9421_CR21","doi-asserted-by":"crossref","unstructured":"Peled D. Combining partial order reductions with on-the-fly model-checking. In Proc. the 6th International Conference on Computer Aided Veri\u00afcation (CAV1994), Stanford, USA, Jun. 1-23, 1994, pp. 377\u2013390.","DOI":"10.1007\/3-540-58179-0_69"},{"key":"9421_CR22","doi-asserted-by":"crossref","unstructured":"Kurshan R P, Levin V, Minea M, Peled D, Yenig\u00fcn, H. Static partial order reduction. In Proc. the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS 1998), Lisbon, Portugal, Mar. 28-Apr. 4, 1998, pp. 345\u2013357.","DOI":"10.1007\/BFb0054182"},{"key":"9421_CR23","doi-asserted-by":"crossref","unstructured":"Velev M. Using rewriting rules and positive equality to formally verify wide-issue out-of-order microprocessors with a reorder buffer. In Proc. The Conference on Design, Automation and Test in Europe (DATE2002), Paris, France, Mar. 4-8, 2002, p. 28.","DOI":"10.1109\/DATE.2002.998246"},{"key":"9421_CR24","doi-asserted-by":"crossref","unstructured":"Clocksin W, Mellish C. Programming in Prolog. Springer Verlag, 1987,","DOI":"10.1007\/978-3-642-97005-4"},{"key":"9421_CR25","doi-asserted-by":"crossref","unstructured":"Bahar R, Frohm E, Gaona C, Hachtel G, Macii E, Pardo A, Somenzi F. Algebraic decision diagrams and their applications. In Proc. IEEE\/ACM International Conference on Computer Aided Design, Santa Clara, California, Nov. 7-11, 1993, pp. 188\u2013191.","DOI":"10.1109\/ICCAD.1993.580054"},{"key":"9421_CR26","doi-asserted-by":"crossref","unstructured":"Cimatti A, Clarke E M, Giunchiglia E, Giunchiglia F, Pistore M, Roveri M, Sebastiani R, Tacchella A. NuSMV 2: An opensource tool for symbolic model checking. In Proc. the 14th International Conference on Computer Aided Verification (CAV2002), Copenhagen, Denmark, Jul. 27-31, 2002, pp. 359\u2013364.","DOI":"10.1007\/3-540-45657-0_29"},{"issue":"1\u20133","key":"9421_CR27","doi-asserted-by":"crossref","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, 2003, 300(1-3): 161\u2013179.","journal-title":"Theoretical Computer Science"},{"key":"9421_CR28","doi-asserted-by":"crossref","unstructured":"Zhou Z, Song X, Tahar S, Cerny E, Corella F, Langevin M. Formal verification of the island tunnel controller using multiway decision graphs. In Proc. the First International Conference on Formal Methods in Computer-Aided Design (FMCAD1996), Palo Alto, USA, Nov. 6-8, 1996, pp. 233\u2013247.","DOI":"10.1007\/BFb0031811"},{"key":"9421_CR29","doi-asserted-by":"crossref","unstructured":"Ait-Mohamed O, Cerny E, Song X. MDG-based verification by retiming and combinational transformations. In Proc. the 8th Great Lakes Symposium on VLSI, Lafayette, USA, Feb. 1998, pp. 356\u2013361.","DOI":"10.1109\/GLSV.1998.665311"},{"issue":"1","key":"9421_CR30","doi-asserted-by":"crossref","first-page":"45","DOI":"10.1006\/inco.1995.1140","volume":"122","author":"H Chen","year":"1995","unstructured":"Chen H, Hsiang J. Recurrence domains: Their unification and application to logic programming. Inform. and Comput., 1995, 122(1): 45\u201369.","journal-title":"Inform. and Comput."}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-011-9421-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-011-9421-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-011-9421-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,3,1]],"date-time":"2025-03-01T16:01:25Z","timestamp":1740844885000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-011-9421-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,1]]},"references-count":30,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2011,1]]}},"alternative-id":["9421"],"URL":"https:\/\/doi.org\/10.1007\/s11390-011-9421-x","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"type":"print","value":"1000-9000"},{"type":"electronic","value":"1860-4749"}],"subject":[],"published":{"date-parts":[[2011,1]]}}}