Internship Students


International Internship Students

Name Period Title of Project Home Institution
Abdelrahman Elshafei June-August 2016 Formal verification of Rambus oscillator in presence of jitter Concordia University, Canada
Sidi Mohamed Beillahi March-July 2014 Formalization of signal-flow graphs in HOL Ecole Polytechnique de Tunisie, Tunisia
Mbarka Soualhia September 2012-April 2013 Formalization of queuing theory in HOL ETS, Montreal, Canada
Paul Winkler October 2012-March 2013 Testbench for Model Order Reductionof Analog Circuits University of Leipzig, Germany
Khaleeque Ansari May-July 2012 Formalization of radom varibles for extended realsin HOL IIT Delhi, India
Harsh Singhal May-July 2012 Formlization of complex vectors in HOL IIT Delhi, India
Johannes Hoelzl September-October 2011 Formal verification of probabilistic modelchecking algorithm TU Munich, Germany
Mukesh Kumar Agrawal Mai – August 2011 Porting of measure and probability theories fromHOL4 to HOL4v7is IIT Delhi, India
Anis Souari February-July 2011 Formal verification of a frequency domainequalizer Ecole Nationale d.Ingenieur de Sousse, Tunisia
Najla Azizi February-July 2011 Verification of AMS designs using iSAT Ecole Nationale d.Ingenieur de Tunis, Tunisia
Alaeddine Daghar February-June 2011 Formal noise and jitter analysis in analog circuitsuinsg patter matching Ecole Polytechnique de Tunisie, Tunisia
Ibtissem Seghaier February-June 2011 Statistical runtime verification of analog circuitdesigns Ecole Nationale d.Ingenieurs de Tunis, Tunisia
Ghassen Helali February-August 2011 Formalization of probaility theory in HOL4theorem prover Ecole Nationale de Science Informatique, Tunisia
Ons Lahiouel February-June 2011 A synthesis tool for analog circuit modeling basedon nodal analysis Ecole Nationale d.Ingenieurs de Tunis, Tunisia, Tunisia
Yan Zhangl January-April 2011 Formalization of matrix theory in HOL4 Capital Normal Universwity, Beijing, China
Anis Souari May-August 2010 FPGA design of frequency domain equalizer Ecole Nationale d.Ingenieur de Sousse, Tunisia
Najla Azizi February-July 2010 Runtime verification of a PLL frequencysynthesizer Ecole Nationale d.Ingenieur de Tunis, Tunisia
Huei-Dian (Johnny) Shih February-April 2010 Dynamic web structure design for hardwareverification group University of Waterloo, Canada
Johnatan Bouchaert June-September. 2006 Multiprocessor systems-on-chip (MPSoC) designin SystemC ISEN, Brest, France
Karim Oumalou February-August 2004 Design for verification of a PCI bus in SystemC Ecole Polytechnique de Marseille, France
Imad Benlalam February-July 2002 Formal verification of hardware descriptionlanguages ENSTA, Paris, France
Chadi El Chantiri 2004 Autoamtic generation of Model Checking properties and constraints from Production Based Specification Concordia univeristy
Kenneth Stevens 2004 Verification of the advanced Encryption Standard (AES) implementation Concordia univeristy
Karim Oumalou 2004 Design for verification of a PCI bus in SystemC Ecole Polytechnique de Marseille
Imad Benlalam 2002 ENSTA Paris France
Karim Oumalou 2004 Design forverification of a PCI bus in SystemC Ecole Polytechnique de Marseille, France
Imad Benalam 2002 Formal verification of hardwaredescription languages ENSTA, Paris, France
Johnatan Bouchaert 2006 Multiprocessorsystems-on-chip (MPSoC) design in SystemC ISEN, Brest, France
Huei-Dian (Johnny) Shih 2010 Multiprocessorsystems-on-chip (MPSoC) Dynamic webstructure design for hardware verification group University of Waterloo, Canada

Concordia Internship Students

Name Year Title of Project
Derek Chung 2005-2006 Generating Finite State Machines from SystemC Design
Hung Yu-Mei 2004-2005 Development of a FSM to Verilog Translator
Meral Shirazipour 2001-2002 Hardware Verification using ASM-SMV
Mohamed Khan 1999-2000 Design and Verif. of Benchmark Circuits with FormalCheck
Ali Abbas Mir 1999-2000 Modeling and Verification of an Embedded Systems in SMV
Bashar Khalaf 1998-1999 Verilog Modeling and Synthesis of an Exponent FPU
Tien H. Bui 1998-1999 VHDL Design and Synthesis of an Exponent FPU
Amir K. Daneshbeh 1997-1998 VHDL Modeling of DLX RISC Processor