Dr. Otmane Ait Mohamed, PhD, ing.

Education

Interests

Digital Design (COEN313)

Computer Architecture (COEN316)

Functional Hardware Verification  (COEN413/COEN6541)

Current Projects

Edited Books

[1]         A. Abdelmalek, O. AitMohamed, and B. Benatallah. Network Security Technologies: Design andApplications. IGI Global, 2014. 1-330. Web. 8 Jan. 2015.doi:10.4018/978-1-4666-4789-3

[2]         A. Amine, O. Ait Mohamedand L. Bellatreche. Modeling Approaches and Algorithms for Advanced ComputerApplications. Studies in Computational Intelligence. Volume 488,  2013.ISBN: 978-3-319-00559-1 (Print) 978-3-319-00560-7 (Online)

[3]         S. Abed* and O. Ait Mohamed.The Verification of MDG Algorithms in the HOL Theorem Prover. LAP LambertAcademic Publishing, October 13, 2009.ISBN: 978-3838317380.

Edited Journals

[1]         L. Bellatreche, A. Amine, O.Ait Mohamed. Special issue on contributions of computational intelligencein designing complex information systems. Computing Journal, V. 7,  no. 7, p. 663, Year: 2015.

Edited Proceedings

[1]         O. Ait Mohamed, Amine Abdelmalek, Zakaria El Berichi. Proceedings of the 2ndConference Internationale sur l'Informatique et ses Applications (CIIA 2009),May 2009, Saida, Algeria.

[2]         O. Ait Mohamed, C. Munoz and S. Tahar. Proceedings of the 21st InternationalConference on Theorem Proving in Higher Order Logics. Springer LNCS, 5171,August 2008.

Books Chapters

[1]         K.A. Hoque*, O. Ait Mohamed, Y. Savaria, C. Thibeault. Early Analysis ofSoft Error Effects for Aerospace Applications Using Probabilistic ModelChecking. Formal Techniques for Safety-Critical Systems - Second International Workshop,{FTSCS} 2013, Queenstown, New Zealand, October 29-30, 2013. Revised Selected Papers. Communicationsin Computer and Information Science Series, Springer-Verlag. (~33 % acceptance rate).

[2]         J.Mani Paret*, O. Ait Mohamed.  Coveragedriven test generation and consistency algorithm. Revised Selected Papers. In Declarative Programming andKnowledge Management, Lecture Notes in Artificial Intellegence, Springer, 2013,pp: 136-152.

[3]         S.Ouchani*, O. Ait Mohamed, M. Debbabi. Efficient ProbabilisticAbstraction for SysML Activity Diagrams. Software Engineering and FormalMethods. 10th International Conference, SEFM’2012, Greece, October, 2012. LNCS7504, pp. 263-277. (~18 % acceptance rate).

[4]         S.Ouchani*, O. Ait Mohamed, M. Debbabi, M. Pourzandi. Verification of theCorrectness in Composed UML Behavioural Diagrams. Software Engineering,Research, Management and Application 2010, pp. 163-176, edited by Roger Lee,Springer Verlag, 2010.

[5]         Y.Mokhtari*, S. Abed*, O. Ait Mohamed, S. Tahar and X. Song. A NewApproach for the Construction of Multiway Decision Graphs. Theoretical Aspectsof Computing - {ICTAC} 2008, 5th International Colloquium, Istanbul, Turkey,September 1-3, 2008. Proceedings, LNCS 5160, pp. 228-242.

Referred Journal Papers Published/Accepted

[1]         K. A. Hoque*, O. Ait Mohamed,Y. Savaria. Formal analysis of SEU mitigation for early dependability andperformability analysis of FPGA-based space applications. Journal of AppliedLogic. Volume ??, Number ??, Pages ??, March 2017.

[2]         A. Baouya*, D. Bennouar, O. AitMohamed, S. Ouchani*. A Quantitative Verification Framework of SysMLActivity Diagrams under Time Constraints. Expert Systems with Applications. Volume42, Issue 21, 30 November 2015, Pages 7493-7510 (I.F, 2.240, 5years I.F., 2.501).

[3]         G. Bany Hamad*, S. Hasan, O.Ait Mohamed,  Y. Savaria (2014). Newinsights into the single event transient propagation through static and TSPClogic. IEEE Transactions on Nuclear Science, vol.61, no.4, pp.1618,1627 (I.F,1.283)

[4]         G. Bany Hamad*, O. Aït Mohamed,S. Rafay, Yvon Savaria. Characterizing, Modeling, and Verifying Soft ErrorPropagation in Asynchronous and Synchronous Circuits. MicroelectronicsReliability, Elsevier, Volume  55, no. 1 (2015), Pages 238-250. (I.F,1.137, 5 years I.F., 1.201).

[5]         M. Ammar*, S. Ouchani*, O.Aït Mohamed. Symmetry Reduction ofTime-Triggered Ethernet Protocol. Procedia Computer Science, Elsveir, Volume19, 2013, pages 273-280.

[6]         S. Ouchani*, O. Aït Mohamed, M.Debbabi. A Property-Based Abstraction Framework for SysML Activity Diagrams. Knowledge-BasedSystems, Elsvier, Volume 56, 2014, Pages 328-343 (I.F, 2.947, 5 years I.F, 3.011), 

[7]         S. Ouchani*, O. Aït Mohamed, M.Debbabi. A Formal Verification Framework for SysML Activity Diagrams. ExpertSystems With Applications, Elsvier, Volume 41, Issue 6, May 2014, Pages2713–2728 (I.F, 1.854, 5 years I.F., 2.339).

[8]         S. Abed*, O. Ait Mohamedand G. Al Sammane*. Automatic Verification of Reduction Techniques in HighOrder Logic. Formal Aspects ofComputing: Volume 25, Issue 6 (2013), Page 971-991 (I.F, 0.806)

[9]         Samir Ouchani*, Y.Jarraya, O. Aït Mohamed, M. Debbabi: Probabilistic Attack Scenariosto Evaluate Policies over Communication Protocols. JSW 7(7):1488-1495 (2012) (I.F, 1.273)

[10]      Iqbal Ahmed*, S. HafizurRahman*, O. Ait-Mohamed, S. Abed*. Towards an FPGA implementation andperformance evaluation of a Digital Carrier Synchronizer with a portableemulation environment. Int. J. Computer Applications in Technology, Vol. 45,No. 1, pp.66–76.

[11]      S. Abed*, O. Ait Mohamedand G. Al Sammane*. Automatic Verification of Reduction Techniques in HighOrder Logic.   Formal Aspect ofComputing,  Online First™, 13 February2012. [21 pages ], Springer London. DOI 10.1007/s00165-012-0223-x. (2011, I.F,0.463).

[12]      Feng Liu*, QingPing, O. AitMohamed. Formal proof of integer adders using all-prefix-sums operation.SCIENCE CHINA Information Sciences. Science China Press, co-published with Springer.  [12 pages]. doi: 10.1007/s11432-011-4331-7,11 August 2011.

[13]      K. Anuarul Hoque*, O. AitMohamed, S. Abed*, M. Boukkadoum. MDG-SAT: An Automated Methodology forEfficient Safety Checking. International Journal of Critical Computer-BasedSystems. Interscience publisher. Volume 3, No. 1/2. DOI:10.1504/IJCCBS.2012.045074.

[14]      S. Abed*, K. Hussein*, O.Ait Mohamed. Abstract Property Language for MDG Model Checking Methodology.Int. J. Computer Applications in Techology. Volume 44,  No. 1. pp 23-36.

[15]      S. Abed*, Y. Mokhtari*, O.Ait Mohamed, S. Tahar. NuMDG: A New Tool for Multiway Decision GraphsConstruction. J. of Computer Science & Technology (JCST). Springer Boston,Vol. 26, No. 1, pp. 139-152, Jan. 2011, DOI 10.1007/s11390-011-1117-8.

[16]      A.Fermas*, A. Belouchrani, O. Ait Mohamed. Floating-Point Scaling for BSS Gain Control.Int. J. Computer and Information Engineering 4:2 2010, World Academy ofScience, Engineering and Technology.

[17]      S. Abed* and O. Ait Mohamed.LCF-style Platform based on Multiway Decision Graphs. Electronic Notes inTheoretical Computer Science (ENTCS), Elsevier, Volume 246, pp. 3-26, August2009.

[18]      S. Abed*, O. Ait Mohamedand G. Al Sammane*. An Abstract Reachability Approach by Combining HOLInduction and Multiway Decision Graphs. Journalof Computer Science and Technology. JCST,Vol. 24 (1): 76-95, January 2009.

[19]      S. Abed*, O. Ait Mohamedand G. Al Sammane*. On the Integration of Decision Diagrams in High Order Logicbased Theorem Provers: a Survey. Journalof Computer Science, Vol. 13, No. 3, pp. 810-817, December 2007.

[20]      O. Ait Mohamed, X. Song, E. Cerny, S. Tahar and Zijian Zhou : MDG Based StateEnumeration by Retiming and Circuit Transformation. Journal of Circuits, Systems and Computers, Vol. 13, No. 5, pp.1111-1132, October 2004, World Scientific Publishing.

[21]      X.Song, M. Dharmadhikari, M. Jeske, O. Ait Mohamed. An Efficient Algorithm for FPGA Board Routing. IEE Electronics Letters, Vol. 40, No. 18, April 2004. [2 pages]

[22]      O. Ait Mohamed, X. Song, E. Cerny. On the non-termination of MDG-based abstractstate enumeration. Theoretical ComputerScience, Vol. 300, pp. 161-179,2003, Elsevier Science Publishers.

[23]      Y.Xu, X. Song, E. Cerny, O. Ait Mohamed. ModelChecking for a First-Order Temporal Logic using Multiway Decision Graphs(MDGs). The Computer Journal, Vol.47, No.1, pp. 71-84. 2004.

Refereed Conference Proceedings Papers

[1]         G. Bany Hamad*, G. Kazma*, O.Ait Mohamed, and Y. Savaria. Efficient and Accurate Analysis of SingleEvent Transients Propagation Using SMT-Based Techniques. To appear in the IEEE InternationalConference on Computer-Aided Design (ICCAD), November 2016.

[2]         M. Ammar*, G. Bany Hamad*, O. Ait Mohamed, and Y. Savaria.Efficient Probabilistic Fault Tree Analysis of Safety Critical Systems viaProbabilistic Model Checking. In IEEE Forum on Design Languages,FDL’2016, pp. 57-64, Bremen, Sept. 2016

[3]         G. Bany Hamad*, G. Kazma*, O. Ait Mohamed and Y. Savaria.Comprehensive Non-Functional Analysis of Combinational Circuits Vulnerabilityto Single Event Transients. In IEEE Forum on Design Languages,FDL’2016, pp. 50-56, Bremen, Sept. 2016

[4]         M. M. Baba, O. Ait Mohamed, F. Awwad, and M. I. Daoud. A Low-Cost Camera-basedTransducer Tracking System for Freehand Three-Dimensional Ultrasound.  In the proceeding ofthe 14th IEEE International NEWCAS conference (NEWCAS 2016), Vancouver,Canada, June 26- 29, 2016.

[5]         M.H. Askarihemmat*, O.Ait Mohamed, M. Boukadoum. Towards Code Generation for Arm Cortex-MMCUs from SysML Activity Diagrams. In the 2016 IEEE International Symposium onCircuits and Systems (ISCAS’2016), Montreal, Canada. (May 22 – 25, 206).

[6]         G. Bany Hamad*, O. AitMohamed,  Y. Savaria. Towards FormalAbstraction, Modeling, and Analysis of Single Event Transients at RTL. In the2016 IEEE International Symposium on Circuits and Systems (ISCAS’2016),Montreal, Canada. (May 22 – 25, 206).

[7]         M.H. Askarihemmat*, O.Ait Mohamed, M. Boukadoum. Formal Modeling, Verification and Implementation ofa Train Control System. In27^th IEEE International Conference in Microelectronics (ICM’2015),Dec 19-23, 2015, Casa Blanca, Morocco.

[8]         J. Mani Paret*, O. AitMohamed.  A Methodology To GenerateEvenly Distributed Input Stimuli By Clustering Of Variable Domain. In The 33^rd IEEE International Conference on Computer Design , October 18- 21,2015, New York City, USA (~30 % acceptance rate).

[9]         A. Baouya*, D. Bennouar, O.Ait Mohamed, S. Ouchani*. A probabilistic and timed verification approachof SysML state machine diagram. In the 12^th IEEE InternationalSymposium for Programming and Systems (ISPS’2015), April 28-30, 2015, Algiers,Algeria.

[10]      G. Bany Hamad, O. AitMohamed, and Y. Savaria. “Efficient Multilevel Formal Modeling, Analysis,and Estimation of Design Vulnerability to Soft Error”, in the 21st IEEEInternational On-Line Testing Symposium, Athena Pallas Village, Greece, July6-8, 2015.

[11]      M.H. Askarihemmat*, O.Ait Mohamed, M. Boukadoum. Automatic mapping of AF3 specifications toARM cortex-M based FRDM platfrom. In 26^th IEEE InternationalConference n Microelectronics (ICM’2014), Dec 14-17, 2014, Doha, Qatar.

[12]      K. A. Hoque*, O. Ait Mohamed,Y. Savaria, C. Thibeault. Probabilistic Model Checking Based DAL Analysis toOptimize a Combined TMR-Blind-Scrubbing Mitigation Technique for FPGA-BasedAerospace Applications. In the 12th  ACM-IEEE International Conference on FormalMethods and Models for System Design (MEMOCODE'14),  Lausanne, Switzerland,  October 19-21, 2014.

[13]      K.A. Hoque*, O. Ait Mohamed, Y. Savaria. TowardsAn Accurate Reliability, Availability and Maintainability Analysis Approach forSatellite Systems Based on Probabilistic Model Checking.  In the the 18th International Conference onDesign Automation and Test in Europe (DATE’2015), Gerenoble, France, March9-13, 2015 (~22% acceptance rate).

[14]      J.Mani Paret*, O. Ait Mohamed.  Optimum domain partitioning to increase functional verificationcoverage. In the 16th International Symposium on Quality Electronic Design(ISQED 2015), Santa Clara, CA, USA.

[15]      G. Bany Hamad*, S. Rafay, O.Aït Mohamed, Yvon Savaria. ProbabilisticModel Checking of Single Event Transient Propagation at RTL Level. In the 2014 21^st IEEE International Conference onElectronics Circuits & Systems, ICECES’2014.

[16]      G. Bany Hamad*, S. Rafay, O.Aït Mohamed, Yvon Savaria. Modeling, Analyzing, and Abstracting SingleEvent Transient Propagation at Gate Level. In the 2014 IEEE 57th InternationalMidwest Symposium on Circuits and Systems (MWSCAS 2014), Texas, USA. (Aug 3-5,2014).

[17]      G. Bany Hamad*, S. Rafay, O.Aït Mohamed, Yvon Savaria. Abstracting Single Event Transient PropagationCharacteristics to Support Gate Level Modeling. In the 2014 IEEE InternationalSymposium on Circuits and Systems (ISCAS’2014), Melbourne, Australia.ISCAS’2014. (June 1-5, 2014).

[18]      S. Ouchani*, O. Ait Mohamed,M. Debbabi. A Security Risk Assessment Framework for SysML  Activity Diagrams. The 7th  IEEE International Conference on SoftwareSecurity and Reliability (SERE’2013), June 18-20, 2013, Washington, D.C.,  (USA).

[19]      M. Ammar*, S. Ouchani* and O.Ait Mohamed. Symmetry Reduction ofTime-Triggered Ethernet Protocol. The 4th International Conference on Ambient Systems, Networks andTechnologiesJune 25-28, 2013, Halifax, Nova Scotia, Canada.

[20]       S. Ouchani*, O. Ait Mohamed, M. Debbabi. A formal verification framework for BluespecSystem Verilog. Specification & Design Languages (FDL), 2013 Forum on,Paris, France (24-26 Sept. )

[21]       J. Mani Paret*, O. Ait Mohamed.A coverage driventest generation methodology using consistency algorithm. Quality ElectronicDesign (ASQED), 2013 5^th  AsiaSymposium on, Penang, Malysia, August 26-28, 2013.

[22]      S. Ouchani*, O. Ait Mohamed,M. Debbabi. A probabilistic verification framework of SysML activitydiagrams. IEEE 12th International Conference on Intelligent SoftwareMethodologies, Tools and Techniques, SoMeT 2013, Budapest, Hungary, September22-24, 2013. IEEE 2013 ISBN 978-1-4799-0419-8

[23]      G. Bany Hamed*, S. Rafay , O.Ait Mohamed, , Y. Savaria. Investigating the Impact of Input Patterns, Propagation Paths, andRe-convergent Paths on the Propagation Induced Pulse Broadening. In Radiation Effects on Components and Systems conference 2013(Radecs’2013), Oxford, UK from 23^rd - 27^th September2013.

[24]      S. Ouchani*, O. Ait Mohamed,M. Debbabi. ANon-Convex Classifier Support for Abstraction-Refinement Framework. The 23th IEEE  International Conference onMicroelectronics (ICM’2012). December 17-20, 2012, in Algiers (Algeria).

[25]      S.Ganaesh*, F. Fereydouni Forouzandeh*, O. Ait Mohamed. Performance Analysis of TBCD Protocol over Wireless Body Channel. Inthe proceeding of the 55th IEEE Midwest Symposium on Circuits andSystems,Boise,  Idaho, USA, August 5-8,2012.

[26]      J.Mani Paret*, O. Ait Mohamed. Modeling DiscreteEvent System with Distributions using SystemVerilog.  In the proceeding of the 2012 IEEEInternational Symposium on Circuits and Systems (ISCAS 2012), Seoul, Korea, May20,-23.

[27]      G. Bany Hamed*, O. AitMohamed, S. Rafay, Y. Savaria. Identification of Soft Error Glitch-PropagationPaths: Leveraging SAT solvers.  In theproceeding of the 2012 IEEE International Symposium on Circuits and Systems(ISCAS 2012), Seoul, Korea, May 20,-23, 2012.

[28]      Z. Al-Bayati*, O. AitMohamed, Y. Savaria, M. Boukadoum. Probabilistic Model Checking of ClockDomain Crossing Interfaces. In the proceeding of the 10th IEEE InternationalNEWCAS conference (NEWCAS 2012), Montreal, Canada, June 17- 20, 2012.

[29]      Z. Al-Bayati*, O. AitMohamed, S. Rafay. Y. Savaria. A Novel Hybrid FIFO-Asynchronous ClockDomain Crossing (CDC) Interfacing Method. In the proceeding of the The 22ndedition of GLSVLSI, Salt Lake City, Utah, USA, May 3-4, 2012.

[30]      G. Bany Hamed*, O. AitMohamed, S. Rafay, Y. Savaria. SEGP-Finder: Tool for Identification of SoftError Glitch-Propagating Paths at Gate level. In the proceeding of the IEEEInternational Conference on Electronics, Circuits, and Systems (ICECS’2011).,Beyrout, Lebanon, Dec 11-14, 2011.

[31]      S.Ouchani*, Y. Jarraya, O. Ait Mohamed. Model-basedSystems Security quantification. In the proceeding of the 9th Annual Conference
on Privacy, Security and Trust (PST’2011), 
Montreal, Quebec, Canada, July19-21, 2011.

[32]      S.Ouchani*, Y. Jarraya, O. Ait Mohamed, M. Debbabi. Security Estimation in Streaming Protocol. In Proc. of the IEEEInternational Conference on Innovations in Information Technology, Abu-Dhabi,UAE, April 2011.

[33]      Khaza Anuarul Hoque*, O. AitMohamed, S. Abed*, M. Boukadoum. An Automated SAT Encoding-VerificationApproach for Efficient Model Checking. In IEEE International Conference onMicroelectronics (ICM), Egypt Dec. 19-22, 2010, 419-422.

[34]      Khaza Anuarul Hoque*, O. AitMohamed, S. Abed*, M. Boukadoum. SAT Based Model Checking for MDG Models.In Proc. IEEE-Northeast Workshop on Circuits and Systems Conference(NEWCAS-2010), Montreal, June 20-23, 2010. pp-241-244. “Best Paper Award”

[35]      F. Fereydouni Forouzandeh*, O.Ait Mohamed, M. Sawan, and F. Awwad. Delay Calculation and ErrorCompensation in TBCD-TDM Communication Protocol for Wireless Body SensorNetworks. In Proc. IEEE-Northeast Workshop on Circuits and Systems Conference(NEWCAS’2010), Montreal, June 20-23, 2010, pp 17-20.

[36]      S. Abed* and O. Ait Mohamed.MDGs Reduction Technique Based on the HOL Theorem Prover. In Proc. of the 40thIEEE International Symposium on Multiple-Valued Logic, ISMVL’2010, Barcelona,Spain, May 26-28, 2010. pp-15-20.

[37]      S. Ouchani*, O. Ait Mohamed,M. Debbabi, M. Pourzandi: Verification of the Correctness in Composed UMLBehavioural Diagrams. SERA (selected papers) 2010: 163-177

[38]      F. Fereydouni Forouzandeh, O.Ait Mohamed, M. Sawan, and F. Awwad. TBCD-TDM:Novel Ultra-Low Energy Protocol for Implantable Wireless Body Sensor Networks.To appear in IEEE Globecom 2009 Ad Hoc, Sensor and Mesh Networking Symposium.

[39]      Saad El Mansori*, O. AitMohamed, Falah Awwad. Static slicing-Based Pre-Reduction Technique for MDGModel-checker. IEEE International Conference on Innovations in InformationTechnology, Al-Ain, UAE, December 2009.

[40]      S. Abed*, K. Hussein*, O.Ait Mohamed.Processing APL Properties to Generate Verification- Ready MDGModel. IEEE International Conference on Microelectronics (ICM 2009), Marakech,Moroco, December 2009.

[41]      Sae’d Abed, Sahel Alouneh and O.Ait Mohamed, Reliability of Recursive Concentrator Structure", InProc. IEEE Symposium on Industrial Electronics & Applications (IEEEISIEA'09), Kuala Lumpur, Malaysia, October 4-6, 2009, pp. 209-211.

[42]      A.Fermas*, A. Belouchrani, O. Ait Mohamed. Hardware Implementation of Free Division Block-basedBSS Algorithm. In Proc. IEEE-Northeast Workshop onCircuits and Systems and TAISA Conference (NEWCAS-TAISA’2008)

[43]      S. Zhang*, A. I. Ahmed*, O.Ait Mohamed. A Re-Usable VerificationFramework of Open Core Protocol (OCP). In Proc. IEEE-Northeast Workshop onCircuits and Systems and TAISA Conference (NEWCAS-TAISA’2008).

[44]      L. Feng*, F. FereydouniForouzandeh*, O. Ait Mohamed, G. Chen, X. Song, Q. Tan. A Compatative Study of Parallel PrefixAdders in FPGA Implementation of EAC. in the 12th EUROMICRO Conference onDigital System Design; Architectures, Methods and Tools, 27-29 August 2009,Patras, Greece.

[45]      Feng Liu*, O. Ait Mohamed,Xiaoyu Song, Qingping Tan. A Case Study on System-Level Modeling byAspect-Oriented Programming. In Proc. of International Sympsium TheInternational Symposium on Quality Electronic Design (ISQED’2009, San Jose, CA,USA)

[46]      S. Abed*, O. Ait Mohamedand G. Al Sammane*. The Performance ofCombining Multiway Decision Graphs and HOL Theorem Prover. In Proc.Languages for Formal Specification and Verification, Forum on Specification& Design Languages (IEEE FDL'08), Stuttgart, Germany, September 23-25,2008.

[47]      S. Abed* and O. Ait Mohamed.LCF-style Platform based on MultiwayDecision Graphs. In Proc. 17th Workshop on Functional and (Constraint)Logic Programming (WFLP'08), Siena, Italy, July 3-4, 2008, pp. 139-153.

[48]      S. Abed*, O. Ait Mohamedand G. Al Sammane*. Multiway DecisionGraphs Reduction Approach based on the HOL Theorem Prover. In Proc. SecondInternational Workshop on Verification and Evaluation of Computer andCommunication Systems (VECoS'08), The British Computer Society, Leeds, U.K,July 2-3, 2008, pp. 1-10.

[49]      F. Fereydouni Forouzandeh*, O.Ait Mohamed and M. Sawan. Ultra lowenergy communication protocol for implantable body sensor networks. 2008Joint 6th International IEEE Northeast Workshop on Circuits and Systems andTAISA Conference, 2008, 22-25 June 2008 Page(s):57 - 60.

[50]      S. Abed* and O. Ait Mohamed.The MDG-HOL Platform for Automatic Verification. In Proc. 10th MaghrebianConference on Software Engineering and Artificial Intelligence (MCSEAI'08),Algeria, April, 2008, pp. 659-664.

[51]      A. I. Ahmed*,K. Hussain*, O. Ait Mohamed and G. Al Sammane*. Modeling and Verification ofDSP Components with Multiway Decision Graphs: The FIR Filter Case Study. InProc. of the First International Conference on Embedded Systems & CriticalApplications, May 2008 , Tunisia, [ 6 pages].

[52]      S. Abed*, O. Ait Mohamedand G. Al Sammane*: Reachability Analysis using Multiway Decision Graphs in theHOL Theorem Prover. in Proc. of the ACM Symposium on Applied Computing (SAC'08), Fortaleza, Brazil, March 2008. [6 pages].

[53]      S. Abed*, O. Ait Mohamed,Zijiang Yang and G. Al Sammane*: Integratin SAT with Multiway Decision Graphfor Efficient Model Checking. Proc. ofIEEE International Conference on Microelectronics (ICM’07), Cairo, Egypt,December 2007, pp. 134-137.

[54]      T. Khan*, A. habibi, S. Taharand O. Ait Mohamed. Automatic Generation of SystemC Transactors fromGraphical FSM. Proc. of IEEEInternational Conference on Microelectronics (ICM’07), Cairo, Egypt,December 2007, pp. 271-274.

[55]      T. Khan*, A.habibi, S. Tahar and O. Ait Mohamed. Automatic Generation of SystemCTransactors from AsmL Specification. Proc.Forum on specification & DesignLanguages (FDL’07), Barcelona, Spain, September 2007, pp. 104-109.

[56]      S. Abed*, O.  Ait Mohamed. Towards the verification ofMDGs basic operations in HOL theorem prover. Proc. International Conference on Theorem Proving in Higher OrderLogics (TPHOLs’07), Kaiserslautern, Germany, September 2007, pp. 1-16.

[57]      S. H. Rahman*, A. I. Ahmed*, O.Ait Mohamed and G. Al Sammane*. FPGA Emulation Environment of DifferentDigital Carrier Synchronizers. Proc. IEEE International Northeast Workshop in Computers and Systems(NEWCAS’07), Montreal, Quebec, Canada, August 2007, pp. 510-513.

[58]      S. Abed*, G. Al Sammane* and O.Ait Mohamed. Symbolic Simulationbased Reduction Technique for MDGs. Proc.BCS(eWiC) International Workshop onVerification and Evaluation of Computer Systems (VEoCS’07), Algiers,Algeria, May 2007. [14 pages].

[59]      D. Li* , S. Abed* and O. AitMohamed. Towards First-Order Symbolic Trajectory Evaluation. Proc. IEEE 37^th International Symposiumon Multiple-Valued Logic (ISMVL’07), Oslo, Norway, May 2007, pp. 53-59.

[60]      S. H. Rahman*, A. I. Ahmed*, O.Ait Mohamed. Analysis and Performance Evaluation of a Digital CarrierSynchronizer for Modem Applications.Proc. IEEE International Symposium on Circuits and Systems (ISCAS’07), Lafayette,New Orleans, USA, May 2007, pp.417-420.

[61]      F. Fereydouni-Forouzand* and O.Ait Mohamed. A New 10 Gbps Traffic Management algorithm for High-speedNetworks. Proc. IEEE International Symposium on Circuits and Systems (ISCAS’07), Lafayette,New Orleans, USA, May 2007, pp. 2510-2513.

[62]      S. Hafizur Rahman*, A. IqbalAhmed*, O. Ait Mohamed. FPGA Implementation and Performance Evaluationof a Digital Carrier Synchronizer using Numerically Controlled Oscillators. Proc. IEEE Canadian Conference on Electricaland Computer Engineering, (CCECE’07), Vancouver, British Columbia, Canada,April 2007, pp.1243-1246.

[63]      G. Al Sammane* and O. AitMohamed. Formal Verification of System Level Designs: A GSM Vocoder CaseStudy. Proc. IEEE Canadian Conference onElectrical and Computer Engineering(CCECE’07), Vancouver, BC, Canada, April2007, pp. 1413-1416.

[64]      S. Abed* and O.Ait Mohamed. Embedding of MDG Directed Formulae in HOL Theorem Prover. Proc. of the Maghrebian Conference onSoftware Engineering and Artificial Intelligence (MCSEAI’06), Agadir,Morocco, December 2006. [6 pages].

[65]      D. Li* and O. Ait Mohamed.MDG-Based Verification of Look-Aside-Interface.Proc. IEEE Canadian Conference on Electrical and Computer Engineering (CCECE’06),Ottawa, Ontario, Canada, May 2006, pp.899- 903.

[66]      A. Habibi, S.Tahar, A. Samara, D. Li*, O. Ait Mohamed: Efficient Assertion Based Verification using TLM. Proc. IEEE/ACM DesignAutomation and Test in Europe (DATE’06), Munich, Germany, March 2006. [6pages].

[67]      D. Li* and O. Ait Mohamed.On the Formal Verification of Look-Aside-Interface using Symbolic TrajectoryEvaluation. Proc. International ComputerSystems and Information Technology Conference(ICSIT’05) , Algiers, Algeria,July 2005, pp.356- 361.

[68]      K. Steven* and O. AitMohamed. Single-Chip FPGA implementation of a pipelined, Memory Based AESRijndael Encryption Design. Proc. IEEECanadian Conference on Electrical and Computer Engineering (CCECE’05), Saskatoon,Saskatchewan, Canada, May 2005, pp.1296-1299.

[69]      D. Li*, A.I. Ahmed*, and O.Ait Mohamed. STE Based Verification of Look-Aside Interface. Proc. IEEE Canadian Conference on Electricaland Computer Engineering (CCECE’05), Saskatoon, Saskatchewan, Canada, May2005, pp. 669-672.

[70]      A. Habibi, A.I. Ahmed*, O. Ait Mohamed and S. Tahar:On the Design and Verification of the Look-Ahead Interface. Proc. IEEE/ACM DesignAutomation and Test in Europe (DATE'05), Munich, Germany, March 2005, pp.290-296.

[71]      A. Merhebi*and O. Ait Mohamed.  FPGA implementation of a modular andpipelined WF scheduler for high speed OC192 networks. Proc. IEEE 15th Great Lakes Symposium on VLSI (GLS-VLSI'05), Chicago, Illinois, USA, April 2005, pp. 422-425.

[72]      F. Fereydouni-Forouzand* and O.Ait Mohamed. An FPGA Implementation of a Modified Version of a REDAlgorithm. Proc.  IEEE International Conference on FieldProgrammable Technology (FPT'04), Brisbane, Australia, December 2004, pp. 425-428.

[73]      A. Merhebi* and O. AitMohamed. A Scalable and Pipelined FPGA implementation of an OC192 WFScheduler. Proc.  IEEE InternationalConference on Field Programmable Technology (FPT'04), Brisbane, Australia, December 2004, pp.395-398.

[74]      F. Wang, S. Tahar, and O.Ait Mohamed. First-order LTL Model Checking using MDGs. In AutomatedTechnology for Verification and Analysis (ATVA’04), Taipei, Taiwan,November 2004, Lecture Notes in ComputerScience 3299, Springer Verlag, pp.441-455.

[75]      D. Li*, M. HU, and O. AitMohamed. Built-In Self-Test Design of Motion Estimation Computing Array. Proc. IEEE Northeast Workshop on Circuitsand Systems (NEWCAS’04), Montreal, Quebec, Canada, June 2004, pp. 349-352.

[76]      M. Krykhtin*, Y. Mokhtari*, O.Ait Mohamed, and X. Song. Towards Software Model Checking using MDGs. Proc. IEEE Northeast Workshop on Circuitsand Systems (NEWCAS’04), Montreal, Quebec, June 2004, pp.345-348.

[77]      S. Jahanpoor* and O. AitMohamed. Automatic Generation of Model Checking Properties and Constraintsfrom Production Based Specification. Proc.IEEE Midwest Symposium on Circuits and Systems (MWSCAS’04), Hiroshima,Japan, July 2004, pp.435-438.

[78]      V.K. Pisini, S. Tahar, P.Curzon, O. Ait Mohamed, and X. Song. Formal Hardware Verification byIntegrating HOL and MDG. Proc. IEEE 10th Great Lakes Symposium onVLSI (GLS- VLSI'00), Chicago,Illinois, USA, March 2000. pp-23-28.

[79]      A.E.K Dekdouk,O. Ait Mohamed, S. Jahanpour*, and E. Cerny. What About FormalVerification of IP-based SoC Designs? InternationalWorkshop on IP Based Synthesis and System Design (IWLAS'98), Grenoble,France, December 98.

[80]      M. Azizi, O. Ait Mohamed,and X.  Song. Cache Coherence ProtocolVerification of Multiprocessor System with Shared Memory. Proc. InternationalConference on Microelectronics (ICM‚Äô98),Monastir, Tunisia, December 1998, pp. 99-102.

[81]      P. Curzon, S.Tahar, and O.  Ait Mohamed.Verification of the MDG Components Library in HOL. Proc. International Conference on Theorem Proving in Higher- OrderLogics (TPHOLs’98), Canberra, Australia, September 1998, pp. 31-45.

[82]      Y.Xu, E. Cerny, X. Song, F. Corella, O. Ait Mohamed. Model Checking for A first-Order Temporal Logic using MultiwayDecision Graphs. In Computer-AidedVerification (CAV’98), Vancouver, British Columbia, Canada, July 1998, Lecture Notes in Computer Science 1427,Springer Verlag, pp. 219-231.

[83]      O. Ait Mohamed, E. Cerny, X. Song. MDG-basedVerification by Retiming and Combinational Transformations. Proc. IEEE 8^th Great LakesSymposium on VLSI (GLS-VLSI’98), Lafayette, Louisiana, USA, February 1998, pp. 356 - 361.

[84]      O. Ait Mohamed. Mechanizing a pi-calculus equivalence in HOL. In International workshopon Higher Order Logic Theorem Proving and Its Applications(HOL’95), SalteLake City, Utah, USA, September 1995, LectureNotes in Computer Science 971, Springer Verlag, pp. 1- 16.

[85]      O. Ait Mohamed, A. Mokkedem. On FormalVerification of Occam Programs. Proc.of the International Conference On Parallel and Distributed Processing Techniqueand Applications (PDPTA’95), Georgia, USA, November 1995.