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)
-
O. Hasan* and S. Tahar: Probabilistic Analysis using Theorem Proving; VDM
Verlag, 2008.(ISBN: 3-639-09472-7) [164 pages]
-
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]
-
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]
-
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]
-
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.
-
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.
-
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.
-
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.
-
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.
-
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.
-
B. Akbarpour*, A. Abdel-Hamid*, S. Tahar and J. Harrison: Verifying a
Synthesized
-
Implementation of the IEEE-754 Floating-Point Exponential Function using
HOL; TheComputer Journal. doi: 10.1093/comjnl/bxp023, 10 April 2009,
pp. 1-24.
-
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.
-
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.
-
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.
-
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.
-
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.
-
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
-
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
-
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, December 2007,
pp.859.881.
-
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.
-
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.
-
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
-
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.
-
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.
-
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.
-
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]
-
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]
-
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]
-
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]
-
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]
-
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]
-
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.
-
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.
-
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
-
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
-
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.
-
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.
-
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.
-
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.