{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2023,5,25]],"date-time":"2023-05-25T04:04:24Z","timestamp":1684987464512},"reference-count":45,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"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":[[2009,1]]},"DOI":"10.1007\/s11390-009-9205-8","type":"journal-article","created":{"date-parts":[[2009,3,26]],"date-time":"2009-03-26T14:12:18Z","timestamp":1238076738000},"page":"76-95","source":"Crossref","is-referenced-by-count":4,"title":["An Abstract Reachability Approach by Combining HOL Induction and Multiway Decision Graphs"],"prefix":"10.1007","volume":"24","author":[{"given":"Sa\u2019ed","family":"Abed","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Otmane","family":"Ait Mohamed","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ghiath","family":"Al-Sammane","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2009,3,1]]},"reference":[{"key":"9205_CR1","doi-asserted-by":"crossref","unstructured":"Kropf T. Introduction to Formal Hardware Verification. Springer Verlag, 1999.","DOI":"10.1007\/978-3-662-03809-3"},{"key":"9205_CR2","doi-asserted-by":"crossref","unstructured":"Aagaard M D, Jones R B, Seger C H. Combining theorem proving and trajectory evaluation in an industrial environment. In Proc. the 1998 Conference on Design Automation (DAC-98), Los Alamitos, CA, ACM\/IEEE, Jun. 1998, pp.538\u2013541.","DOI":"10.1145\/277044.277189"},{"key":"9205_CR3","doi-asserted-by":"crossref","unstructured":"Joyce J J, Seger C H (eds.). The HOL-Voss system: Model checking inside a general-purpose theorem prover. Lecture Notes in Computer Science 780, Springer, 1994, pp.185\u2013198.","DOI":"10.1007\/3-540-57826-9_135"},{"key":"9205_CR4","unstructured":"Schneider K, Kropf T. Verifying hardware correctness by combining theorem proving and model checking. Technical Report SFB 358-C2-5\/95, Institut f\u00fcr Rechnerentwurf und Fehlertoleranz, 1995."},{"issue":"3","key":"9205_CR5","doi-asserted-by":"crossref","first-page":"313","DOI":"10.1007\/s10009-002-0082-5","volume":"4","author":"S Kort","year":"2003","unstructured":"Kort S, Tahar S, Curzon P. Hierarchical verification using an MDG-HOL hybrid tool. International Journal on Software Tools for Technology Transfer, May 2003, 4(3): 313\u2013322.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"11","key":"9205_CR6","doi-asserted-by":"crossref","first-page":"1200","DOI":"10.1016\/j.mejo.2006.07.019","volume":"37","author":"R Mizouni","year":"2006","unstructured":"Mizouni R, Tahar S, Curzon P. Hybrid verification incorporating HOL theorem proving and MDG model checking. Microelectronics Journal, November 2006, 37(11): 1200\u20131207.","journal-title":"Microelectronics Journal"},{"key":"9205_CR7","doi-asserted-by":"crossref","unstructured":"Rajan S, Shankar N, Srivas M K. An integration of model checking with automated proof checking. In Proc. the 7th International Conference on Computer Aided Verification, Wolper P (ed.), Liege, Belgium, LNCS 939, Springer Verlag, 1995, pp.84\u201397.","DOI":"10.1007\/3-540-60045-0_42"},{"key":"9205_CR8","doi-asserted-by":"crossref","unstructured":"Schneider K, Hoffmann D. A HOL conversion for translating linear time temporal logic to \u03c9-automata. In Proc. TPHOLs, Nice, France, LNCS 1690, Springer-Verlag, 1999, pp.255\u2013272.","DOI":"10.1007\/3-540-48256-3_17"},{"key":"9205_CR9","doi-asserted-by":"crossref","unstructured":"Amjad H. Programming a symbolic model checker in a fully expansive theorem prover. In Proc. the 16th International Conference on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 2758, Springer-Verlag, 2003, pp.171\u2013187.","DOI":"10.1007\/10930755_11"},{"key":"9205_CR10","doi-asserted-by":"crossref","unstructured":"Gordon M J C. Programming combinations of deduction and BDD-based symbolic calculation. LMS Journal of Computation and Mathematics, Aug. 2002, ISSN 1461-1570, 5: 56\u201376.","DOI":"10.1112\/S1461157000000693"},{"key":"9205_CR11","doi-asserted-by":"crossref","unstructured":"Gordon M J C. Reachability programming in HOL98 using BDDs. In Proc. International Conference on Theorem Proving in Higher Order Logics (TPHOLs), Portland, USA, Lecture Notes in Computer Science, August 14\u201318, 2000, pp.179\u2013196.","DOI":"10.1007\/3-540-44659-1_12"},{"key":"9205_CR12","unstructured":"Seger C H. Voss \u2014 A formal hardware verification system, user\u2019s guide. Technical report, Nortel Networks, Ottawa, Canada, The University of British Columbia, December, 1993."},{"issue":"1","key":"9205_CR13","doi-asserted-by":"crossref","first-page":"7","DOI":"10.1023\/A:1008663530211","volume":"10","author":"F Corella","year":"1997","unstructured":"Corella F, Zhou X, Song X, Langevin M, Cerny E. Multiway decision graphs for automated hardware verification. Formal Methods in System Design, February 1997, 10(1): 7\u201346.","journal-title":"Formal Methods in System Design"},{"key":"9205_CR14","unstructured":"Cadence Design Systems. V2.3. FormalCheck Users Guide, August 1999."},{"key":"9205_CR15","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K L McMillan","year":"1993","unstructured":"McMillan K L. Symbolic Model Checking. Kluwer Academic Publishers, Boston, Massachusetts, 1993."},{"issue":"8","key":"9205_CR16","doi-asserted-by":"crossref","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, August 1986, 35(8): 677\u2013691.","journal-title":"IEEE Transactions on Computers"},{"key":"9205_CR17","doi-asserted-by":"crossref","unstructured":"Aagaard M, Jones R B, Kaivola R, Kohatsu K R, Seger C H. Formal verification of iterative algorithms in microprocessors. In Proc. the 37th Conference on Design Automation (DCA\u201800), Los Angeles, California, USA, ACM, 2000, pp.201\u2013206.","DOI":"10.1145\/337292.337388"},{"key":"9205_CR18","doi-asserted-by":"crossref","unstructured":"Melham T. Integrating model checking and theorem proving in a reflective functional language. In Proc. Integrated Formal Methods: 4th International Conference (IFM 2004), Boiten E A, Derrick J, Smith G (eds.), Canterbury, UK, Lecture Notes in Computer Science 2009, Springer-Verlag, April 4\u20137, 2004, pp.36\u201339.","DOI":"10.1007\/978-3-540-24756-2_3"},{"key":"9205_CR19","doi-asserted-by":"crossref","first-page":"162","DOI":"10.1093\/comjnl\/38.2.162","volume":"38","author":"John Harrison","year":"1995","unstructured":"John Harrison. Binary decision diagrams as a HOL derived rule. The Computer Journal, 1995, 38: 162\u2013170.","journal-title":"The Computer Journal"},{"key":"9205_CR20","doi-asserted-by":"crossref","unstructured":"Pisini V, Tahar S, Curzon P, Ait-Mohamed O, Song X. Formal hardware verification by integrating HOL and MDG. In Proc. IEEE GLS-VLSI\u201900, Chicago, Illinois, USA, 2000, pp.23\u201328.","DOI":"10.1145\/330855.330947"},{"key":"9205_CR21","doi-asserted-by":"crossref","unstructured":"Mhamdi T, Tahar S. Providing automated verification in HOL using MDGs. In Proc. Automated Technology for Verification and Analysis, National Taiwan Univ., Taiwan, China, 2004, pp.278\u2013293.","DOI":"10.1007\/978-3-540-30476-0_24"},{"key":"9205_CR22","unstructured":"Xiong H, Curzon P, Tahar S, Blandford A. Providing a formal linkage between MDG and HOL. Formal Methods in Systems Design, 2006, 29(3): 1\u201336."},{"key":"9205_CR23","doi-asserted-by":"crossref","unstructured":"Reif W, Ruf J, Schellhorn G, Vollmer T. Do you trust your model checker? In Proc. Formal Methods in Computer Aided Design (FMCAD), Warren A Hunt Jr, Steven D Johnson (eds.), LNCS 1954, Springer, November 2000, pp.199\u2013216.","DOI":"10.1007\/3-540-40922-X_12"},{"key":"9205_CR24","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","year":"1993","unstructured":"Gordon M J C, Melham T F (eds.) Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, New York, NY, USA, 1993."},{"key":"9205_CR25","unstructured":"Crow J, Owre S, Rushby J, Shankar N, Srivas M. A tutorial introduction to PVS. In Workshop on Industrial-Strength Formal Specification Techniques, Boca Raton, USA, 1995."},{"key":"9205_CR26","unstructured":"Huet G, Kahn G, Paulin-Mohring C. The Coq Proof Assistant: A Tutorial. HAL-CCSd-CNRS, 2002."},{"key":"9205_CR27","doi-asserted-by":"crossref","unstructured":"Matt Kaufmann, Panagiotis Manolios, J Strother Moore. Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Jun. 2000.","DOI":"10.1007\/978-1-4615-4449-4"},{"key":"9205_CR28","doi-asserted-by":"crossref","unstructured":"Verma K N, Goubault-Larrecq J, Prasad S, Arun-Kumar S. Reflecting BDDs in Coq. In Proc. 6th Asian Computing Science Conference (ASIAN\u20182000), Penang, Malaysia, Nov. 2000, LNCS 1961, Springer, 2000, pp.162\u2013181.","DOI":"10.1007\/3-540-44464-5_13"},{"key":"9205_CR29","doi-asserted-by":"crossref","unstructured":"Ortner V, Schirmer N. Verification of BDD Normalization. In Proc. TPHOLs, Oxford, UK, 2005, pp.261\u2013277.","DOI":"10.1007\/11541868_17"},{"issue":"3","key":"9205_CR30","first-page":"810","volume":"10","author":"S Abed","year":"2007","unstructured":"S Abed, O Ait Mohamed, G Al Sammane. On the integration of decision diagrams in high order logic based theorem provers: A survey, Journal of Computer Science, 2007, 10(3): 810\u2013817.","journal-title":"Journal of Computer Science"},{"issue":"1","key":"9205_CR31","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1093\/comjnl\/47.1.71","volume":"47","author":"Y Xu","year":"2004","unstructured":"Y Xu, X Song, E Cerny, O Ait Mohamed. 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":"9205_CR32","doi-asserted-by":"crossref","unstructured":"Clocksin W, Mellish C. Programming in Prolog. Springer Verlag, 1987.","DOI":"10.1007\/978-3-642-97005-4"},{"key":"9205_CR33","unstructured":"Zhou Z, Boulerice N. MDGs tools (V1.0) user\u2019s manual. D\u2019IRO, University of Montreal, June 1996."},{"key":"9205_CR34","doi-asserted-by":"crossref","unstructured":"Gordon M, Milner R, Wadsworth C. Edinburgh LCF. Lecture Notes in Computer Science 78, Springer Verlag, 1979.","DOI":"10.1007\/3-540-09724-4"},{"key":"9205_CR35","first-page":"169","volume-title":"From LCF to HOL: A Short History. Proof, Language, and Interaction: Essays in Honour of Robin Milner","author":"M Gordon","year":"2000","unstructured":"Gordon M. From LCF to HOL: A Short History. Proof, Language, and Interaction: Essays in Honour of Robin Milner, Cambridge: MIT Press, MA, USA, 2000, pp.169\u2013185."},{"issue":"1","key":"9205_CR36","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1016\/S0304-3975(01)00345-0","volume":"300","author":"O Ait Mohamed","year":"2003","unstructured":"O Ait Mohamed, X Song, E Cerny. On the non-termination of MDG-based abstract state enumeration. Theoretical Computer Science, 2003, 300(1): 161\u2013179(19).","journal-title":"Theoretical Computer Science"},{"key":"9205_CR37","unstructured":"S Abed, O Ait Mohamed. Embedding of MDG directed formulae in HOL theorem prover. In Proc. 9th Maghrebian Conference on Software Engineering and Artificial Intelligence (MCSEAI\u201806), Agadir, Morocco, December 2006, pp.659\u2013664."},{"key":"9205_CR38","doi-asserted-by":"crossref","unstructured":"S Abed, O Ait Mohamed, G Al Sammane. A high level reachability analysis using multiway decision graphs in the HOL theorem prover. In B-Track Proc. International Conference on Theorem Proving in Higher Order Logics (TPHOLs\u201807), Kaiserslautern, Germany, September 2007, pp.1\u201317.","DOI":"10.1145\/1363686.1363774"},{"key":"9205_CR39","doi-asserted-by":"crossref","unstructured":"S Abed, O Ait Mohamed, G Al Sammane. Reachability analysis using multiway decision graphs in the HOL theorem prover. In Proc. ACM SAC\u201908, Brazil, ACM Press, 2008, pp.333\u2013338.","DOI":"10.1145\/1363686.1363774"},{"key":"9205_CR40","doi-asserted-by":"crossref","unstructured":"S Abed, O Ait Mohamed, G Al Sammane. On the embedding and verification of multiway decision graphs in HOL theorem prover. Technical Report 2007-1-Abed, ECE Department, Concordia University, Montreal, Canada, February 2007.","DOI":"10.1109\/FDL.2008.4641435"},{"key":"9205_CR41","unstructured":"Abed S. Verification of MDG algorithms. http:\/\/www.ece.concordia.ca\/~s_abed\/Project.htm ."},{"key":"9205_CR42","unstructured":"Butler R W. An introduction to requirements capture using PVS: Specification of a simple autopilot. Technical report, NASA Technical Memorandum 110255, NASA Langley Research, 1996."},{"key":"9205_CR43","unstructured":"Young W. The specification of a simple autopilot in ACL. Technical Report CLI Internal Note 327, July 1996."},{"key":"9205_CR44","unstructured":"Network Processing Forum. Look-Aside (LA-1) Interface, Implementation Agreement, Revision 1.1. Kluwer Academic Publishers, April 15, 2004."},{"key":"9205_CR45","doi-asserted-by":"crossref","first-page":"233","DOI":"10.1007\/BFb0031811","volume-title":"Proc. the First International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201896)","author":"Z Zhou","year":"1996","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 (FMCAD\u201896), London, UK, Springer-Verlag, 1996, pp.233\u2013247."}],"container-title":["Journal of Computer Science and Technology"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-009-9205-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11390-009-9205-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11390-009-9205-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,24]],"date-time":"2023-05-24T16:33:34Z","timestamp":1684946014000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11390-009-9205-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1]]},"references-count":45,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2009,1]]}},"alternative-id":["9205"],"URL":"https:\/\/doi.org\/10.1007\/s11390-009-9205-8","relation":{},"ISSN":["1000-9000","1860-4749"],"issn-type":[{"value":"1000-9000","type":"print"},{"value":"1860-4749","type":"electronic"}],"subject":[],"published":{"date-parts":[[2009,1]]}}}