Master's Students
Master’s Students (MASc)
| Name |
Period |
Title of Thesis |
Present Position |
| Oumaima Barhoumi |
2020 – 2022 |
Formal Analysis of Traffic Conflicts Severity using KeYmaera | Ph.D. Student, Concordia University, Montreal, Canada |
| Alain Aoun |
2019 – 2021 |
On the Improving of Approximate Computing Quality Assurance | Ph.D. Student, Concordia University, Montreal, Canada |
| Sowmith Nethula |
2018 – 2019 |
Single Event Multiple Transient Analysis using Satisfiability Modulo Theories | Associate Digital Verification Engineer, Huawei, Ottawa, Canada |
| Muhammad Shirjeel Shehzad |
2015 – 2016 |
Statistical classification based est. of circuits failure probability | Embedded Software Developer, Aspin Kemp, PEI, Canada |
| Sidi Mohamed Beilahi |
2014 – 2016 |
Towards the design automation of of quantum circuits | Ph.D. Student, Université de Paris, France |
| Muhammad Qasim |
2014 – 2016 |
Formalization of Normal random variables | Staff ASIC Verification Engineer, AMD, Toronto, Canada |
| Mohamed Baba |
2013 – 2016 |
A low-cost camera-based transducer tracking System for freehand three-dimensional ultrasound imaging |
ASIC Verification Engineer, Microsemi, Montreal, Canada |
| Donia Chaouch |
2013 – 2015 |
Formalization of continuous-time Markov chains with applications | System Software Developer, Black-Berry/QNX, Ottawa, Canada |
| Mohammad Hossein Askari Hemmat |
2013 – 2015 |
Model to code generation of UML/SysML activity diagrams for ARM CortexM MCUs | ASIC Verification Engineer, Microsemi, Montreal, Canada |
| Ons Seddiki |
2012 – 2014 |
Linking HOL Light to Mathemat- ica using OpenMath | R.A., U. Bramberg, Germany |
| Paul Winkler |
2013 – 2014 |
Automatic gen. of reduced mod- els using SPICE simulation traces | R.A., U. Chemnitz, Germany |
| Najla Azizi |
2010 – 2012 |
Automatic verification and analy- sis of AMS designs using iSAT | Ph.D. Student, ETS, Montreal, Canada |
| Alaeddine Daghar |
2011 – 2012 |
Lyapunov approach for nonlinear aircrafts using sum of squares | Senior Production Analyst, DGCIB, Montreal, Canada |
| Ghassen Hlali |
2011 – 2012 |
Analysis of information flow using min and belief-min-entropy. | Senior Consultant Sys Integration, Deloitte, Montreal, Canada |
| Ons Lahiouel |
2011 – 2012 |
A synthesis tool for analog circuit analysis | Senior ASIC Verification Engineer, MDA, Montreal, Canada |
| Ibtissem Seghaier |
2011 – 2012 |
Statistical analysis of analog cir- cuit designs | Sr. AMS Verification Engineer, Renesas Electronics, Ottawa, Canada |
| Sara Mohammed Ahmed |
2011 – 2012 |
Hierarchical finite state machine watermarking | Lecturer, German University in Cairo, Egypt |
| Saleem Al- Akhras |
2006 – 2012 |
On the verification of a WiMax design using symbolic simulation | Service Engineer, Mobility, Riyadh, Saudi Arabia |
| Ghaith Bany Hamad |
2010 – 2011 |
Identification of Soft Error at Gate Level using Formal Model Checking | McGill University, Montreal, Canada |
| Yan Zhang |
2010 – 2011 |
Development of a matrix theory in HOL | Verification Engineer, China Techenergy, Beijing, China |
| Anis Souari |
2009 – 2010 |
FPGA implementation of fre- quency domain equalizer | R.A., ETS, Montreal, Canada |
| Zhiwei Wang |
2008 – 2009 |
Runtime verification of analog and mixed signal designs | Product Development Engineer., Microsemi, Montreal, Canada |
| William Denman |
2008 – 2009 |
Towards the automated modelling and formal verif. of AMS designs | Systems Developer, Obis, Vancouver, BC, Canada |
| Mohamed Ahmed Taha |
2008 – 2009 |
Formal verification of IEEE 8002.16 security sublayer |
Lecturer, German University of Cairo, Egypt |
| Suliman Al- Basheir |
2007 – 2008 |
Radio access protocols for mobile network traffic generation | Cloud Solutions Architect, Google, Seatle, USA |
| Essam Ahmed |
2007 – 2008 |
Enhancing coverage based verif. using probability distribution | Principal ASIC Design Engineer, Microchip, Pennsylvania, USA |
| Tareq Khan |
2006 – 2007 |
Automatic generation of transac- tors in SystemC | Assistant Prof., Miami U., Florida, USA |
| Amer Samara |
2005 – 2006 |
Automated coverage directed test gen. using cell-based genetic algo. | Design Engineer, FOTA Technologies, Toronto, Canada |
| Moinudeen Haja |
2004 – 2006 |
Design for verification of a PCI- X bus model | Manager/Sr. Staff Engineer, AMD, Toronto, Canada |
| Abu Nasser M. Abdullah. |
2004 – 2006 |
Formal analysis and verification of an OFDM modem design | Verification Systems Engineer, Cadence, Massachusetts, USA |
| Mohamed Layouni |
2002 – 2003 |
Formal verification of a group communications protocol | Cybersecurity Senior Researcher, GM, Michigan, USA |
| Tarek El- Mhamdi |
2001 – 2003 |
On the embedding of multiway decision graphs in HOL | Graphics Verification Engineer, Apple, Florida, USA |
| Faiez Charfi |
2001 – 2003 |
Interfacing CoD and UPPAAL for real-time system verification | Lecturer, University of the Center, Tunisia |
| Rabeb Mizouni |
2001 – 2002 |
Hybrid tool for HOL theorem proving and MDG model | Assistant Prof., Khalifa University, Abu Dhabi, UAE |
| Amjad Gawanmeh |
2000 – 2002 |
Interfacing abstract state machines with MDGs | Associate Prof., University of Dubai, UAE |
| Mohamed Zaki |
2000 – 2002 |
Syntactic model reduction for hardware verification | Assistant Prof., University of Central Florida, USA |
| Amr Talaat Abdel-Hamid |
1999 – 2001 |
Verification of IEEE-754 floating-point function in HOL | Associate Prof. , Germany University of Cairo, Egypt |
| Ali Habibi |
1999 – 2001 |
Verification of digital signal processor ADSP-2100 in HOL | Principle Engineer, Qualcomm, California, USA |
| Mohamed Hasan Zobair |
1999 – 2000 |
Verification of a telecom system block using MDGs | Principal Engineer, Qualcomm, SOC, California, USA |
| Leila Barakatain |
1999 – 2000 |
Practical approaches to model checking using FormalCheck | Embedded Software Engineer, Boeing, Seattle, USA |
| Tallal Osam Elshabrawy |
1998 – 2000 |
MAC architecture for broadband satellite access systems | Associate Prof. & Assoc. Dean, German U. of Cairo, Egypt |
| Vijay Kumar Pisini |
1996 – 2000 |
Integration of HOL and MDG for hardware verification | Software Engineer, Aerospace Industry, USA |
| Jianping Lu |
1997 – 1999 |
Formal verification of ATM switches | Senior Researcher, Alcatel, Ottawa, Canada |
| Subhashini Balakrishnan |
1996 – 1999 |
Modeling and verification of embedded systems using MDGs | Software Designer, Multimedia, Ericsson, Montreal, Canada |
| Mathias Dehof |
1993-1994 |
Formal verification of DLX processor using HOL |
Control Systems Engineer, KUKA, Augsburg, Germany |
| Ghassen Ben Amor |
1993 – 1994 |
Automatic the formal verification of pipelined processors in HOL | Senior Engineer, Debis, Stuttgart, Germany |
| Stefan Kühnel |
1991 – 1992 |
Using expert systems for communications protocol design | Industrial sector, Germany. |
| Aroua Ben Mohamed |
2009 – 2010 |
Synthesis tool for formal verification of SPICE models | IT Manager Tennis Canada, Montreal, Canada |
| Hani Al Talibani |
2006 – 2007 |
Symbolic simulation of SystemC designs | Private sector, Montreal, Canada |
| Ishtiaque Khan |
2002 – 2005 |
Translation of Sugar language to SystemC | Technical Leader, CAE, Montreal, Canada |
| Mohamed Hasanuzzaman |
2001 – 2002 |
Translating Verilog HDL to HOL- MDG | Ph.D. Student, Polytechnique Montreal, Canada |
| Mounadher Kharroubi |
1999 – 2000 |
Semi-formal verification of hardware/software systems | Verification Engineer, AMD, California, USA |
| Hung Tien Bui |
1999 – 2000 |
Formal verification of floating- point arithmetic hardware | Associate Prof. U. Quebec at Chicoutimi, Canada |
Master’s (M.Eng) Students (Graduate Projects)
| Name |
Years |
Title of Project |
Present Position |
Zubin Ghandi |
2013 – 2014 |
Generating Analog Circuits FSMs using Learning and Clustering Methods |
Firmware Engineer, SoundofMotion Technologies Inc., Vancouver, Canada |
| Aroua Ben Mohamed |
2010 – 2011 |
Synthesis Tool for Formal Verification of SPICE Models |
IT Manager Tennis Canada, Montreal, Canada |
| Jigar Patel |
2009 – 2010 |
Formal Reliability Analysis of Digital Circuits |
ASIC/FPGA verification Engineer, Ciena, Ottawa, Canada |
| Zhiwei Wang |
2007 – 2008 |
VHDL-AMS Modeling of a PLL Design |
Verification Engineer, PMC Sierra, Montreal, Canada |
| Zhi Jie Dong |
2007 – 2008 |
Design and Simulation of Non-linear AMS Circuits |
FPGA Design Engineer, Neptec, Ottawa, Canada |
| Bahador Sohrabi |
2006 – 2007 |
RTL Design of a MIPS R3000 Processor Model |
Hardware Architect Manager, SICPA, Vancouver, Canada |
| Zhi Jie Dong |
2006 – 2007 |
Modeling ad Simulation of Analog and Mixed Signal Designs |
FPGA Design Engineer, Neptec, Ottawa, Canada |
| Yon Jun Shin |
2006 – 2007 |
SystemC Transaction Level Modeling of the MIPS R3000 Processor |
Verification Engineer, Samsung, South Korea |
| Mohamed Al Homrane |
2003 – 2004 |
Cone of Influence Algorithm for NuMDG |
Engineer, ICT, Abu Dhabi, UAE |
| Md Hasan Zobair |
1999 – 2000 |
Design and Verification of an ATM Switch Fabric in MDG |
Principal Engineer, Qualcomm, SOC, California, USA |
| Leila Barakatain |
1999 – 2000 |
Formal Verification of an ATM Switch Fabric in FormalCheck |
Embedded Software Engineer, Boeing, Seattle, USA |
| Murugesh Palanisamy |
1998 – 1999 |
Verification of RCMP-Egress Routing Logic |
Verification Engineer, Nortel, Ottawa, Canada |
