Prof. Sofiène Tahar

Concordia University, Canada

Email: tahar@ece.concordia.ca

Qualifications

1994  Ph.D., University of Karlsruhe, Germany

1990  M.Sc., University of Darmstadt, Germany

1987  B.Sc., University of Darmstadt, Germany

Publications (Selected)

1. O. Hasan* and S. Tahar: Probabilistic Analysis using Theorem Proving; VDM Verlag, 2008.(ISBN: 3-639-09472-7) [164 pages]
2. O. Ait Mohamed, C.A. Munoz, and S. Tahar (Eds.): Theorem Proving in Higher Order Logics;Volume 5170 of Lecture Notes in Computer Science, Springer-Verlag, 2008. (ISBN: 3-540-71065-5) [321 pages]
3. V.A. Carreno, C.A. Munoz, and S. Tahar (Eds.): Theorem Proving in Higher Order Logics;Volume 2410 of Lecture Notes in Computer Science, Springer-Verlag, 2002. (ISBN 3-540-44039-9) [349 pages]
4. S. Tahar: A Methodology for the Formal Verification of RISC Processors; VDI Series 10, No.350, Düsseldorf, VDI-Verlag, 1995 (in German). (ISBN: 3-18-335010-6) [178 pages]
5. E. Cerny, F. Corella, M. Langevin, X. Song, S. Tahar, and Z. Zhou: Automated Verificationwith Abstract State Machines Using Multiway Decision Graphs; In T. Kropf (Ed.), FormalHardware Verification: Methods and Systems in Comparison, Vol. 1287 of Lecture Notes inComputer Science, State-of-the-Art Survey, pp. 79-113, Springer Verlag, 1997.
6. R. Narayanan*, M. Zaki, and S. Tahar: Using Stochastic Differential Equation for Verificationof Noise in Analog/RF Circuits,  Journal of Electronic Testing: Theory and Applications,doi:10.1007/s10836-009-5137-z, 7 January 2010, Springer Verlag, pp. 1-13.
7. O. Hasan*, S. Tahar, and N. Abassi*: Formal Reliability Analysis using Theorem Proving,IEEE Transactions on Computers, doi:10.1109/TC.2009.165, 23 October 2009, pp. 1-14.
8. 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., July2009, pp. 43-58.
9. N. Abdullah*, B. Akbarpour*, and S. Tahar: Error Analysis and Verification of an IEEE 802.11OFDM Modem using Theorem Proving; Electronic Notes in Theoretical Computer Science,Vol. 242, No. 2, Elsevier B.V. Pub., July 2009, pp. 3-30.
10. M. Zaki*, W. Denman*, S. Tahar, and G. Bois: Integrating Abstraction Techniques for theFormal Verification of Analog Designs; Journal of Aerospace Computing, Information, andCommunication, Vol. 6, No. 5, The American Institute of Aeronautics and Astronautics(AIAA), May 2009, pp. 373-392.
11. B. Akbarpour*, A. Abdel-Hamid*, S. Tahar and J. Harrison: Verifying a Synthesized
12. Implementation of the IEEE-754 Floating-Point Exponential Function using HOL;  TheComputer Journal. doi: 10.1093/comjnl/bxp023, 10 April 2009, pp. 1-24.
13. O. Hasan* and S. Tahar: Formal Verification of Tail Distribution Bounds in the HOL TheoremProver; Mathematical Methods in The Applied Sciences, Vol. 32, no. 4, Wiley Interscience,March 2009, pp. 480-504.
14. A. Gawanmeh*, A. Bouhoula, and S. Tahar: Rank Functions based Inference System for GroupKey Management Protocols Verification; International Journal of Network Security, Vol. 8,No. 2, Science Publications, March 2009, pp. 187-198.
15. 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.
16. M. Zaki*, S. Tahar and G. Bois: Formal Verification of Analog and Mixed Signal Designs: ASurvey; Microelectronics Journal, Vol. 39, No. 12, Elsevier B.V. Pub., December 2008, pp.1395-1404.
17. O. Hasan* and S. Tahar: Using Theorem Proving to Verify Expectation and Variance forDiscrete Random Variables,  Journal of Automated Reasoning, Vol. 41, No. 3-4, Springer,November, 2008, pp. 295-323.
18. A. Cui*, C.-H. Chang and S. Tahar: IP Watermarking using Incremental Technology Mappingat Logic Synthesis Level;  IEEE Transactions on CAD of Integrated Circuits and Systems,Volume 27, No. 9, September 2008, pp. 1565-1570
19. A. Gawanmeh*, S. Tahar, and K. Winter: Formal Verification of ASMs using MDGs; Journalof Systems Architecture, Vol. 54, No. 1-2, Elsevier B.V. Pub.,January-February, 2008, pp. 15-34.Page 4
20. A. Gawanmeh*, S. Tahar, H. Moinudeen*, and A. Habibi*: A Design for Verification
21. Approach using an Embedding of PSL in AsmL; Journal of Circuits, Systems, and Computers,Vol. 16, No. 6, World Scientific Publishing, December 2007, pp.859.881.
22. M. Zaki*, S. Tahar, and G. Bois: Qualitative Abstraction based Verification for AnalogCircuits; Revue des Nouvelles Technologies de l'information, Vol. 4, Issue 7, December 2007,RNTI-SM-1, Edition Cepadues, pp. 147-158.
23. 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.
24. O. Hasan* and S. Tahar: Formalization of the Standard Uniform Random Variable; TheoreticalComputer Science, Vol. 382, No. 1, Elsevier B.V. Pub., 2007, pp. 71-83
25. 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, SciencePublications, 2007, pp. 288-298.
26. H. Xiong*, P. Curzon, S. Tahar, and A. Blandford: Providing a Formal Linkage between MDGand HOL; Formal Methods in Systems Design, Vol. 30, No. 2, Springer Verlag, April 2007, pp.83-116.
27. B. Akbarpour* and S. Tahar: Error Analysis of Digital Filters using HOL Theorem Proving;Journal of Applied Logic, Volume 5, Elsevier B.V. Pub., 2007, pp.1-16.
28. S. Tahar, S. Balakrishnan*, and X. Song: Formal Verification of Embedded Systems UsingMultiway Decision Graphs;  International Journal on Multiple Valued Logic, Gordon andBreach Pub. In-Print. [20 pages]
29. O. Ait-Mohamed, X. Song, E. Cerny, S. Tahar, and Z. Zhou: Solving the Non-termination ofAbstract Implicit State Enumeration using a Circuit Transformation;  VLSI Design AnInternational Journal of Custom-Chip Design, Simulation, and Testing, Taylor & FrancisPublishers. In-Print. [23 pages]
30. S. Hasnaoui, M. Hamdi, and S. Tahar: Throughput Performance Analysis of Wireless ControlArea Networks and its Coupling to the Latency Time; Wireless Communications and MobileComputing journal, Wiley Interscience. In-Print [14 pages]
31. A. Samarah*, A. Habibi*, S. Tahar, and N. Kharma: Automated Coverage Directed TestGeneration Using Cell-Based Genetic Algorithm;  IEEE Transactions on Very Large ScaleIntegration Systems. Accepted, 2007. [48 pages]
32. A. Habibi*, H. Moinudeen*, A. Samara*, S. Tahar, D. Li and O. Ait-Mohamed: EfficientSystemC Assertion Based Verification using TLM and Genetic Algorithms; IEEE Trans. onVLSI Systems. Accepted, 2007. [44 pages]
33. J. Ben Hassen* and S. Tahar: Formal Verification of an  SoC Platform Converter usingFormalCheck;  International Journal of Modelling and Simulation, ACTA Press. Accepted,2006. [16 pages]
34. R. Mizouni*, S. Tahar and P. Curzon: Hybrid Verification Incorporating HOL TheoremProving and MDG Model Checking;  Microelectronics Journal, Volume 37, Issue 11,November 2006, pp. 1200-1207, Elsevier B.V. Pub.
35. B. Akbarpour* and S. Tahar: An Approach for the Formal Verification of DSP Designs usingTheorem Proving; IEEE Transactions on CAD of Integrated Circuits and Systems, Vol. 25, No.8, August 2006, pp. 1141-1457.
36. A. Habibi* and S. Tahar: Design and Verification of SystemC Transaction Level Models; IEEETransactions on Very Large Scale Integration Systems, Vol. 14, No. 1, January 2006, pp. 57-68
37. 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, pp. 173-200, Springer
38. A.T. Abdel-Hamid*, S. Tahar, E.M. Aboulhamid: A Survey on IP Watermarking Techniques;Design Automation for Embedded Systems, Vol. 10, 2005, pp. 1-17, Springer Verlag.
39. A. Habibi* and S. Tahar: On the Transformation of SystemC to AsmL using Abstract
40. Interpretation; Electronic Notes in Theoretical Computer Science, Vol. 131, May 2005, pp. 39-49, Elsevier B.V. Pub.
41. O. Ait-Mohamed, X. Song, E. Cerny and S. Tahar: MDG Based State Enumeration byRetiming and Circuit Transformation; Journal of Circuits, Systems and Computers, Vol. 13,No. 5, pp. 1111-1132, October 2004, World Scientific Publishing.
42. S. Tahar, M.H. Zobair*, and X. Song: Formal Verification of a SONET Data Stream Processor;IEE Proceedings Computers and Digital Techniques, Vol. 151, No. 1, February 2004, pp. 1-10.