Publications

Patents and Intellectual property rights

    G. Al Sammane, O. Ait Mohamed and S. Tahar. Integrated Circuit Testing. Ref. 15656-45USPR AD/JG/mg, Filed, January 2008.
Books

Books

  1. O. Ait Mohamed, C. Munoz and S. Tahar. Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics. Springer LNCS, 5171, August 2008.

Books Chapter

  1. O. Ait-Mohamed, X. Song, E. Cerny. On the non-termination of MDG-based abstract state enumeration. Advances in Hardware Design and Verification, 218-235, edited by H. F. Li and D. K. Probst, Chapman & Hall, 1997.

Referred Journal Papers Published/Accepted1
  1. S. Abed*, O. Ait Mohamed and G. Al Sammane*. An Abstract Reachability Approach by Combining HOL Induction and Multiway Decision Graphs. Journal of Computer Science and Technology, (September 2008, accepted with modifications).[39 pages]
  2. S. Abed, O. Ait Mohamed and G. Al Sammane. Automatic Verification of Reduction Techniques in High Order Logic. IEEE Transactions on Computers. (August 2008, accepted with modifications). [20 pages]
  3. S. Abed, O. Ait Mohamed and G. Al Sammane. Decision Diagrams based Model Checkers in High Order Theorem Provers: A Survey. Journal of Computer Science, Vol. 13, No. 3, pp. 810-817, Dec 2007.
  4. A. Habibi*, H. Moinudeen*, A. Samarah*, S. Taher, D. Li* and O. Ait Mohamed. Efficient SystemC Assertion Based Verification using TLM and Genetic Algorithms. Accepted for publication in IEEE transaction on VLSI. (Accepted 2007),
  5. O. Ait-Mohamed, X. Song, E. Cerny and S. Tahar: MDG Based State Enumeration by Retiming and Circuit Transformation; Journal of Circuits, Systems and Computers, Vol. 13, No. 5, pp. 1111-1132, October 2004, World Scientific Publishing.
  6. X. Song, M. Dharmadhikari, M. Jeske, O. Ait-Mohamed. An Efficient Algorithm for FPGA Board Routing. IEE Electronics Letters, in 2004.
  7. O. Ait Mohamed, X. Song, E. Cerny. On the non-termination of MDG-based abstract state enumeration. Theoretical Computer Science, Vol. 300, pp. 161-179, 2003, Elsevier Science Publishers.
  8. 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, Vol. 47, No.1, pp. 71-84. 2004.

Refereed Journal Papers Submitted

  1. Y. Mokhtari*, O. Ait Mohamed, S. Abed*, S. Tahar and X. Song. NuMDG: A New Approach for the Construction of Multiway Decision Graphs. Submitted to IET Software, 2007.
  2. S. Abed and O. Ait Mohamed. LCF-style Platform based on Multiway Decision Graphs. Submitted to Electronic Notes in Theoretical Computer Science (ENTCS), July 2008.
  3. S. H. Rahman, A. I. Ahmed, O. Ait Mohamed and G. Al Sammane. On The Design and Implementation of FPGA Emulation Environment of Digital Carrier Synchronizers. Submitted to Journal of Circuits, Systems, and Computers, 2007.
  4. Feng Liu, Gang Chen, O. Ait Mohamed, Qingping Tan. Formal Analysis of Prefix-based Adders. Submitted to International Journal of Computer mathematics, November 2008.

Refereed Conference Proceedings Papers

  1. Feng Liu, O. Ait Mohamed, Xiaoyu Song, Qingping Tan. A Case Study on System-Level Modeling by Aspect-Oriented Programming. In Proc. of International Sympsium The International Symposium on Quality Electronic Design (ISQED'2009, San Jose, CA, USA)
  2. S. Abed, O. Ait Mohamed and G. Al Sammane. The Performance of Combining Multiway Decision Graphs and HOL Theorem Prover. In Proc. Languages for Formal Specification and Verification, Forum on Specification & Design Languages, Stuttgart, Germany, September 23-25, 2008.
  3. Y. Mokhtari, S. Abed, O. Ait Mohamed, S. Tahar and X. Song. A New Approach for the Construction of Multiway Decision Graphs. In Proc. 5th International Colloquium on Theoretical Aspects of Computing (ICTAC'08), LNCS 5160, Istanbul, Turkey, Sept 1-3,2008.
  4. S. Abed, O. Ait Mohamed and G. Al Sammane. Multiway Decision Graphs Reduction Approach based on the HOL Theorem Prover. In Proc. Second International Workshop on Verification and Evaluation of Computer and Communication Systems, The British Computer Society, Leeds, U.K, July 2-3, 2008, pp. 1-10.
  5. S. Abed, O. Ait Mohamed and G. Al Sammane: Reachability Analysis using Multiway Decision Graphs in the HOL Theorem Prover. To appear in Proc. of the 2008 ACM symposium on Applied computing (ACM SAC '08), Fortaleza, Ceará, Brazil.
  6. T. Khan*, A. habibi*, S. Tahar and O. Ait Mohamed. Automatic Generation of SystemC Transactors from Graphical FSM. In Proc. of IEEE International Conference on Microelectronics (ICM) 2007, Egypt.
  7. S. Abed*, O. Ait Mohamed and G. Al Sammane*: Integratin SAT with Multiway Decision Graph for Efficient Model Checking. In Proc. of IEEE International Conference on Microelectronics (ICM) 2007, Egypt.
  8. S. H. Rahman*, A. I. Ahmed*, O. Ait Mohamed. FPGA Emulation Environment of Different Digital Carrier Synchronizers. IEEE International Symposium on Circuits and Systems, MWSCAS/NEWCAS'07, (August 2007).
  9. T. Khan*, A. habibi*, S. Tahar and O. Ait Mohamed. Automatic Generation of SystemC Transactors from AsmL Specification. To appear in Forum on specification & Design Languages (FDL'07), Barcelona, Spain, September 2007.
  10. S. Abed*, G. Al Sammane* and O. Ait Mohamed. Symbolic Simulation based Reduction Technique for MDGs. First International Workshop on Verification and Evaluation of Computer Systems, VEoCS'2007, May 2007.
  11. S. Abed*, O. Ait Mohamed. Towards the verification of MDGs basic operations in HOL theorem prover.In: Theorem Proving in Higher Order Logics. Emerging Trends, 2007. Proc. International Conference on Theorem Proving in Higher- Order Logics (TPHOLs'2007)-B-Track, Kaiserslautern, Germany, September 2007.
  12. D. Li*, O. Ait Mohamed and Sa'ed* Abed. Towards First-Order Symbolic Trajectory Evaluation. IEEE 37th International Symposium on Multiple-Valued Logic, ISMVL'07, (May 2007).
  13. F. Fereydouni-forouzand* and O. Ait Mohamed. A New 10 Gbps Traffic Management algorithm for High-speed Networks. IEEE International Symposium on Circuits and Systems, ISCAS'2007, (May 2007).
  14. S. Hafizur Rahman*, A. Iqbal Ahmed*, O. Ait Mohamed. Analysis and Performance Evaluation of a Digital Carrier Synchronizer for Modem Applications. IEEE International Symposium on Circuits and Systems, ISCAS'2007, (May 2007).
  15. S. Hafizur Rahman*, A. Iqbal Ahmed*, O. Ait Mohamed. FPGA Implementation and Performance Evaluation of a Digital Carrier Synchronizer using Numerically Controlled Oscillators. IEEE Canadian Conference on Electrical and Computer Engineering, CCECE'06,(April 2007)
  16. G. Al Sammane* and O. Ait Mohamed. Formal Verification of System Level Designs: A GSM Vocoder Case Study. IEEE Canadian Conference on Electrical and Computer Engineering, CCECE'06, (April 2007).
  17. S'aed Abed* and O. Ait Mohamed. Embedding of MDG Directed Formulae in HOL Theorem Prover. In Proc. of the Maghrebian Conference on Software Engineering and Artificial Intelligence. MCSEAI'06, Dec., 2006.
  18. D. Li* and O. Ait Mohamed. MDG-Based Verification of the Look-Aside-Interface. In Proc. IEEE Canadian Conference on Electrical and Computer Engineering (CCECE'06), Ottawa, Ontario, Canada, May 2006.
  19. A. Habibi*, S. Tahar, A. Samara*, D. Li*, O. Ait-Mohamed: Efficient Assertion Based Verification using TLM; Proc. IEEE/ACM Design Automation and Test in Europe (DATE'06), Munich, Germany, March 2006.
  20. D. Li* and O. Ait Mohamed. On the Formal Verification of Look-Aside-Interface using Symbolic Trajectory Evaluation. In Proc. IEEE, International Computer Systems and Information Technology Conference. Algiers, Algeria, July 2005.
  21. K. Steven* and O. Ait Mohamed. Single-Chip FPGA implementation of a pipelined, Memory Based AES Rijndael Encryption Design. In Proc. IEEE Canadian Conference on Electrical and Computer Engineering (CCECE'05), Saskatoon, Saskatchewan, Canada, May 2005.
  22. D. Li*, A.I. Ahmed*, and O. Ait Mohamed. STE Based Verification of Look-Aside Interface. In Proc. IEEE Canadian Conference on Electrical and Computer Engineering (CCECE'05), Saskatoon, Saskatchewan, Canada, May 2005.
  23. A. Habibi*, A.I. Ahmed*, O. Ait-Mohamed and S. Tahar: On the Design and Verification of the Look-Ahead Interface; Proc. IEEE/ACM Design Automation and Test in Europe (DATE'05), Munich, Germany, March 2005, pp. 290-296.
  24. A. Merhebi* and O. Ait Mohamed. FPGA implementation of a modular and pipelined WF scheduler for high speed OC192 networks. Proc. IEEE 15th Great Lakes Symposium on VLSI (GLS-VLSI'05), Chicago, Illinois, USA, April 2005.
  25. F. Fereydouni-forouzand* and O. Ait Mohamed. An FPGA Implementation of a Modified Version of a RED Algorithm. In Proc. IEEE International Conference on Field Programmable Technology (FPT'04), December 2004.
  26. A. Merhebi* and O. Ait Mohamed. A Scalable and Pipelined FPGA implementation of an OC192 WF Scheduler. In Proc. IEEE International Conference on Field Programmable Technology (FPT'04), December 2004.
  27. F. Wang*, S. Tahar, and O. Ait Mohamed. First-order LTL Model Checking using MDGs. In F. Wang (Ed.), Automated Technology for Verification and Analysis (ATVA'04), Lecture Notes in Computer Science 3299, Springer Verlag, 2004, pp. 441-455.
  28. D. Li*, M. HU, and O. Ait Mohamed. Built-In Self-Test Design of Motion Estimation Computing Array. In Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'04), June 2004.
  29. M. Krykhtin*, Y. Mokhtari*, O. Ait Mohamed, and X. Song. Towards Software Model Checking using MDGs. In Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'04), June 2004.
  30. S. Jahanpoor* and O. Ait Mohamed. Automatic Generation of Model Checking Properties and Constraints from Production Based Specification. In Proc. IEEE Midwest Symposium on Circuits and Systems (MWSCAS'04), July 2004.
Non-refereed Workshop Proceedings Papers
  1. F. Wang*, S. Tahar, and O. Ait Mohamed: Automaton based Model Checking Using Multiway Decision Graphs; Proc. 2004 Micronet Annual Workshop, Alymer, Canada, April 2004, pp. 133-134.
  2. S. Abed*, O. Ait Mohamed and G. Al Sammane*. On the Embedding and Verification of Multiway Decision Graph in HOL Theorem Prove. Technical Report 2007-1-Abed, Department of ECE, Concordia University, Montreal, Canada, Feb., 2007.
1. Names followed by asterisk (*) are supervised student or PDF co-authors