| 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 transducertracking System for freehandthree-dimensionalultrasound 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 IEEE8002.16 security sublayer |
Lecturer, German University ofCairo, 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 theCenter, 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 DLXprocessor 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, PolytechniqueMontreal, 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 atChicoutimi, Canada |