Master's Students


Master’s Students (MASc)



Title of Thesis

Present Position
Mohamed Baba

2013 - 2016

A low-cost camera-based transducer
tracking System for freehand
ultrasound imaging
ASIC Verification Engineer,
Microsemi, Montreal, Canada
Muhammad Qasim

2013 - 2015

Formalization of Normal Random Variables ASIC/Layout Design Engineer, AMD Toronto, Canada
Donia Chaouch

2013 - 2015

Formalization of continuous-time Markov chains with applications Technical Support Engineer, Genetec, Montreal, 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 RA, U. Bramberg, Germany
Paul Winkler

2013 - 2014

Automatic gen. of reduced mod- els using SPICE simulation traces RA, U. Chemnitz, Germany
Najla Azizi

2010 - 2012

Automatic verification and analy- sis of AMS designs using iSAT Ph.D. Student, ETS, Montreal, Canada


2011 - 2012

Lyapunov approach for nonlinear aircrafts using sum of squares PhD Student, Concordia U., Montreal, Canada
Ghassen Hlali

2011 - 2012

Analysis of information flow using min and belief-min-entropy. PhD Student, Concordia U., Montreal, Canada
Ons Lahiouel

2011 - 2012

A synthesis tool for analog circuit analysis PhD Student, Concordia U., Montreal, Canada


2011 - 2012

Statistical analysis of analog cir- cuit designs PhD Student, Concordia U., Montreal, Canada
Sara Mohammed


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, Ericsson, 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 Ph.D. Student, ETS, Montreal, Canada
Zhiwei Wang

2008 - 2009

Runtime verification of analog and mixed signal designs Verification Engineer., PMC- Sierra, Montreal, Canada


2008 - 2009

Towards the automated modelling and formal verif. of AMS designs Systems Developer, Obis,
Vancouver, BC, Canada

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 IP Systems Integrator, Ericsson, Montreal, Canada
Essam Ahmed

2007 - 2008

Enhancing coverage based verif. using probability distribution Verification Engineer, PMC- Sierra, Oregon, 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


2004 - 2006

Design for verification of a PCI- X bus model ASIC Verification 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


2002 - 2003

Formal verification of a group communications protocol Freelance Consultant, Financial
sector, Montreal, Canada
Tarek El- Mhamdi

2001 - 2003

On the embedding of multiway decision graphs in HOL Graphics Verification Engineer,
Apple, 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


2000 - 2002

Interfacing abstract state machines with MDGs Assistant Prof.,
Khalifa University, Sharjah, UAE
Mohamed Zaki

2000 - 2002

Syntactic model reduction for hardware verification Consultant, Innovia Technologies, Vancouver, Canada
Amr Talaat


1999 - 2001

Verification of IEEE-754 floating-point function in HOL Assistant Prof.
, Germany

University of Cairo, Egypt

Ali Habibi

1999 - 2001

Verification of digital signal processor ADSP-2100 in HOL Chief Engineer, SiFive Inc.,
California, USA

Hasan Zobair

1999 - 2000

Verification of a telecom system block using MDGs Principal Engineer, Qualcomm, SOC, California, USA


1999 - 2000

Practical approaches to model checking using FormalCheck Embedded Software Engineer, Boeing, Seattle, USA
Tallal Osam


1998 - 2000

MAC architecture for broadband satellite access systems Associate Prof.,
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


Senior Researcher, Alcatel, Ottawa, Canada


1996 - 1999

Modeling and verification of embedded systems using MDGs Software Designer, Multimedia, Ericsson, Montreal, Canada
Mathias Dehof


Formal verification of DLX

processor using HOL

Control Systems Engineer, KUKA, Augsburg, Germany
Ghassen Ben


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


2009 - 2010

Synthesis tool for formal verification of SPICE models IT Manager Tennis Canada, Montreal, Canada
Hani Al


2006 - 2007

Symbolic simulation of SystemC


Private sector, Montreal, Canada
Ishtiaque Khan

2002 - 2005

Translation of Sugar language to


Technical Leader, CAE, Montreal, Canada


2001 - 2002

Translating Verilog HDL to HOL- MDG PhD Student, Polytechnique
Montreal, Canada


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 Assistant Prof.
U. Quebec at
Chicoutimi, Canada

Master’s (M.Eng) Students (Graduate Projects)



Title of Project

Present Position



2013 - 2014

Generating Analog Circuits

FSMs using Learning and

Clustering Methods

Firmware Engineer,

SoundofMotion Technologies

Inc., Vancouver, Canada

Aroua Ben


2010 - 2011

Synthesis Tool for Formal

Verification of SPICE Models

IT Manager Tennis Canada, Montreal,


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



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


FPGA Design Engineer, Neptec,

Ottawa, Canada

Yon Jun Shin

2006 - 2007

SystemC Transaction Level

Modeling of the MIPS R3000


Verification Engineer, Samsung,

South Korea

Mohamed Al


2003 - 2004

Cone of Influence Algorithm

for NuMDG

Engineer, ICT, Abu Dhabi, UAE
Md Hasan


1999 - 2000

Design and Verification of an

ATM Switch Fabric in MDG

Principal Engineer, Qualcomm, SOC, California, USA


1999 - 2000

Formal Verification of an

ATM Switch Fabric in


Embedded Software Engineer, Boeing, Seattle, USA


1998 - 1999

Verification of RCMP-Egress

Routing Logic

Verification Engineer, Nortel,

Ottawa, Canada


Concordia University