Text Box: PUBLICATIONS

Journal Papers

Conference Papers

Books

Technical Reports

Thesis

Text Box: Journal Papers
Text Box: Conference Papers
Text Box: PHD Thesis
Text Box: Technical Reports
Text Box: Master Thesis
Google Scholar

Home

Contact Us

People

Alumni

Laboratories

Sponsors / Partners

Research

Publications

Events

Photo Gallery

Related Links

Conference CFPs

HVG Local

Text Box: Books

1. Saed Abed: The Verification of MDG Algorithms in the HOL Theorem Prover. LAP Lambert Academic Publishing , 2009. ISBN: 978-3838317380 [160 pages].

2. O.Hasan and S. Tahar. : Probabilistic Analysis using Theorem Proving - A Higher-Order-Logic Based Approach. VDM Verlag Dr. Mueller e.K.,  November, 2008. ISBN: 978-3639094725 [164 pages] .

3. Otmane Ait Mohamed, César A. Mu˜noz, and S.Tahar (Eds.): Theorem Proving in Higher Order Logics; Vol.5170 of Lecture Notes in Computer Science, Springer-Verlag, 2008. (ISBN: 3-540-71065-5) [321 pages].

4. Victor A. Carre˜no, César A. Mu˜noz, and S. Tahar (Eds.): Theorem Proving in Higher Order Logics; Vol.2410 of Lecture Notes in Computer Science, Springer-Verlag, 2002. (ISBN: 3-540-44039-9) [349 pages].

5. E. Cerny, F. Corella, M. Langevin, X. Song, S. Tahar, Z. Zhou: Automated Verification with Abstract State Machines Using Multiway Decision Graphs; In: Kropf, T. (Ed.), Formal Hardware Verification: Methods and Systems in Comparison, Lecture Notes in Computer Science 1287, State-of-the-Art Survey, Springer Verlag, 1997, pp. 79-113.

1. Zhiwei Wang, "Runtime Verification of Analog and Mixed Signal Designs".M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, June 2009.

2. William Denman, "Towards the Automated Modelling and Formal Verification of Analog Designs".M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, April 2009.

3. Suliman Al-Basheir "Modeling of Radio Access Application Protocols for Mobile Network Trafic Generation". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, December 2008.

4. EssamArshed Ahmed, "Enhancing Coverage Based Verification using Probability Distribution". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, September 2008.

5. Tareq Hasan Khan, "Automatic Generation of Transactors in SystemC". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, September 2007.

6. Amer Samarah, "Automated Coverage Directed Test Generation Using a Cell-Based Genetic Algorithm". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, September 2006.

7. Donglin Li , "Towards First-Order Symbolic Trajectory Evaluation using MDGs". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, March 2006.

8. Haja Moinudeen, "Design for Verification of a PCI-X Bus Model". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, February 2006.

9. Abu Nasser Mohammed Abdullah,  "Formal Analysis and Verification of an OFDM Modem Design". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, February 2006.

10. Asif Iqbal Ahmed,  "Assertion-Based Verification of the Look-Aside Interface". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, April 2005. 

11. Fariborz Fereydouni–forouzand , "FPGA Implementation of Congestion Control Routers in High Speed Networks ". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, April 2005.  

12. Jagmit Singh, "Custom and Model Based Detection of Deficiencies Related to Java Multithreading". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, July 2004.

13. Tarek El-Mhamdi, "On the Embedding of Multiway Decision Graphs in HOL". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, August 2003.

14. Mohamed Layouni, "On the Formal Verification of an Intrusion-Tolerant Group Communications Protocol". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, August 2003.

15. Mohamed Zaki, "Syntactic Model Reduction for Hardware Verification". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada,  April 2003.

16. Amjad Gawanmeh, "Interfacing Abstract State Machines with Miltiway Decision Graphs". MaSc Thesis, Concordia University, Department of Electrical and Computer Engineering, April 2003.

17. Rabeb Mizouni, "A Hybrid Tool for Linking HOL Theorem Proving with MDG Model Checking".  M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, Spring 2003. 

18. Amr Talaat Abdel-Hamid, "A Hierarchical Verification of the IEEE-754 Table-Driven Floating-Point Exponential Function using HOL". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, June 2001.

19. Ali Hbibi, "Formal Verification of the Digital Signal Processor Family ADSP-2100 of Analog Devices", DEA (M.A.Sc) Thesis, Ecole National d'Ingenieurs de Tunis, Mai 2001.

20. Mohamed Hasan Zobair, "Modeling and Formal Verification of a Telecom System Block using MDGs". M.A.Sc Thesis, Concordia University, Department of Electrical and Computer Engineering, December 2000.

21. Leila Barakatain, "Practical Approaches to Model Checking using FormalCheck". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, April 2000.

22. Tallal Osam Elshabrawy, "MAC Architecture for Broadband Satellite Access Systems". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, April 2000.

23. Vijay Kumar Pisini, "Integration of HOL and MDG for Hardware Verification". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, February 2000.

24. Subhashini Balakrishnan, "Modeling and Verification of Embedded Systems using MDGs". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada,  November 1999.

25. Jianping Lu, "On the Formal Verification of ATM Switches". M.A.Sc. Thesis, Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, May 1999.

1.  Amjad Gawanmeh, “On the Formal Verification of Group Key security Protocols”, Ph.D. Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, September 2008.

2.  Mohamed Hamed Zaki Hussein, “ Techniques for the Formal Verification of Analog and Mixed- Signal Designs”,  Ph.D. Department of Electrical and Computer Engineering, Concordia University, September 2008.

3. Osman Hsasan,  “Formal Probabilistic Analysis using Theorem Proving”,  Ph.D. Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada,  April 2008.

4. Amr Talaat Abdel-Hamid, “Watermarking techniques for Intellectual Property Protection in SOC Design”,  Ph.D. Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, in cosupervision with Dr. E.M. Aboulhamid (University of Montreal), April 2006.

5. Ali Habibi, “A Framework for System Level Verification, «The SystemC Case”,  Ph.D. Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, November 2005.

6. Fang Wang, “First Order Model Checking of w-Automata using Multiway Decision Graphs”,  Ph.D. Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, April 2005.

7. Behzad Akbarpour, “Modeling and Verification of DSP Designs in HOL”, Ph.D. Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, April 2005.

8. Hong Peng, “ Improving Compositional Verification Environment Synthesis and Syntactic Model Reduction”, Ph.D. Department of Electrical and Computer Engineering, Concordia University, Montreal, Quebec, Canada, Fall 2002.

9. Haiyan Xiong, “Providing a Formal Linkage Between MDG and HOL Based on a Verified MDG System”, Ph.D. Computer Science, in cosupervision with Dr. P. Curzon (Middlesex University, UK), January 2002.

10. Mustafa Azizi, “Coverification of Hardware/Software Systems (Covérification des Systèmes Intégrés)”, Ph.D. Computer Science, University of Montreal, in cosupervision with Dr. E.M. Aboulhamid (University of Montreal), July 2001.

11. Tallal Osam Elshabrawy, “MAC Architecture for Broadband Satellite Access Systems”, in cosupervision with Dr. T. LeNgoc, April 2000.

Hardware Verification Group

Concordia University

1. R. Narayanan, M. Zaki, and S. Tahar: Using Stochastic Differential Equation for Verification of Noise in Analog/RF Circuits; Journal of Electronic Testing, doi:10.1007/s10836-009-5137-z, 7 January 2010, Springer Verlag, pp. 1-13.

2. O. Hasan, S. Tahar, N. Abassi: “Formal Reliability Analysis using Theorem Proving”, IEEE Transactions on Computers, doi:10.1109/TC.2009.165, 23 Oct. 2009, pp. 1-14.

3. N. Abdullah, B. Akbarpour, and S. Tahar: Error Analysis and Verification of an IEEE 802.11 OFDM Modem using Theorem Proving; Electronic Notes in Theoretical Computer Science, Vol. 242, No. 2, Elsevier B.V. Pub., July 2009, pp. 3-30.

4. O. Hasan and S. Tahar: Probabilistic Analysis of Wireless Systems using Theorem Proving; Electronic Notes in Theoretical Computer Science, Vol. 242, No. 2, Elsevier B.V. Pub., July 2009, pp. 43-58.

5. M.H. Zaki, W. Denman and S. Tahar: Integrating Abstraction Techniques for Formal Verification of Analog Designs; Journal of Aerospace Computing, Information, and Communication, Vol. 6, May 2009, pp. 373-392.

6. B. Akbarpour, A.T. Abdel-Hamid, S. Tahar, and J. Harrison: Verifying a Synthesized implementation of IEEE-754 Floating-Point Exponential Functionn using HOL; The Computer Journal, DOI:10.1093/comjnl/bxp023, 10 April 2009, pp. 1-24.

7. O. Hasan and S. Tahar: Formal Verification of Tail Distribution Bounds in the HOL Theorem Prover; Mathematical Methods in The Applied Sciences, Vol. 32, No. 4, Wiley Interscience, March 2009, pp. 480-504.

8. A. Gawanmeh, A. Bouhoula, and S. Tahar: Rank Functions based Inference System for Group Key Management Protocols Verification; International Journal of Network Security, Vol. 8, No. 2, Science Publications, March 2009, pp. 207-218.

9. O. Hasan and S. Tahar: Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL; Journal of Automated Reasoning, Vol. 42, No. 1, Springer Verlag, January 2009, pp. 1-33.

10. M. Zaki, S. Tahar and G. Bois: Formal Verification of Analog and Mixed Signal Designs: A Survey; Microelectronics Journal, Vol. 39, No. 12, Elsevier B.V. Pub., December 2008, pp. 1395-1404.

11. O.Hasan and S. Tahar: Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables. Journal of Automated Reasoning, Vol. 41, No. 3-4, Springer Verlag, November 2008, pp. 295-323.

12. A. Cui, C.-H. Chang and S. Tahar: IP Watermarking using Incremental Technology Mapping at Logic Synthesis Level; IEEE Transactions on CAD of Integrated Circuits and Systems, Vol.27, No. 9, September 2008, pp 1565-1570.

13. A.Gawanmeh, S. Tahar, H. Moinudeen, and A. Habibi: A Design for Verification Approach using an Embedding of PSL in AsmL; Journal of Circuits, Systems, and Computers, Vol. 16, No. 6, World Scientific Publishing, 2008, pp. 859.881.

14. M. Zaki, S. Tahar, and G. Bois: Qualitative Abstraction based Verification for Analog Circuits; Revue des Nouvelles Technologies de l'information, Vol. 4, Issue 7, December 2007, RNTI-SM-1, Edition Cepadues, pp. 147-158

15. A. Gawanmeh, S. Tahar, and K. Winter: Formal Verification of ASMs using MDGs; Journal of  Systems Architecture, Vol. 54, No. 1-2, Elsevier B.V. Pub., January-February, 2008, pp. 15-34.

16. B. Akbarpour and S. Tahar: Error Analysis of Digital Filters using HOL Theorem Proving; Journal of Applied Logic, Vol. 5, No. 4, Elsevier B.V. Pub., December 2007, pp. 651-666.

17. O. Hasan and S. Tahar Formalization of the Standard Uniform Random Variable; Theoretical Computer Science, Vol. 382, No. 1, Elsevier B.V. Pub., 2007, pp. 71-83.

18. H. Xiong, P. Curzon, S. Tahar, and A. Blandford: Providing a Formal Linkage between MDG and HOL; Formal Methods in Systems Design, Vol. 30, No. 2, Springer Verlag, April 2007, pp. 83-116.

19. M. Layouni, J. Hooman, and S. Tahar: Formal Specification and Verification of the Intrusion-Tolerant Enclaves Protocol; International Journal of Network Security, Vol. 5, No. 3, Science Publications, 2007, pp. 288-298.

20. R. Mizouni, S. Tahar and P. Curzon: Hybrid Verification Incorporating HOL Theorem Proving and MDG Model Checking; Microelectronics Journal, Vol. 37, No. 11, November 2006, Elsevier B.V. Pub., pp. 1200-1207.

21. B. Akbarpour and S. Tahar: An Approach for the Formal Verification of DSP Designs using Theorem Proving; IEEE Transactions on CAD of Integrated Circuits and Systems, Vol. 25, No. 8, August 2006, pp. 1141-1457.

22. A. Habibi and S. Tahar: Design and Verification of SystemC Transaction Level Models; IEEE Transactions on Very Large Scale Integration Systems, Vol. 14, No. 1, January 2006, pp. 57-68.

23. B. Akbarpour, S. Tahar, and A. Dekdouk: Formalization of Fixed-Point Arithmetic in HOL; Formal Methods in Systems Design, Vol. 27, No. 1-2, September 2005, Springer Verlag , pp. 173-200.

24. A.T. Abdel-Hamid, S. Tahar, E.M. Aboulhamid: A Survey on IP Watermarking Techniques; Design Automation for Embedded Systems, Vol. 9, No. 3, July 2005, Springer Verlag, pp. 211-227.

25. A. Habibi and S. Tahar: On the Transformation of SystemC to AsmL using Abstract Interpretation; Electronic Notes in Theoretical Computer Science, Vol. 131, May 2005, pp. 39-49, Elsevier B.V. Pub.

26. Ying Xu, Xiaoyu Song, Eduard Cerny, Otmane Aït Mohamed: Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs (MDGs); Computer Journal, Vol 47, No 1, 2004, pp. 71-84.

27. O. Ait-Mohamed, X. Song, E. Cerny and S. Tahar: MDG Based State Enumeration by retiming and Circuit transformation; Journal of Circuits, Systems and Computers, Vol. 13, No. 5, October 2004, pp. 1111-1132, World Scientific Publishing.

28. S. Tahar, M.H. Zobair, and X. Song: On the Formal Verification of a SONET Data Stream Processor; IEE Proceedings - Computers and Digital Techniques, Vol. 151, No. 1, January 2004, pp. 71-81.

29. Otmane Aït Mohamed, Xiaoyu Song, Eduard Cerny: On the non-termination of MDG-based abstract state enumeration; Theoretical Computer Science, 1-3(300): 161-179 (2003)

30. S. Kort, S. Tahar, and P. Curzon: Hierarchical Formal Verification Using a Hybrid Tool; International Journal on Software Tools for Technology Transfer, Vol. 4, Springer Verlag, 2002, pp. 1-10.

31. H. Peng, S. Tahar and F. Khendek: Comparison of SPIN and VIS for Protocol Verification; International Journal on Software Tools for Technology Transfer, Vol. 4, No. 2, pp. 234-245, February 2003, Springer Verlag.

32. J.F. Weng, T. Le-Ngoc, G.Q. Xue, and S. Tahar: Performance of Multistage Interference Cancellation Schemes for Asynchronous QPSK/DS/CDMA over Multipath Rayleigh Fading Channels; IEEE Transactions on Communications, Vol. 49, No. 5, May 2001, pp. 774-778.

33. J.F. Weng, T. Le-Ngoc, G.Q. Xue, and S. Tahar: Multilevel Quantized Soft-Limiting Detector for an FH-SSMA System; Journal of Communications and Networks, Vol. 2, No. 4, December 2000, pp. 379-388.

34. G.Q. Xue, J.F. Weng, T. Le-Ngoc, and S. Tahar: An Analytical Model for Performance Evaluation of Parallel Interference Cancellers in CDMA Systems; IEEE Communications Letters, Vol. 4, No. 6, June 2000, pp. 184-186.

35. J.F. Weng, G.Q. Xue, T. Le-Ngoc, and S. Tahar: Multistage Interference Cancellation with Diversity Reception for Asynchronous QPSK DS/CDMA Systems over Multipath Fading Channels; IEEE Journal on Selected Areas in Communications, Vol. 17, No. 12, December 1999, pp. 2162-2180.

36. S. Tahar and P. Curzon: Comparing HOL and MDG: A Case Study on the Verification of an ATM Switch Fabric; Nordic Journal of Computing, Vol. 6, 1999, Publishing Association Nordic Journal of Computing, pp. 372-402

37. G.Q. Xue, J.F. Weng, T. Le-Ngoc, and S. Tahar: Adaptive Multistage Parallel Interference Cancellation for CDMA; IEEE Journal on Selected Areas in Communications, Vol. 17, No. 10, October 1999, pp. 1815-1827.

38. S. Tahar, X. Song, E. Cerny, Z. Zhou, M. Langevin and O. Ait-Mohamed: Modeling and Verification of the Fairisle ATM Switch Fabric using MDGs; IEEE Transactions on CAD of Integrated Circuits and Systems, Vol. 18, No. 7, July 1999, pp. 956-972.

39. S. Tahar and R. Kumar: A Practical Methodology for the Formal Verification of RISC Processors; Formal Methods in Systems Design, Vol.13, No. 2, September 1998, Kluwer Academic Publishers, pp. 159-225. 

40. S. Tahar and R. Kumar: Formal Specification and Verification Techniques for RISC-Pipeline Conflicts; The Computer Journal, Vol. 38, No. 2, July 1995, Oxford University Press, pp. 111-120.

1. Z. Wang, M. Zaki, S. Tahar: Statistical Runtime Verification of Analog and Mixed Designs; Proc. IEEE International Conference on Signals, Circuits and Systems (SCS.09), Djerba, Tunisia, November 2009, pp. 1-6.

2. W. Denman, B. Akbarpour, S. Tahar, M. Zaki, L. Paulson:   Formal Verification of Analog Designs using MetiTarski ; Proc. IEEE International Conference on Formal Methods in CAD (FMCAD'09), Austin, Texas, USA, November 2009, pp. 93-100, IEEE Computer Society Press.

3. O. Hasan, N. Abbasi, B. Akbarpour, S. Tahar, and R. Akbarpour: Formal Reasoning about Expectation Properties for Continuous Random Variables; In: A. Cavalcanti and D. Dams (Eds.), Formal Methods, Lecture Notes in Computer Science 5850, Springer Verlag, 2009, pp. 435-450. [Proc. International Symposium on Formal Methods (FM'09) , Eindhoven, The Netherlands, November 2009.]

4. O. Hasan, S.K. Afshar, and S. Tahar: Formal Analysis of Optical Waveguides in HOL; In: S. Berghofer et al.  (Eds.), Theorem Proving in Higher-Order Logics, Lecture Notes in Computer Science 5674, Springer Verlag, 2009, pp. 228-243. [Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'09), Munich, Germany, August 2009.]

5. S. Albasheir, S. Tahar, C. Gauthier, and J. Personna: Radio Access Network Traffic Generation for Mobile Switching Center; Proc. IEEE Symposium on Computers and Communications (ISCC'09), Sousse, Tunisia, July 2009, pp. 705-710.

6. Z. Wang, N. Abbasi, R. Narayanan, G. Al Sammane, M. Zaki, and S. Tahar : Verification of Analog and Mixed Signal Designs using Online Monitoring; Proc. IEEE International Mixed-Signals, Sensors, and Systems Test Workshop (IMS3TW'09), Scottsdale, Arizona, USA, June 2009, pp. 1-8.

7. A.M. Taha, A.T. Abdel-Hamid, and S. Tahar: Formal Verification of IEEE 802.16 Security Sublayer Using Scyther Tool; Proc. IFIP International Conference on Network and Service Security (N2S'09), Paris, France, June 2009, pp. 1-6.

8. R. Narayanan, M. Zaki, and S. Tahar: Using Stochastic Differential Equation for Assertion Based Verification of Noise in Analog/RF Circuits; Proc. IEEE International Mixed-Signals, Sensors, and Systems Test Workshop (IMS3TW'09), Scottsdale, Arizona, USA, June 2009, pp. 1-8.

9. A.M. Taha, A.T. Abdel-Hamid, and S. Tahar: Formal Analysis of the Handover Schemes in Mobile WiMAX Networks; Proc. IEEE International Conference on Wireless and Optical Communications Networks (WCON'09), Cairo, Egypt, April 2009, pp. 1-5.

10. N. Abbasi, O. Hasan and S. Tahar: Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays; In: M. Leuschel and H. Wehrheim (Eds.), Integrated Formal Methods, Lecture Notes in Computer Science 5423, Springer Verlag, 2009, pp. 277-291. [Proc. International Conference on Integrated Formal Methods (IFM'09), Düsseldorf, Germany, February 2009.]

11. R. Narayanan, N. Abbasi, M. Zaki, G. Al Sammane, and S. Tahar: On the Simulation Performance of Contemporary AMS Hardware Description Languages;  Proc. IEEE International Conference on Microelectronics (ICM'08), Sharjah, UAE, December 2008, pp. 390-393.

12. A. Gawanmeh, L. Jemni and S. Tahar: Event-B based Invariant Checking of Secrecy in Group Key Protocols; Proc. IEEE LCN Workshop on Network Security (WNS'08), Montreal, Quebec, Canada, October 2008, IEEE Computer Society Press.

13. Y. Mokhtari, S. Abed, O. Ait Mohamed, S. Tahar, and X. Song: A New Approach for the Construction of Multiway Decision Graphs; In: J.S. Fitzgerald, A.E. Haxthausen, and H. Yenigun (Eds.), Theoretical Aspects of Computing, Lecture Notes in Computer Science 5160, Springer Verlag 2008, pp. 228-242. [Proc. International Colloquium on Theoretical Aspects of Computing (ICTAC'08), Istanbul, Turkey, September 2008.]

14. O. Hasan and S. Tahar: Probabilistic Analysis of Wireless Systems using Theorem Proving; Proc. Formal Methods in Wireles Systems (FMWS'08), Toronto, Ontario, Canada, August 2008, pp. 3-18.

15.  A. Nasser, B. Akbarpour and S. Tahar: Error Analysis and Verification of an IEEE 802.11 OFDM Modem using Theorem Proving;  Proc. Formal Methods in Wireles Systems (FMWS'08), Toronto, Ontario, Canada, August 2008, 43-63.

16. A.T. Abdel-Hamid and S. Tahar: Fragile IP Watermarking Techniques; Proc. NASA/ESA Conference on Adaptive Hardware and Systems (AHS'08), July 2008, Noordwijk, The Netherlands, IEEE Computer Society Press, pp. 513-519.

17. R. Narayanan, N. Abbasi, G. Al Sammane, M. Zaki, and S. Tahar: A Comparative Study of AMS Circuit Simulation in VHDL-AMS and SystemC-AMS; Proc. International Conference on Embedded Systems & Critical Applications (ICESCA'08), Gammarth, Tunisia, May 2008, pp. 23-28.

18. W. Denman, M. Zaki and S. Tahar: A Bond Graph Approach for the Constraint based Verification of Analog Circuits; Proc. Workshop on Formal Verification of Analog Circuit (FAC'08), July 2008, Princeton, New Jersey, USA, pp. 1-28.

19. O. Hasan and S. Tahar: Performance Analysis of ARQ Protocols using a Theorem Prover; IEEE International Symposium on Performance Analysis of Systems and Software (ISPASS'08), Austin, Texas, USA, April 2008, IEEE Computer Society Press, pp 85-94.

20. M. Zaki, S. Tahar, and G. Bois: Qualitative Abstraction based Verification for Analog Circuits; Proc. Workshop On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'07), Poitier, France, December 2007, pp. 147-158

21. T.H. Khan, A. Habibi, S. Tahar and O. A. Mohamed. Automatic Generation of SystemC Transactors from Graphical FSM”; In Proc. IEEE International Conference on Microelectronics (ICM’07), Cairo, Egypt, December 2007. pp. 271-274.

22. Z.J. Dong, M.H. Zaki, G. Al Sammane, S. Tahar and G. Bois: Checking Properties of PLL Designs using Run-time Verification; Proc. IEEE International Conference on Microelectronics (ICM'07), Cairo, Egypt, December 2007, pp. 129-132.

23. O.Hasan and S. Kort. Automated Formal Synthesis of Wallace Tree Multipliers; Proc. IEEE Midwest Symposium on Circuits & Systems (MWSCAS'07), Montreal, Quebec, Canada, August 2007, pp. 293-296.

24. M. Zaki, G. Al Sammane, S. Tahar, and G. Bois: Combining Symbolic Simulation and Interval Arithmetic for the Verification of AMS Designs; Proc. IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD'07), Austin, Texas, USA, November 2007, IEEE Computer Society Press. pp. 207-215.

25. O. Hasan and S. Tahar: Verification of Tail Distribution Bounds in a Theorem Prover; In: T.E.Simos, G. Psihoyios and Ch. Tsitouras (Eds.), Numerical Analysis and Applied Mathematics, AIP Conference Proceedings Vol.936, 2007, pp. 259-262. [Proc. International Conference of Numerical Analysis and Applied Mathematics (ICNAAM'07), Corfu, Greece, September 2007.]

26. G. Al Sammane, M.H. Zaki, Z.J. Dong and S. Tahar: Towards Assertion Based Verification of Analog and Mixed Signal Designs Using PSL; Proc. Languages for Formal Specification and Verification, Forum on Specification & Design Languages (FDL'07), Barcelona, Spain, September 2007, pp. 293-298.

27. T.H. Khan, A. Habibi, S. Tahar and O. Ait Mohamed: Automatic Generation of SystemC Transactors from AsmL Specification; Proc. Languages for Formal Specification and Verification, Forum on Specification & Design Languages (FDL'07), Barcelona, Spain, September 2007. pp. 104-109.

28. O. Hasan and S. Tahar: Verification of Expectation Properties for Discrete Random Variables in HOL; In: K.Schneider and J.Brandt (Eds.), Theorem Proving in Higher-Order Logics, Lecture Notes in Computer Science 4732, Springer Verlag, 2007, pp. 119-134. [Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'07), Kaiserslautern, Germany, September 2007.]

29. Z.J. Dong, M. Zaki, G. Al Sammane, S. Tahar, and G. Bois: Run-Time Verification using the VHDL-AMS Simulation Environment; Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'07), Montreal, Quebec, Canada, August 2007, pp. 1513-1516.

30. G. Al Sammane, M. Zaki, S. Tahar, and G. Bois: Constraint-Based Verification of Delta Sigma Modulators Using Interval Analysis; Proc. IEEE Midwest Symposium on Circuits & Systems (MISWEST'07), Montreal, Quebec, Canada, August 2007, pp. 726-729.

31. O. Hasan and S. Tahar: Formalization of Continuous Probability Distributions; In: F. Pfenning (Ed.), Automated Deduction, Lecture Notes in Computer Science 4603, Springer Verlag, 2007, pp. 2-18. [Proc. 21st Conference on Automated Deduction (CADE-21), Bremen, Germany, July 2007.]

32. O. Hasan and S. Tahar: Verification of Probabilistic Properties in the HOL Theorem Prover; In: J. Davies and J. Gibbons (Eds.), Integrated Formal Methods, Lecture Notes in Computer Science 4591, Springer Verlag, 2007, pp. 333-352. [Proc. International Conference on Integrated Formal Methods (IFM'07), Oxford, UK, July 2007.]

33. M. Zaki, G. Al Sammane, and S. Tahar: Formal Verification of Analog and Mixed Signal Designs in Mathematica; In: Y. Shi et al. (Eds.), Computational Science, Lecture Notes in Computer Science 4488, Springer Verlag, 2007, pp. 263-267. [Proc. International Conference on Computational Science (ICCS'07), Beijing, China, May 2007]

34. M. Zaki, S. Tahar, and G. Bois: A Symbolic Approach for the Safety Verification of Continuous Systems; Proc. International Conference on Computational Science (ICCS'07), Beijing, China, May 2007, pp. 93-100.

35. A. Gawanmeh and S. Tahar: Rank Theorems for Forward Secrecy in Group Key Management Protocols; Proc. IEEE International Conference on Advanced Information Networking and Applications Workshops (AINAW'07), Niagara Falls, Canada, May 2007, pp. 18-23. IEEE Computer Society Press.

36. G. Al Sammane, M. Zaki, and S. Tahar: A Symbolic Methodology for the Verification of Analog and Mixed Signal Designs; Proc. IEEE/ACM Design Automation and Test in Europe (DATE'07), Nice, France, April 2007, pp. 249-254.

37. Y.J. Shin, A. Habibi, and S. Tahar: A SystemC Transaction Level Model for MIPS R3000 Processor; Proc. Sciences of Electronics, Technologies of Information and Telecommunications (SETIT'07), Hammamet, Tunisia, March 2007, pp. 1-8.

38. A. Gawanmeh, A. Habibi, and S. Tahar: Embedding and Verification of PSL using ASM;  Proc. IEEE International Workshop on System-on-Chip (IWSOC'06), Cairo, Egypt, December 2006, pp. 125-130, IEEE Computer Society Press.

39. A. Samara, A. Habibi, and S. Tahar: Automated Coverage Directed Test Generation Using Cell-Based Genetic Algorithm; Proc. IEEE International High Level Design Validation and Test Workshop (HLDVT'06), Monterey, California, USA, November 2006, pp. 19-26, IEEE Computer Society Press.

40. N. Abdullah, B. Akbarpour, and S. Tahar: Formal Analysis and Verification of an OFDM Modem Design using HOL; Proc. IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD'06), San Jose, California, USA, November 2006, pp. 189-190, IEEE Computer Society Press.

41. H. Moinudeen, A. Habibi, and S. Tahar: Design for Verification of the PCI-X Bus; Proc. IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD'06), San Jose, California, USA, November 2006, pp. 187-188, IEEE Computer Society Press.

42. M. Zaki, S. Tahar, and G. Bois: Abstraction Based Verification of Analog Circuits Using Computer Algebra and Constraint Solving; Proc. IEEE International Workshop on Symbolic Methods and Applications to Circuit Design (SMACD'06), Florence, Italy, October 2006, pp. 1-8.

43. A.T. Abdel-Hamid, S. Tahar, and E.M. Aboulhamid: Finite State Machine IP Watermarking: A Tutorial; Proc. First NASA/ESA Conference on Adaptive Hardware and Systems (AHS 2006), June 2006, Istanbul, Turkey, pp. 457-464, IEEE Computer Society Press.

44. M. Zaki, S. Tahar, and G. Bois: Formal Verification of Analog and Mixed Signal Designs: Survey and Comparison; Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'06), Gatineau, Quebec, Canada, June 2006, pp. 281-284.

45. H. Moinudeen, A. Habibi, and S. Tahar: Model Based Verification of SystemC Designs; Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'06), Gatineau, Quebec, Canada, June 2006, pp. 289-292.

46. M. Zaki, S. Tahar, and G. Bois: A Practical Approach for Monitoring Analog Circuits; Proc. ACM 16th Great Lakes Symposium on VLSI (GLS-VLSI'06), Philadelphia, Pennsylvania, USA, April 2006, ACM Publications, pp. 330-335.

47. A. Habibi, H. Moinudeen, A. Samara, S. Tahar: Towards a Faster Simulation of SystemC Designs; Proc. IEEE Computer Society Annual Symposium on VLSI (ISVLSI'06), Karlsruhe, Germany, March 2006, pp. 418-419, IEEE Computer Society Press.

48. A. Habibi, S.Tahar, A. Samara, D. Li, O. Ait-Mohamed: Efficient Assertion Based Verification using TLM; Proc. IEEE/ACM Design Automation and Test in Europe (DATE'06), Munich, Germany, March 2006, pp. 106-111.

49.  A. Habibi, H. Moinudeen and S. Tahar: Generating Finite State Machines from SystemC; Proc. IEEE/ACM Design Automation and Test in Europe (DATE'06), Munich, Germany, March 2006, pp. 76-81.

50. J. Ben Hassen and S. Tahar: On the Numerical Verification of Probabilistic Rewriting Systems; Proc. IEEE/ACM Design Automation and Test in Europe (DATE'06), Munich, Germany, March 2006, pp. 1223-1224.

51. A. Habibi and S. Tahar: On the Formal Verification of a SystemC Packet Switch Model; Proc. IEEE International Conference on Electronics, Circuits and Systems (ICECS'05), Gammarth, Tunisia, December 2005, Vol. 1, pp. 252-255.

52. A. Habibi and S. Tahar: An Approach for the Verification of SystemC Designs using AsmL;  In: D.A. Peled. and Y.-K. Tsay (Eds.), Automated Technology for Verification and Analysis, Lecture Notes in Computer Science 3707, Springer Verlag, 2005, pp. 69-83. [Proc. International Symposium on Automated Technology for Verification and Analysis (ATVA'05), Taipei, Taiwan, October 2005]

53. M. Zaki, S. Tahar, and G. Bois: On the formal Analysis of Analog Systems using Interval Abstraction; Proc. NETCA Workshop on Verification and Theorem Proving for Continuous Systems, Oxford, UK, August 2005, pp. 42-56.

54. B. Akbarpour and S. Tahar: Incorporating Formal Methods in the Design Flow of DSP Systems; Proc. NETCA Workshop on Verification and Theorem Proving for Continuous Systems, Oxford, UK, August 2005, pp. 31-41.

55. Donglin li, A.I. Ahmed, and O. Ait Mohamed. STE Based Verification of Look-Aside Interface. Proc. IEEE Canadian Conference on Electrical and Computer Engineering (CCECE’05), Saskatoon, Saskatchewan, Canada, May 2005.

56. A. Habibi and S. Tahar: A Framework for the Verification of SystemC Transaction Level Models; Proc. 2005 Micronet Annual Workshop, Ottawa, Canada, May 2005, pp. 99-100

57. A. Habibi and S. Tahar: Design for Verification of SystemC Transaction Level Models; Proc. IEEE/ACM Design Automation and Test in Europe (DATE'05), Munich, Germany, March 2005, pp. 560-566.

58.  A. Habibi, A.I. Ahmed, O. Ait-Mohamed and S. Tahar: On the Design and Verification of the Look-Ahead Interface;  Proc. IEEE/ACM Design Automation and Test in Europe (DATE'05), Munich, Germany, March 2005, pp. 290-296.

59. A. Abdel-Hamid, S. Tahar, and E.M. Aboulhamid: A Public-Key Watermarking Technique for IP Designs;  Proc. IEEE/ACM Design Automation and Test in Europe (DATE'05), Munich, Germany, March 2005, pp. 330-336.

60. A. Gawanmeh, A. Habibi, and S. Tahar: Embedding and Verification of PSL using ASM; Proc. International Conference on Abstract State Machines (ASM'05), Paris, France, March 2005, pp. 201-215. 

61. A. Habibi, and S. Tahar: AsmL Semantics in Fixpoint; Proc. International Conference on Abstract State Machines (ASM'05), Paris, France, March 2005, pp 233-245.

62. H. Moinudeen, A. Habibi, and S. Tahar: An Executable Specification of the PCI-X Bus Standard in AsmL; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'05), Saskatoon, Saskatchewan, Canada, May 2005, pp. 1247-1250.

63. A. Merhebi and O. Ait Mohamed. FPGA Implementation of a Modular and Pipelined WF Scheduler for high speed OC192 Networks. Conference GLSVLSI 2005 (Great Lakes Symposium on VLSI circuits) Chicago USA.

64. A. Habibi and S. Tahar: On the Transformation of SystemC to AsmL using Abstract Interpretation; Proc. Int. Workshop on Abstract Interpretation for Object Oriented Languages (AIOOL'05), Paris, France, January 2005, pp. 1-11.

65. R. Mizouni, S. Tahar and P. Curzon: A Hybrid Tool Integrating HOL Theorem Proving with MDG Model Checking; Proc. IEEE International Conference on Microelectronics (ICM'04), Tunis, Tunisia, December 2004, pp. 392-395.

66. F. Fereydouni-forouzand and O. Ait Mohamed. An FPGA Implementation of a Modified Version of a RED Algorithm. In Proc.  IEEE International Conference on Field Programmable Technology (FPT'04), December 2004.

67. A. Merhebi and O. Ait Mohamed. A Scalable and Pipelined FPGA implementation of an OC192 WF Scheduler. In Proc. IEEE International Conference on Field Programmable Technology (FPT'04), December 2004.

68. T. Mhamdi and S. Tahar: Providing Automated Verification in HOL using MDGs; In: F. Wang (Ed.), Automated Technology for Verification and Analysis, Lecture Notes in Computer Science 3299, Springer Verlag, 2004, pp. 278-293. [Proc. International Symposium on Automated Technology for Verification and Analysis (ATVA'04), Taipei, Taiwan, November 2004]

69. F. Wang, S. Tahar, and O. Ait Mohamed: First-order LTL Model Checking using MDGs; In: F. Wang (Ed.), Automated Technology for Verification and Analysis, Lecture Notes in Computer Science 3299, Springer Verlag, 2004, pp. 441-455. [Proc. International Symposium on Automated Technology for Verification and Analysis (ATVA'04), Taipei, Taiwan, November 2004]

70. B. Akbarpour and S. Tahar: A Methodology for the Formal Verification of FFT Algorithms in HOL; In: A. Hu and A. Martin (Eds.), Formal Methods in Computer-Aided Design, Lecture Notes in Computer Science 3312, Springer Verlag, 2004, pp. 37-51. [Proc. International Conference on Formal Methods in Computer-Aided Design (FMCAD'04), Austin, Texas, USA, November 2004

71. A. Habibi and S. Tahar: Towards an Efficient Assertion Based Verification of SystemC DesignsProc. IEEE International High Level Design Validation and Test Workshop (HLDVT'04), Sonoma Valley, California, USA, November 2004, pp. 19-22.

72. A. Habibi, A. Gawanmeh and S. Tahar: Assertion Based Verification of PSL for SystemC Designs; Proc. IEEE International Symposium on System-on-Chip (SOC'04), Tampere, Finland, November 2004, pp. 177-180.

73. K. Oumalou, A. Habibi and S. Tahar: Design for verification of a PCI bus in SystemC; Proc. IEEE International Symposium on System-on-Chip (SOC'04), Tampere, Finland, November 2004, pp. 201-204.

74. A. Gawanmeh, A. Habibi and S. Tahar: Enabling SystemC Verification using Abstract State Machines; Proc. Languages for Formal Specification and Verification, Forum on Specification & Design Languages (FDL'04), Lille, France, September 2004, pp. 649-661.

75. B. Akbarpour and S. Tahar: Error Analysis of Digital Filters using Theorem Proving; In: K. Slind and G. Gopalakrishnan (Eds.), Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 3223, Springer Verlag, 2004, pp. 1-16. [Proc. International Conference on Theorem Proving in Higher in Higher-Order Logics (TPHOLs'04), Park City, Utah, USA, September 2004]

76.  T. Mhamdi and S. Tahar: Embedding Multiway Decision Graphs in HOL; B-Track; Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'04), Park City, Utah, USA, September 2004, pp. 121-136

77. S. Jahanpoor and O. Ait Mohamed. Automatic Generation of Model Checking Properties and Constraints from Production Based Specification. In Proc. IEEE Midwest Symposium on Circuits and Systems (MWSCAS’04), July 2004.

78.  M. Zaki, Y. Mokhtari and S. Tahar: SynAbs: Model Reduction Tool for Verilog Verification; Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'04), Montreal, Quebec, Canada, June 2004, pp. 57-60.

79.  A. Habibi, S. Tahar and L. Halleb: Formal Verification of a Bus Structure Modeled in SystemC; Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'04), Montreal, Quebec, Canada, June 2004, pp. 61-64.

80. D. Li, M. HU, and O. Ait Mohamed. Built-In Self-Test Design of Motion Estimation Computing Array. In Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS’04), June 2004.

81. M. Krykhtin, Y. Mokhtari, O. Ait Mohamed, and X. Song. Towards Software Model Checking using MDGs. In Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS’04), June 2004.

82.  A.T. Abdel-Hamid, S. Tahar and E.M. Aboulhamid: A Tool for Automatic Watermarking of IP Designs; Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'04), Montreal, Quebec, Canada, June 2004, pp. 381-384.

83. J. Ben Hassen and S. Tahar: Formal Verification of an SoC Platform Converter; Proc. IEEE International Symposium on Circuits and Systems (ISCAS'04), Vancouver, B.C., Canada, May 2004, Vol. 5, pp. 313-316.

84. A. Habibi and S. Tahar: On the Extension of SystemC by SystemVerilog Assertions; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'04), Niagara Falls, Ontario, Canada, May 2004, Vol. 4, pp. 1869-1872.

85. A. Abdel-Hamid, M. Zaki, and S. Tahar: A tool for Converting Finite State Machine to VHDL; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'04), Niagara Falls, Ontario, Canada, May 2004, Vol. 4, pp. 1907-1910 .

86. F. Wang, S. Tahar, and O. Ait Mohamed: Automaton based Model Checking Using Multiway Decision Graphs; Proc. 2004 Micronet Annual Workshop, Alymer, Canada, April 2004, pp. 133-134.

87.  P. Hong, S. Tahar, and Y. Mokhtari: Compositional Verification of a Switch Fabric from Nortel Networks ; In: J. Dong and J. Woodcock (Eds.), Formal Engineering Methods, Lecture Notes in Computer Science 2885, pp. 560-578, Springer Verlag, 2003. [Proc. International Conference on Formal Engineering Methods (ICFEM'03), Singapore, November 2003.]

88. B. Akbarpour and S. Tahar: Modeling SystemC Fixed-Point Arithmetic in HOL; In: J. Dong and J. Woodcock (Eds.), Formal Engineering Methods, Lecture Notes in Computer Science 2885, pp. 206-225, Springer Verlag, 2003. [Proc. International Conference on Formal Engineering Methods (ICFEM'03), Singapore, November 2003.]

89. M. Layouni, J. Hooman, and S. Tahar: On the correctness of an Intrusion-Tolerant Group Communication Protocol; In: D. Geist, E. Tronci (Eds.), Correct Hardware Design and Verification Methods, Lecture Notes in Computer Science 2860, pp. 231-246, Springer Verlag, 2003. [Proc. 12th IFIP Conf. on Correct Hardware Design and Verification Methods (CHARME'03), L'Aquila, Italy, October 2003.]

90. A. Gawanmeh, S. Tahar, and K. Winter; A Tool for Verifying ASM Models using Multiway Decision Graphs; Proc. 2003 Micronet Annual Workshop, Toronto, Canada, October 2003, pp. 127-128. 

91. A. Gawanmeh, S. Tahar, and K. Winter: Formal Verification of ASM Designs using the MDG Tool; Proc. IEEE International Conference on Software Engineering and Formal Methods (SEFM'03), Brisbane, Australia, September 2003, pp. 210-219, IEEE Computer Society Press.

92. M. Layouni, J. Hooman, and S. Tahar: Modeling and Verification of Leaders Agreement in the Intrusion-Tolerant Enclaves Using PVS; B-Track Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'03), Roma, Italy, September 2003, pp145-158. [In: D. Basin and B. Wolff (Eds.), TPHOLs 2003 Emerging Trends Proceedings, Technical Report No. 187, Institut of Informatics, Albert-Ludwigs University, Freiburg, Germany.]

93. B. Akbarpour and S. Tahar: The Application of Formal Verification to SPW Designs; Proc. EUROMICRO Symposium on Digital System Design (DSD'03), Belek, Turkey, September 2003, pp. 325 -332, IEEE Computer Society Press. 

94. R. Mizouni, S. Tahar, and P. Curzon: On the Embedding of MDG Specification Languages in HOL; Proc. IEEE International Conference on Computer Systems and Applications (AICCSA'03), Tunis, Tunisia, July 2003, pp. 71-78. IEEE Computer Society Press.

95. A.T. Abdel-Hamid, S. Tahar, and E.M. Abulhamid: IP Watermarking Techniques: Survey and Comparison; Proc. IEEE 3rd International Workshop on System-on-Chip (IWSOC'03), Calgary, Alberta, Canada, June-July 2003, pp. 60-65, IEEE Computer Society Press.

96. A. Habibi and S. Tahar: A Survey on System-On-a-Chip Design Languages; Proc. IEEE 3rd International Workshop on System-on-Chip (IWSOC'03), Calgary, Alberta, Canada, June-July 2003, pp. 212-215, IEEE Computer Society Press.

97. M. Zaki, Y. Mokhtari, and S. Tahar: A Path Dependency Graph for Verilog Program Analysis; Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'03), Montreal, Quebec, Canada, June 2003, pp. 109-112.

98. F. Wang, A. Habibi, and S. Tahar: Translating LTL Specification to MDG-HDL; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'03), Montreal, Quebec, Canada, May 2003, Vol. 2, pp. 1369-1373.

99. M. Zaki and S. Tahar: Syntax Code Analysis and Generation for Verilog; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'03), Montreal, Quebec, Canada, May 2003, Vol. 1, pp. 235-240.

100. J. Lu and S. Tahar: Modeling and Verification of an ATM Port Controller in VIS; PrProc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'03), Montreal, Quebec, Canada, May 2003, Vol. 1, pp. 241-245.

101. F. Wang and S. Tahar: Language Emptiness Checking using MDGs; Proc. ACM 13th Great Lakes Symposium on VLSI (GLS-VLSI'03), Washington D.C., USA, April 2003, pp. 88-91, ACM Publications.

102. A.T. Abdel-Hamid, S. Tahar, and J. Harrison; Hierarchical Approach for the Verification of an IEEE-754 Floating-Point Function; Proc. 2002 Micronet Annual Workshop, Alymer, Canada, April 2002, pp. 107-108.

103. A. Gawanmeh, S. Tahar and K. Winter: Interfacing ASMs with the MDG Tool; In: E. Boerger, A. Gargantini, E. Riccobene (Eds.) Abstract State Machines - Advances in Theory and Applications, Lecture Notes in Computer Science 2589, Springer Verlag, 2003, pp. 278-292. [Proc. International Conference on Abstract State Machines (ASM'03), Taormina, Italy, March 2003.]

104. A.T. Abdel-Hamid, S. Tahar, and J. Harrison: Enabling Hardware Verification through Design Changes; In: C. George and H. Miao (Eds.), Formal Methods in Software Engineering, Lecture Notes in Computer Science 2495, Springer Verlag, 2002, pp. 459-470. [Proc. International Conference on Formal Engineering Methods (ICFEM'02), Shanghai, China, October 2002.]

105. M.H. Zobair and S. Tahar: Formal Verification of a SONET Telecom System Block; Proc. International Conference on Formal Engineering Methods (ICFEM'02), Lecture Notes in Computer Science, Springer Verlag, Shanghai, China, October 2002.

106. H. Peng, Y. Mokhtari, and S. Tahar: Environment Synthesis for Compositional Model Checking; Proc. IEEE International Conference on Computer Design (ICCD'02), Freiburg, Germany, September 2002, IEEE Computer Society Press, pp 70-75.

107. A. Habibi, S. Tahar, and A. Ghazel: Formal Verification of a DSP Chip Using an Iterative Approach; Proc. EUROMICRO Symposium on Digital System Design (DSD'02), Dortmund, Germany, September 2002, pp. 12-19.

108. B. Akbarpour, S. Tahar, and A. Dekdouk: Formalization of Cadence SPW Fixed-Point Arithmetic in HOL; In: M. Butler, L. Petre, and K. Sere (Eds.), Integrated Formal Methods, Lecture Notes in Computer Science 2335, Springer Verlag, 2002, pp. 185-204. [Proc. International Conference on Integrated Formal Methods (IFM'02), Turku, Finland, May 2002.]

109. H. Xiong, P. Curzon, S. Tahar, and A. Blandford: Formally Linking MDG and HOL Based on a Verified MDG System; In: M. Butler, L. Petre, and K. Sere (Eds.), Integrated Formal Methods, Lecture Notes in Computer Science 2335, Springer Verlag, 2002, pp. 205-224. [Proc. International Conference on Integrated Formal Methods (IFM'02), Turku, Finland, May 2002.]

110. A. Habibi, S. Tahar, and A. Ghazel: Behavioral Modeling and Verification of the ADSP-2100 Processor using HOL; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'02), Winnipeg, Manitoba, Canada, May 2002, Vol. 2, pp. 614-619.

111. F. Wang, S. Tahar, and E. Cerny: Towards Language Emptiness Model Checking for MDGs; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'02), Winnipeg, Manitoba, Canada, May 2002, Vol. 2, pp. 590-595.

112. A. Habibi, S. Tahar, and A. Ghazel: A Progressive Methodology for the Verification of a DSP Chip; Proc. ACM 12th Great Lakes Symposium on VLSI (GLS-VLSI'02), New York City, New York, USA, April 2002. 

113. J. Lu and S. Tahar: On the Model Checking of the RCMP-800 Input FIFO; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'02), Winnipeg, Manitoba, Canada, May 2002, Vol. 1, pp. 578-583.

114. P. Curzon and S. Tahar: Automating the Verification of Parameterized Hardware using a Hybrid Tool; Proc. IEEE 13th International Conference on Microelectronics (ICM'01), Rabat, Morocco, October 2001, pp. 257-260.

115. J. Lu and S. Tahar: Design and Verification of a Knockout ATM Concentrator; Proc. IEEE 13th International Conference on Microelectronics (ICM'01), Rabat, Morocco, October 2001, pp. 261-264.

116. L. Barakatain and S. Tahar: Functional Verification of a SCI-PHY Level 2 Protocol Engine; Proc. IEEE International Conference on Information, Communications & Signal Processing (ICICS'01), Singapore, October 2001.

117. P. Hong, Y. Mokhtari, and S. Tahar: Model Reduction Based on Value Dependency; Proc. IEEE International ASIC/SOC Conference (ASIC'01), Washington, DC, USA, September 2001, pp. 220-224.

118. H. Xiong, P. Curzon, S. Tahar, and A. Blandford: Proving Existential Theorems when Importing Results from MDG to HOL; B-Track Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'01), Edinburgh, Scotland, UK, September 2001, pp. 384-399. In: R.J. Boulton and P.B. Jackson (Eds.), [TPHOLs 2001: Supplemental Proceedings, Informatic Reprot Series EDI-INF-RR-0046, Division of Informatics, University of Edinburgh, Edinburgh, UK, September 2001.]

119. A.T. Abdel-Hamid, S. Tahar, and J. Harrison: Hierarchical Verification of the Implementation of the IEEE-754 Table-Driven Floating-Point Exponential Function using HOL; B-Track Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'01), Edinburgh, Scotland, UK, September 2001, pp. 1-16. [In: R.J. Boulton and P.B. Jackson (Eds.), TPHOLs 2001: Supplemental Proceedings, Informatic Reprot Series EDI-INF-RR-0046, Division of Informatics, University of Edinburgh, Edinburgh, UK, September 2001.]

120. S. Kort, S. Tahar, and P. Curzon: Hierarchical Verification Using an MDG-HOL Hybrid Tool; In: Margaria, T. and Melham, T. (Eds.), Correct Hardware Design and Verification Methods, Lecture Notes in Computer Science 2144, Springer Verlag, 2001, pp. 244-258. Proc. 11th IFIP Conference on Correct Hardware Design and Verification Methods (CHARME'2001), Livingston, Scotland, UK, September 2001.

121. L. Baratain and S. Tahar: Model Checking of the Fairisle ATM Switch Fabric using FormalCheck; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'01), Toronto, Ontario, Canada, May 2001.

122. M.H. Zobair and S. Tahar: Modeling and Formal Verification of a Telecom System Block using MDGs; Proc. 2001 Micronet Annual Workshop, Alymer, Canada, April 2001, pp. 161-162.

123. L. Barakatain, S. Tahar, J. Lamarche, and J-M Gendreau: Practical Approaches to the Model Checking of a Telecom Megacell using FormalCheck; Proc. ACM 11th Great Lakes Symposium on VLSI (GLS-VLSI'01), West Lafayette, Indiana, USA, March 2001, ACM Publications, pp. 1-6.

124. Y. Mokhtari, M. Shirazipour, and S. Tahar: A Case Study on Model Checking and Refinement of Abstract State Machines; Proc. Eight International Conference on Computer Aided Systems Theory (EUROCAST'01), Las Palmas de Gran Canaria, Canary Islands, Spain, February 2001, pp. 239-242.

125. P. Hong and S. Tahar: Hardware Modeling and Verifiation of an ATM Ring MAC Protocol; Proc. IEEE 12th International Conference on Microelectronics (ICM'00), Teheran, Iran, November 2000, pp. 21-24.

126. P. Hong, S. Tahar, and F. Khendek: SPIN vs. VIS: A Case Study on the Formal Verification of the ATMR Protocol; Proc. IEEE International Conference on Formal Engineering Methods (ICFEM'2000), York, UK, September 2000, IEEE Computer Society Press, pp. 79-87.

127. H. Xiong, P. Curzon, S. Tahar, and A. Blandford: Embedding and Verification of an MDG-HDL Translator in HOL; B-Track Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'2000), Portland, Oregon, USA, August 2000, pp. 237-248.

128. M. Azizi, E.-M. Aboulhamid, and S. Tahar: Sequential and Distributed Simulations using Java Threads; Proc. IEEE International Conference on Parallel Computing in Electrical Engineering (PARELEC'2000), Trois-Rivières, Québec, Canada, August 2000, pp. 237-241. IEEE Computer Society

129. M. Hasan, S. Tahar, and P. Curzon: Impact of Design Changes on Verification Using MDGs; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'00), Halifax, Nova Scotia, Canada, May 2000, pp. 173-178.

130. A. A. Mir, S. Balakrishnan, and S. Tahar: Modeling and Verification of an Embedded System using Cadence SMV; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'00), Halifax, Nova Scotia, Canada, May 2000, pp. 179-183.

131. S. Kort, S. Tahar, P. Curzon, X. Song: HOL-MDG: A Hybrid Tool for Forma1 Verification;  Proc. 2000 Micronet Annual Workshop, Ottawa, Canada, April 2000, pp. 131-132.

132. V.K. Pisini, S. Tahar, P. Curzon, O. Ait-Mohamed and X. Song: Formal Hardware Verification by Integrating HOL and MDG; Proc. ACM 10th Great Lakes Symposium on VLSI (GLS-VLSI'00), Chicago, Illinois, USA, March 2000, ACM Publications, pp. 23-28.

133. H. Peng and S. Tahar: Compositional Verification of IP Based Designs; Proc. IFIP International Worshop on IP Based Synthesis and System Design, Grenoble, France, December 1999, pp. 189-193.

134. M. Palanisamy and S. Tahar: Formal Verification of the RCMP Egress Routing Logic; Proc. IEEE 11th International Conference on Microelectronics (ICM'99), Kuwait City, Kuwait, November 1999, pp. 89-92.

135. H. Xiong, P. Curzon, and S. Tahar: Importing MDG Results into HOL ;In: Bertot, Y.; Dowek, G.; Hirschowitz, A.; Paulin, C. and Theryvon, L. (Eds.), Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 1690, Springer Verlag, 1999, pp. 293-310. Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'99), Nice, France, September 1999.

136. M. Azizi, E.-M. Aboulhamid and S. Tahar: Properties Coverification for HW/SW Systems; Proc. 2nd Electronic Circuits and Systems Conference (ECS'99),pp. 81-84, Bratislava, Slovakia, September 1999.

137. M. Azizi, E.-M. Aboulhamid, and S. Tahar: Multithreading-Based Co-Verification Technique of HW/SW Systems ; Proc. International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99), CSREA Press, Vol. VI, pp. 1999-2005, Las Vegas, Nevada, USA, June/July 1999. 

138. H.T. Bui and S. Tahar: Design and Synthesis of an IEEE-754 Exponential Function; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'99), pp. 450-455, Edmonton, Alberta, Canada, May 1999.

139. M. Palanisamy and S. Tahar: RTL Design and Verification of the RCMP Egress Routing Logic; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'99), pp. 111-115, Edmonton, Alberta, Canada, May 1999.

140. T.H Bui, T. Elshabrawy, F. Khendek, S. Tahar, and T. LeNgoc: Description and Validation of the Internet Stream Protocol (ST2+) Using SDL/MSC; Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'99), pp. 238-244, Edmonton, Alberta, Canada, May 1999.

141. V.K. Pisini, S. Tahar, O. Ait-Mohamed, P. Curzon, and X. Song: An Approach to Link HOL and MDG for Hardware Verification; Proc. 1999 Micronet Annual Workshop, Ottawa, Canada, April 1999, pp. 156-157.

142. S. Balakrishnan and S. Tahar: A Hierarchical Approach to the Formal Verification of Embedded Systems Using MDGs; Proc. IEEE 9th Great Lakes Symposium on VLSI (GLS-VLSI'99), Ann Arbor, Michigan, USA, March 1999, IEEE Computer Society Press, pp. 284-287.

143. S. Balakrishnan and S. Tahar: Modeling and Formal Verification of a Commercial Microcontroller for Embedded System Applications; Proc. IEEE 10th International Conference on Microelectronics (ICM'98), Monastir, Tunisia, December 1998, pp. 107-110.

144. S. Tahar, P. Curzon and J. Lu: Three Approaches to Hardware Verification: HOL, MDG and VIS Compared; In Gopalakrishnan, G. and Windley, P. (Eds.), Formal Methods in Computer-Aided Design, Lecture Notes in Computer Science 1522, Springer Verlag, 1998, pp. 433-450. Proc. International Conference on Formal Methods in Computer-Aided Design (FMCAD'98), Palo Alto, California, USA, November 1998.

145. J. Lu, S. Tahar, D. Voicu and X. Song: Model Checking of a real ATM Switch; Proc. IEEE International Conference on Computer Design (ICCD'98), Austin, Texas, USA, October 1998, IEEE Computer Society Press, pp. 195-198.

146. P. Curzon, S. Tahar, and O. Ait-Mohamed: Verification of the MDG Components Library in HOL; In: J. Grundy and M. Newey (Eds.), Theorem Proving in Higher Order Logics: Emerging Trends, The Australian National University, 1998, pp. 31-45. Supplementary Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'98), Canberra, Australia, September 1998.

147. J. Lu and S. Tahar: Practical Approaches to the Automatic Verification of an ATM Switch Fabric using VIS; Proc. IEEE 8th Great Lakes Symposium on VLSI (GLS-VLSI'98), Lafayette, Louisiana, USA, February 1998, IEEE Computer Society Press, pp. 368-373.

148. Ying Xu, Eduard Cerny, Xiaoyu Song, Francisco Corella, Otmane Aït Mohamed: Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs. (CAV 1998): 219-231

149. A.E.K Dekdouk, Otmane Aït Mohamed, Sadegh Jahanpour, Eduard Cerny.What About Formal Verification of IP-based SoC Designs International Conference IWLAS'98. Grenoble,France.

150. Mostefa Azizi, Otmane Aït Mohamed, Xiaoyu Song.Cache Coherence Protocol Verification of Multiprocessor System with Shared Memory Microelectronics(ICM'98).Monastir, Tunisia. Dec. 14-16, 98

151. Otmane Aït Mohamed, Eduard Cerny, Xiaoyu Song: MDG-based Verification by Retiming and Combinational Transformations. Proc. of the  Great Lakes Symposium on VLSI (GLS-VLSI'98):  356--361.IEEE Computer Society Press.

152. Otmane Aït Mohamed, Xiaoyu Song, Eduard Cerny: On the non-termination of MDGs-based abstract state enumeration. CHARME 1997: 218-235

153. Z. Zhou, X. Song, S. Tahar, E. Cerny, F. Corella and M. Langevin: Verification of the Island Tunnel Controller using Multiway Decision Graphs; In: Srivas, M. and Camilleri, A. (Eds.), Formal Methods in Computer-Aided Design, Lecture Notes in Computer Science 1166, Springer Verlag, 1996, pp. 233-246. Proc. International Conference on Formal Methods in Computer-Aided Design (FMCAD'96), Palo Alto, California, USA, November 1996.

154. M. Langevin, S. Tahar, Z. Zhou, X. Song and E. Cerny: Behavioral Verification of an ATM Switch Fabric using Implicit Abstract State Enumeration; Proc. IEEE International Conference on Computer Design (ICCD'96) , Austin, Texas, USA, October 1996, IEEE Computer Society Press, pp. 20-26.

155. S. Tahar and P. Curzon: A Comparison of MDG and HOL for Hardware Verification; In: von Wright, J.; Grundy, J. and Harrison, J. (Eds.), Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 1125, Springer Verlag, 1996, pp. 415-430. Proc. International Conference on Theorem Proving in Higher Order Logics (TPHOLs'96), Turku, Finland, August 1996.

156. Z. Zhou, X. Song, F. Corella, M. Langevin, E. Cerny and S. Tahar: MDG Tools for the Verification of RTL Designs; In: Alur, R. and Henzinger, T. (Eds.), Computer Aided Verification, Lecture Notes in Computer Science 1102, Springer Verlag, 1996, pp. 433-436. Proc. Conference on Computer Aided Verification (CAV'96), New Brunswick, New Jersey, USA, July/August 1996. 

157. S. Tahar, Z. Zhou, X. Song, E. Cerny and M. Langevin: Formal Verification of an ATM Switch Fabric using Multiway Decision Graphs; Proc. IEEE Sixth Great Lakes Symposium on VLSI (GLS-VLSI'96), Ames, Iowa, USA, March 1996, IEEE Computer Society Press, pp. 106-111.

158. S. Tahar, Z. Zhou, X. Song, E. Cerny and M. Langevin: Verification of an ATM Switch Fabric using Multiway Decision Graphs ; Proc. 1996 Micronet Annual Workshop, Ottawa, Canada, March 1996, pp. 77-78.

159. Otmane Aït Mohamed: Mechanizing a pi-Calculus Equivalence in HOL. TPHOLs 1995: 1-16

 

 

 

1. Osman Hasan, Jigar Patel and Sofiene Tahar, Accurate Reliability Analysis of Combinational Circuits using Theorem Proving.Technical Report, Department of Electrical and Computer Engineering, Concordia University, January 2010. [13 Pages].

2. Rajeev Narayanan, Behzad Akbarpour, Mohamed H. Zaki, Sofiene Tahar and Lawrence C. Paulson, Automated Formal Verification of Analog/RF Circuits in the Presence of Noise.Technical Report, Department of Electrical and Computer Engineering, Concordia University, June 2009. [14 Pages].

3. Naeem Abbasi, Rajeev Narayanan, Ghiath Al Sammane, Mohamed H. Zaki and Sofi`ene Tahar. Enabling AMS Simulation using Recurrence Notations. Technical Report, Department of Electrical and Computer Engineering, Concordia University, May 2008. [30 Pages].

4. R.Narayanan, N.Abbasi, M.Zaki, G.Al Sammane, and S.Tahar. On the Simulation Performance of Contemporary AMS Hardware Description Languages. Technical Report, Department of Electrical and Computer Engineering, Concordia University, October 2008. [13 Pages].

5. Z. J. Dong, M.H. Zaki, G. Al Sammane, S. Tahar and G. Bois. A Run-Time Verfication Approach for AMS Designs. Technical Report, Department of Electrical and Computer Engineering, Concordia University, July 2007. [16 Pages].

6. O. Hasan and S. Tahar : Formal Verification of Expectation and Variance for Discrete Random Variables ;  Technical Report, Concordia University, Department of Electrical and Computer Engineering, June 2007 [27 pages]

7. M.H. Zaki, S. Tahar and G. Bois: Combining Constraint Solving and Formal Methods for the Verification of Analog Designs; Technical Report, Concordia University, Department of Electrical and Computer Engineering, June 2007. [28 Pages].

8. M.H. Zaki, G. Al Sammane, S. Tahar and Guy Bois: A Bounded Model Checking Approach for AMS Designs; Technical Report, Concordia University, Department of Electrical and Computer Engineering, May 2007. [22 Pages].

9. A. Gawanmeh, A. Bouhoula and Sofiene Tahar: Rank Functions based Inference System for Group Key Management Protocols Verification. Technical Report, Concordia University, Department of Electrical and Computer Engineering, March 2007.

10. T. Khan, A. Habibi, S. Tahar and O. Mohamed : A Tool for Converting Finite State Machines to SystemC ; Technical Report, Concordia University, Department of Electrical and Computer Engineering, March 2007. [17 pages]

11. O.Hasan and S. Tahar : Formalization of Continuous Probability Distributions ; Technical Report, Concordia University, Department of Electrical and Computer Engineering, February 2007. [42 pages]

12. O.Hasan and S. Tahar : Standard Uniform Distribution Theory in HOL-4; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2006. [14 pages]

13. O.Hasan and S. Tahar : Formalization of the Standard Uniform Random Variable in HOL; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2006. [20 pages].

14. A. Gawanmeh and Sofiene Tahar: Rank Theorems for Forward Secrecy in Group Key Management Protocols. Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2006.

15. A. Gawanmeh and Sofiene Tahar: Formal Specification Requirements for Group Key Management Protocols. Technical Report, Concordia University, Department of Electrical and Computer Engineering, January 2006.

16. M.H. Zaki, S. Tahar, G. Bois: A Survey on Formal Methods for Analog and Mixed Signal Designs, Technical Report, ECE Dept, Concordia University, 2006 [16 Pages].

17. A. Habibi and S. Tahar: Design and Verification of SystemC Transaction Level Models; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2004. [32 pages]

18. A. Habibi and S. Tahar: AsmL Fixpoint Semantics; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2004. [16 pages]

19. A. Habibi and S. Tahar: SystemC Fixpoint Semantics; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2004. [16 pages] 

20. A. Gawanmeh, A. Habibi, and S. Tahar: Enabling SystemC Verification using Abstract State Machines; Technical Report, Concordia University, Department of Electrical and Computer Engineering, May 2004. [15 pages]

21. A. Gawanmeh, A. Habibi, and S. Tahar: An Executable Operational Semantics for SystemC using Abstract State Machines; Technical Report, Concordia University, Department of Electrical and Computer Engineering, March 2004. [24 pages]

22. B. Akbarpour , and S. Tahar: Verification of the Fast Fourier Transform using HOL Theorem Proving; Technical Report, Concordia University, Department of Electrical and Computer Engineering, March 2004. [40 pages]

23. B. Akbarpour , and S. Tahar: Error Analysis of Digital Filters using HOL Theorem Proving; Technical Report, Concordia University, Department of Electrical and Computer Engineering, February 2004. [36 pages]

24. T. Mhamdi, and S. Tahar: Embedding Multiway Decision Graphs in HOL; Technical Report, Concordia University, Department of Electrical andComputer Engineering, February 2004. [20 pages]

25. H. Peng, Y. Mokhrari, and S. Tahar: Environment Synthesis for Compositional Model Checking; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2003. [?? pages] 

26. M. Layouni, J. Hooman and S. Tahar: Formal Specification and Verification of the Intrusion-Tolerant Enclaves Protocol; Technical Report, Concordia University, Department of Electrical and Computer Engineering, November 2003. [23 pages] 

27. H. Peng, Y. Mokhrari, and S. Tahar: Compositional Verification of an ATM Switch Fabric from Nortel Networks: A Case Study; Technical Report, Concordia University, Department of Electrical and Computer Engineering, October 2003. [?? pages]

28. A. Gawanmeh, S. Tahar and Kirsten Winter: Formal Verification of ASM Designs using the MDG Tool; Technical Report, Concordia University, Department of Electrical and Computer Engineering, June 2003. [28 pages]

29. M. Layouni, J. Hooman, and S. Tahar: Modeling and Verification of Leaders Agreement in the Intrusion-Tolerant Enclaves Using PVS; Technical Report, Concordia University, Department of Electrical and Computer Engineering, May 2003. [13 pages]

30. J. Ben Hassen, and S. Tahar: Formal Verification of a Protocol Converter Memory Manager using FormalCheck; Technical Report, Concordia University, Department of Electrical and Computer Engineering, April 2003. [21 pages] 

31.  A. Habibi and S. Tahar: A Survey: System-on-a-Chip Design and Verification; Technical Report, Concordia University, Department of Electrical and Computer Engineering, January 2003. [32 pages]

32. J. Lu and S. Tahar: Modeling and Verification of the Fairisle ATM Null Port Controller in VIS; Technical Report, Concordia University, Department of Electrical and Computer Engineering, March 2003. [16 pages]

33. B. Akbarpour and S. Tahar: Formalization of Fixed-Point Arithmetic in HOL, Technical Report, Concordia University, Department of Electrical and Computer Engineering, September 2002.

34. J. Lu and S. Tahar: Model Checking of the RCMP-800 Input FIFO in VIS; Technical Report, Concordia University, Department of Electrical and Computer Engineering, February 2002. [10 pages]

35. A. Habibi, S. Tahar, and A. Ghazel: Formal Verification of the ADSP-2100 Processor Using the HOL Theorem Prover; Technical Report, Concordia University, Department of Electrical and Computer Engineering, March 2002. [28 pages] 

36. A.T. Abdel-Hamid, S. Tahar, and J. Harrison: Hierarchical Verification of the Implementation of the IEEE-754 Table-Driven Floating-Point Exponential Function using HOL; Technical Report, Concordia University, Department of Electrical and Computer Engineering, April 2001. [19 pages]

37. H. Peng, Y. Mokhtari and S. Tahar: Improving Cone of Influence Reduction; Technical Report, Concordia University, Department of Electrical and  Computer Engineering, April 2001. [12 pages]

38. J. Lu and S. Tahar: Design and Verification of a Knockout ATM Concentrator; Technical Report, Concordia University, Department of Electrical and Computer Engineering, Feb 2001. [10 pages]

39. M. Shirazipour, Y. Mokhtari, and S. Tahar: Model Checking and Refinement of ASM Models Using SMV; Technical Report, Concordia University, Department of Electrical and  ComputerEngineering,January 2001. [17 pages]

40. M. Hasan and S. Tahar:   On the Modeling and Verification of a Telecom System Block Using MDGs;Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2000. [33 pages]

41. L. Barakatain, S. Tahar, Jean-Marc Gendreau and Jean Lamarche: Model Checking of the Transmit Master/Receive Slave (TMRS) using FormalCheck; Technical Report, Concordia University, Department of Electrical and Computer Engineering, October 1999. [17 pages]

42. M. Hasan, S. Tahar, and P. Curzon: Impact of Design Changes on Verification using MDG; Technical Report, Concordia University, Department of Electrical and Computer Engineering, October 1999. [15 pages]

43. V.K. Pisini, S. Tahar, P. Curzon, O. Ait-Mohamed, and X. Song : Integration of HOL and MDG for Hardware Verification; Technical Report, Concordia University, Department of Electrical and Computer Engineering, November 1999. [20 pages]

44. A. A. Mir, S. Balakrishnan, and S. Tahar: Model and Verification of an Embedded System using Cadence SMV; Technical Report, Concordia University, Department of Electrical and Computer Engineering, September 1999. [14 pages]

45. J. Lu and S. Tahar: Modeling and Verification of the Fairisle ATM Null Port Controller in VIS; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 1999. [18 pages]

46. J. Lu and S. Tahar: Model Checking of the RCMP-800 Input FIFO in VIS; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 1999. [9 pages]

47. L. Barakatain and S. Tahar: Model Checking of the Fairisle ATM Switch Fabric using FormalCheck; Technical Report, Concordia University, Department of Electrical and Computer Engineering, September 1999. [11 pages]

48. P. Curzon, S. Tahar, and J. Lu: Comparing HOL, MDG and VIS: A Case Study on the Verification of an ATM Switch Fabric; Technical Report CS-99-05, School of Computing Science Technical Report Series, July 1999. (ISSN 1462-0871) [39 pages]

49. H. Peng and S. Tahar: Formal Verification of an Asynchronous MAC Layer Protocol in VIS; Technical Report, Concordia University, Department of Electrical and Computer Engineering, June 1999. [14 pages]

50. H. Peng, S. Tahar and F. Khendek: Comparison of SPIN and VIS for Protocol Verification; Technical Report, Concordia University, Department of Electrical and Computer Engineering, May 1999. [15 pages]

51. H. Peng and S. Tahar: Compositional Verification of an ATM Bit Error Rate Monitor Circuit; Technical Report, Concordia University, Department of Electrical and Computer Engineering, March 1999. [23 pages]

52. H. Peng and S. Tahar: A Survey on Compositional Verification; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 1998. [17 pages]

53. H. T. Bui, B. Khalaf and S. Tahar: Table-Driven Floating-Point Exponential Function; Technical Report, Concordia University, Department of Electrical and Computer Engineering, September 1998. [19 pages]

54. M. Palanisamy and S. Tahar: Functional Verification of the RCMP Egress Routing Logic; Technical Report, Concordia University, Department of Electrical and Computer Engineering, September 1998. [14 pages]

55. J. Lu, D. Voicu, S. Tahar, and X. Song: Model Checking of the Fairisle ATM Switch; Technical Report, Concordia University, Department of Electrical and Computer Engineering, June 1998. [22 pages]

56. S. Balakrishnan and S. Tahar: On the Formal Verification of Embedded Software Using Multiway Decision Graphs. Technical Report No. 402, Concordia University, Department of Electrical and Computer Engineering, December 1997. [14 pages]

57. S. Tahar, X. Song, E. Cerny, Z. Zhou and M. Langevin: Modeling and Automatic Verification of the Fairisle ATM Switch Fabric using MDGs; Technical Report No. IRO-1101, IRO Department, University of Montreal, Montreal, Quebec, Canada, December 1997. [33 pages]

58. J. Lu and S. Tahar: On the Formal Verification and Reimplementation of an ATM Switch Fabric Using VIS; Technical Report No. 401, Concordia University, Department of Electrical and Computer Engineering, September 1997. [19 pages]

59. Z. Zhou, X. Song, S. Tahar, M. Langevin and E. Cerny: Formal Verification of the Island Tunnel Controller using Multiway Decision Graphs; Technical Report No. IRO-1042, IRO Department, University of Montreal, Montreal, Quebec, Canada, July 1996. [20 pages]

60. M. Langevin, S. Tahar, Z. Zhou, X. Song and E. Cerny: Behavioral Verification of an ATM Switch Fabric using Implicit Abstract State Enumeration; Technical Report No. IRO-1021, IRO Department, University of Montreal, Montreal, Quebec, Canada, March 1996. [14 pages]