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 Reduction of Analog Circuits |
University of Leipzig, Germany |
| Khaleeque Ansari | May-July 2012 | Formalization of radom varibles for extended reals in 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 model checking algorithm |
TU Munich, Germany |
| Mukesh Kumar Agrawal | Mai – August 2011 | Porting of measure and probability theories from HOL4 to HOL4v7is |
IIT Delhi, India |
| Anis Souari | February-July 2011 | Formal verification of a frequency domain equalizer |
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 circuits uinsg patter matching |
Ecole Polytechnique de Tunisie, Tunisia |
| Ibtissem Seghaier | February-June 2011 | Statistical runtime verification of analog circuit designs |
Ecole Nationale d.Ingenieurs de Tunis, Tunisia |
| Ghassen Helali | February-August 2011 | Formalization of probaility theory in HOL4 theorem prover |
Ecole Nationale de Science Informatique, Tunisia |
| Ons Lahiouel | February-June 2011 | A synthesis tool for analog circuit modeling based on 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 frequency synthesizer |
Ecole Nationale d.Ingenieur de Tunis, Tunisia |
| Huei-Dian (Johnny) Shih | February-April 2010 | Dynamic web structure design for hardware verification group |
University of Waterloo, Canada |
| Johnatan Bouchaert | June-September. 2006 | Multiprocessor systems-on-chip (MPSoC) design in 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 description languages |
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 for verification of a PCI bus in SystemC |
Ecole Polytechnique de Marseille, France |
| Imad Benalam | 2002 | Formal verification of hardware description languages |
ENSTA, Paris, France |
| Johnatan Bouchaert | 2006 | Multiprocessor systems-on-chip (MPSoC) design in SystemC |
ISEN, Brest, France |
| Huei-Dian (Johnny) Shih | 2010 | Multiprocessor systems-on-chip (MPSoC) Dynamic web structure design for hardware verification group |
University of Waterloo, Canada |
Concordia Internship Students
| Name | Years | 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 |
