[1] Osman Hasan and Sofiène Tahar:

[2] Otmane Ait Mohamed, César A. Mu˜noz, and SofièneT ahar (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]
URL

[3] Victor A. Carre˜no, César A. Mu˜noz, and Sofiène 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]
URL

[4] Sofiène Tahar: *Eine Methode zur formalen Verifikation von RISC
Prozessoren * (engl. A Methodology for the Formal Verification
of RISC Processors); VDI Reihe 10, Nr. 350, D’sseldorf, VDI-Verlag,
1995. (ISBN: 3-18-335010-6) [178 pages]
PS File

**
Book Chapters
**

[1] E. Cerny, F. Corella, M. Langevin, X. Song, S. Tahar, and Z. Zhou:
Automated Verification with Abstract State Machines Using Multiway
Decision Graphs; In: T. Kropf (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.
PS File

**
Journal Papers
**

Published/In-Print Papers
-->

[1] O. Hasan, S. Tahar, and N. Abassi:
Formal Reliability Analysis using Theorem Proving;
*IEEE Transactions on Computers*, Vol. 59, No. 5, May 2010, pp. 579-592.

[2] R. Narayanan, M. Zaki, and S. Tahar: Using Stochastic Differential Equation
for Verification of Noise in Analog/RF Circuits;
*Journal of Electronic Testing: Theory and Applications*, Vol. 26, No. 1,
Springer, February 2010, pp. 97-109.

[3] 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.

[4] 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.

[5] M. Zaki, W. Denman, S. Tahar, and G. Bois:
Integrating Abstraction Techniques for the Formal Verification of Analog
Designs; *Journal of Aerospace Computing, Information, and
Communication*, Vol. 6, No. 5, The American Institute of Aeronautics and
Astronautics (AIAA), May 2009, pp. 373-392.

[6] B. Akbarpour, A. Abdel-Hamid, S. Tahar, and J. Harrison:
Verifying a Synthesized Implementation of the IEEE-754 Floating-Point Exponential Function 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. 187-198.

[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*, Volume
27, No. 9, September 2008, pp 1565-1570,

[13] 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.

[14] 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.

[15] 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.

[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] 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, November 2007, pp. 288-298.

[18] O. Hasan ands S. Tahar
Formalization of the Standard Uniform Random Variable;
*Theoretical Computer Science*, Vol. 382, No. 1, Elsevier
B.V. Pub., August 2007, pp. 71-83.

[19] 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.

[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, pp. 173-200, Springer Verlag.

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

[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.
PDF File

[26] 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.

[27] 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, pp. 71-81, January 2004.
PDF File

[28] S. Kort, S. Tahar, and P. Curzon: Hierarchical Formal
Verification Using a Hybrid Tool;
*International Journal on Software
Tools for Technology Transfer*, Vol. 4, No. 3, pp. 313-322,
May 2003, Springer Verlag.
PDF File

[29] 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.
PDF File

[30] 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.
PDF File

[31] 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.
PS File

[32] 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.
PS File

[33] 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.
PS File

[34] 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.
PS File

[35] 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.
PDF File

[36] 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.
PS File

[37] 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.
PS File

[38] 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.
PS File

L. Liu, O. Hasan and S. Tahar: Formalization of Finite-State Discrete-Time Markov Chains in HOL; In: T. Bultan and P.-A. Hsiung (Eds.), Automated Technology for Verification and Analysis, Lecture Notes in Computer Science 6996, Springer Verlag, 2011, pp. 90-104. [Proc. International Symposium on Automated Technology for Verification and Analysis (ATVA'11), Taipei, Taiwan, October 2011]

[0] N. Abbasi, O. Hasan, and S. Tahar:
Formal Lifetime Reliability Analysis Using Continuous Random Variables;
*Logic, Language, Information and Computation (WoLLIC'10)*, Lecture
Notes in Computer Science, Springer Verlag, Brasília, Brazil, July 2010.

[0] T. Mhamdi, O. Hasan, and S. Tahar:
On the Formalization of the Lebesgue Integration Theory in HOL;
*Interactive Theorem Proving (ITP'10)*, Lecture Notes in Computer
Science, Springer Verlag, Edinburgh, UK, June 2010.

[0] R. Narayanan, M. Zaki, B. Akbarpour, S. Tahar, and L. Paulson:
Formal Verification of Analog/RF Circuits in the Presence of Noise and Process Variation;
*Proc. IEEE/ACM Design Automation and Test in Europe (DATE'10)*,
Dresden, Germany, March 2010, pp. 1309-1312.

[0] O. Hasan and S. Tahar:
Formal Probabilistic Analysis: The Higher-Order Logic Based Approach;
In: M. Frappier, U. Glaeser, S. Khurshid, R. Laleau, and S. Reeves (Eds.),
*Abstract Satte Machines, Alloy, B and Z*, Lecture Notes in Computer
Science 5977, Springer Verlag, 2010, pp. 2-19.
[*Proc. International Conference on Abstract Satte Machines, Alloy, B and
Z (ABZ'10)*, Orford, Quebec, Canada, February 2010.]

[0] W. Denman, B. Akbarpour, S. Tahar, M. Zaki, and L. Paulson:
Automated 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.

[1] 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.]

[2] Z. Wang, M. Zaki, and 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.

[3] 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.]

[4] 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.

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

[6] 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.

[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] O. Hasan, N. Abbasi, B. Akbarpour, and S. Tahar:
Formal Probabilistic Analysis using Theorem Proving;
*Proc. 77th ACFAS Symposium (ACFAS'09)*, Ottawa, Canada, May 2009.

[9] M. Zaki, G. Al Sammane, Z.J. Dong, S. Tahar, and G. Bois:
Techniques for the Formal Verification of Analog and Mixed-Signal Designs;
*Proc. 77th ACFAS Symposium (ACFAS'09)*, Ottawa, Canada, May 2009.

[11] 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.

[12] 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.]

[13] 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.

[14] A. Gawanmeh, L. Jemni and S. Tahar:
Event-B based Invariant Checking of Secrecy in Group Key Protocols;
* Proc. IEEE Conference on Local Area Networks (LCN - WNS'08)*, Montreal,
Quebec, Canada, October 2008, IEEE Computer Society Press, pp. 950-957.

[15] Y. Mokhtari, O. Ait Mohamed, S. Abed, 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.]

[16] 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.

[7] 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.

[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] 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.

[20] 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.

[21] 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.

[22] 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. 1-12.

[23] T.H. Khan, S. Tahar, O. Ait Mohamed, and A. Habibi:
Automatic Generation of SystemC Transactors from Graphical FSM;
*Proc. IEEE International Conference on Microelectronics
(ICM'07)*, Cairo, Egypt, December 2007, pp. 271-274.

[24] 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.

[25] 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.

[26] 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 Volume 936, 2007, pp. 259-262. [Proc. *International
Conference of Numerical Analysis and Applied Mathematics (ICNAAM'07)*,
Corfu, Greece, September 2007.]

[27] 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.

[28] 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.

[29] 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.]

[30] 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.]

[31] 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.]

[32] 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.

[33] 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 (MDSCAS'07)*,
Montreal, Quebec, Canada, August 2007, pp. 726-729.

[34] 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]

[35] 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.

[36] 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.

[37] 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.

[38] 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.

[39] 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.

[40] 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.

[41] 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.

[42] 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.

[43] 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.

[44] 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.

[45] 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.

[46] 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.

[47] 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.

[48] A. Habibi, H. Moinudeen, A. Samara, and 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.

[49] A. Habibi, S. Tahar, A. Samara, D. Li, and 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.

[50] 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.

[51] 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.

[52] 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.

[53] 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]

[54] 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.

[55] 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.

[56] 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.

[57] 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.

[58] 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.

[59] 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.

[60] 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.

[61] 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.

[62] A.T. 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.

[63] 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.

[64] 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.

[65] 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.

[66] 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.

[67] 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]

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

[69] 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]
PDF File

[70] 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]
PDF File

[71] B. Akbarpour and S. Tahar:
Error Analysis of Digital Filters using Theorem Proving;
In: K. Slind, A. Bunker 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]

[72] 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

[73] 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.

[74] 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.

[75] 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.

[76] 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.

[77] 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.
PDF File

[78] 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.
PDF File

[79] A.T. 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.
PDF File

[80] 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.
PDF File

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

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

[83] 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.]
PS File

[84] 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.
PDF File

[85] 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.
PS File

[86] 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.]
PS File

[87] 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.
PS File

[88] 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.
PDF File

[89] 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.
PDF File

[90] 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.
PDF File

[91] 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.
PDF File

[92] 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.
PDF File

[93] 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.
PDF File

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

[95] 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.
PS File

[96] 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.]
PS File

[97] F. Charfi, L. Jemni, S. Ben Ahmed, and S. Tahar:
An Approach Translating CoD Specification to be Checked by UPPAAL;
*Proc. 3è Journée Scientifiques des Jeunes Chercheurs en Génie Electrique et
Informatique (GEI'03)*, Mahdia, Tunisia, March 2003, pp 54-59.
PDF File

[98] 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.]
PS File

[99] M.H. Zobair and S. Tahar:
Formal Verification of a SONET Telecom System Block;
In: C. George and H. Miao (Eds.),
*Formal Methods in Software Engineering*,
Lecture Notes in Computer Science 2495, Springer Verlag, 2002,
pp. 447-458.
[*Proc. International Conference on Formal Engineering Methods
(ICFEM'02)*, Shanghai, China, October 2002.]
PS File

[100] 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.
PS File

[101] 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.
PDF File

[102] 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.]
PS File

[103] 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.]
PS File

[104] A. Habibi, S. Tahar, and A. Ghazel:
Formal Modeling 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.
PDF File

[105] F. Wang and S. Tahar:
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.
PDF File

[106] 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.
PDF File

[107] 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.
PDF File

[108] 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.
PDF File

[109] 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.
PS File

[110] 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.
PDF File

[111] L. Barakatain, S. Tahar, J. Lamarche, and J.-M. Gendreau:
Functional Verification of a SCI-PHY Level 2 Protocol Engine;
*Proc. IEEE International Conference on Information, Communications
& Signal Processing (ICICS'01)*, Singapore, October 2001.
PDF File

[112] H. Peng, 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.
PS File

[113] S. Kort, S. Tahar, and P. Curzon: Hierarchical Verification Using
an MDG-HOL Hybrid Tool; In: T. Margaria and T. Melham (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'01)*, Livingston,
Scotland, UK, September 2001.]
PS File

[114] 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.]
PDF File

[115] 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.]
PDF File

[116] L. Barakatain, S. Tahar, J. Lamarche and J-M. Gendreau:
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.
PDF File

[117] 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.
PDF File

[118] 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.
PDF File

[119] 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.
PS File

[120] H. Peng 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.
PDF File

[121] H. Peng, 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'00)*, York, UK, September 2000, IEEE Computer
Society Press, pp. 79-87.
PS File

[122] 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'00)*, Portland, Oregon, USA,
August 2000, pp. 237-248.
In: M. Aagard, J. Harrison, and T. Shubert (Eds.)
[*TPHOLs 2000 Supplemental Proceedings*,
Technical Reprot CSE-00-009, Oregon Graduate Institute,
Portland, Oregon, USA, August 2000.]
PS File

[123] 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'00)*, Trois-Rivières, Québec,
Canada, August 2000, IEEE Computer Society Press, pp. 237-241.
PDF File

[124] J.F. Weng, G.Q. Xue, T. Le-Ngoc, and S. Tahar:
Analysis of Multilevel Quantized Soft-Limiting Detector for an FH-SSMA
System;
*Proc. IEEE International Conference on Communications (ICC'00)*,
New Orleans, Louisiana, USA, June 2000, Vol. 3, pp. 1380-1384.
PDF File

[125] T. Elshabrawy, T. Le-Ngoc, and S. Tahar:
Two-way Broadband Satellite Access for Interactive Multimedia
Services;
*Proc. IEEE International Conference on Telecommunications
(ICT'00)*, Acapulco, Mexico, May 2000.
PDF File

[126] 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.
PDF File

[127] 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.
PDF File

[128] S. Kort, S. Tahar, P. Curzon, X. Song:
HOL-MDG: A Hybrid Tool for Formal Verification;
*Proc. 2000 Micronet Annual Workshop*, Ottawa, Canada, April
2000, pp. 131-132.
PDF File

[129] 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.
PS File

[130] S. Balakrishnan and S. Tahar:
Une approche hiérarchique à la vérification formelle des systèmes embarqué
en utilisant MDGs;
*Proc. 68th ACFAS Symposium (ACFAS'00)*, Montreal, Canada, May 2000.

[131] S. Kort, V.K. Pisini, S. Tahar, O. Ait-Mohamed, P. Curzon and X. Song:
Un outil hybride pour la vérification formelle de circuits;
*Proc. 68th ACFAS Symposium (ACFAS'00)*, Montreal, Canada, May 2000.

[132] M. Azizi, E.-M. Aboulhamid, and S. Tahar:
Entre la covérification concurrente et l'ordonnancement des threads;
*Proc. 68th ACFAS Symposium (ACFAS'00)*, Montreal, Canada, May 2000.

[133] M. Kharroubi, E.-M. Aboulhamid, and S. Tahar:
Protection de la propriété intellectuelle des implémentations des
fonctions séquentielle;
*Proc. 68th ACFAS Symposium (ACFAS'00)*, Montreal, Canada, May 2000.

[134] H. Peng and S. Tahar:
Compositional Verification of IP Based Designs;
*Proc. IFIP International Workshop on IP Based Synthesis
and System Design*, Grenoble, France, December 1999,
pp. 189-193.
PS File

[135] 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.
PS File

[136] H. Xiong, P. Curzon, and S. Tahar:
Importing MDG Results into HOL;
In: Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and
L. Theryvon (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.]
PS File

[137] M. Azizi, E.-M. Aboulhamid, and S. Tahar:
Properties Coverification for HW/SW Systems;
*Proc. IEEE International Conference of Electronic Circuits
and Systems Conference (ECS'99)*, Bratislava, Slovakia,
September 1999, pp. 81-84.
PDF File

[138] G.Q. Xue, J.F. Weng, T. Le-Ngoc, and S. Tahar:
Impact of Imperfect Power Control on the Performance of Multiuser
Detectors;
*Proc. IEEE Global Telecommunications Conference (GLOBECOM99)*,
Rio de Janeiro, Brazil, December 1999, pp. 138-142.
PDF File

[139] J.F. Weng, G.Q. Xue, T. Le-Ngoc, and S. Tahar:
Blind Adaptive Minimum Output Energy Rake Receiver for DS/CDMA
over Multipath Fading Channels;
*Proc. IEEE 1999 Vehicular Technology Conference (VTC'99)*,
Amsterdam, The Netherlands, September 1999, pp. 208-212.
PS File

[140] G.Q. Xue, J.F. Weng, T. Le-Ngoc, and S. Tahar:
An Analytical Model for Performance Evaluation of Multistage
Parallel Interference Cancellation Detectors in CDMA Systems;
*Proc. IEEE 1999 Vehicular Technology Conference (VTC'99)*,
Amsterdam, The Netherlands, September 1999, pp. 1144-1149.
PS File

[141] M. Azizi, E.-M. Aboulhamid, and S. Tahar:
Multithreading-Based Coverification 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 1999.
PDF File

[142] J.F. Weng, G.Q. Xue, T. Le-Ngoc, and S. Tahar:
Combined Multistage Interference Cancellation and Multipath
Decorrelating Techniques for Asynchronous QPSK/DS/CDMA over
Multipath Rayleigh Fading Channels;
*Proc. IEEE International Conference on Telecommunications
(ICT'99)*, Cheju, Korea, June 1999, Vol. 1, pp. 103-107.
PS File

[143] 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;
*Proc. IEEE International Conference on Communications (ICC'99)*,
Vancouver, Canada, June 1999, Vol. 1, pp. 78-82.
PDF File

[144] G.Q. Xue, J.F. Weng, T. Le-Ngoc, and S. Tahar:
Adaptive Multistage Parallel Interference Cancellation for CDMA;
*Proc. IEEE International Conference on Communications (ICC'99)*,
Vancouver, Canada, June 1999, Vol. 2, pp. 917-921.
PDF File

[145] J.F. Weng, G.Q. Xue, T. Le-Ngoc, and S. Tahar:
Multistage Interference Cancellation with Multipath Decorrelating
for Asynchronous QPSK DS/CDMA Systems;
*Proc. IEEE 1999 Vehicular Technology Conference (VTC'99)*,
Houston, Texas, USA, May 1999, Vol. 3, pp. 2240-2244.
PDF File

[146] G.Q. Xue, J.F. Weng, T. Le-Ngoc, and S. Tahar:
Adaptive Multistage Parallel Interference Cancellation for CDMA
over Multipath Fading Channels;
*Proc. IEEE 1999 Vehicular Technology Conference (VTC'99)*,
Houston, Texas, USA, May 1999, Vol. 2, pp. 1251-1255.
PDF File

[147] 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)*, Edmonton, Alberta, Canada, May 1999,
pp. 450-455.
PDF File

[148] M. Palanisamy and S. Tahar:
RTL Modeling of the RCMP Egress Routing Logic;
*Proc. IEEE Canadian Conference on Electrical & Computer
Engineering (CCECE'99)*, Edmonton, Alberta, Canada, May 1999,
pp. 111-115.
PDF File
PS File

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

[150] 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.
PS File

[151] 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. PS File

[152] 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.
PS File

[153] S. Tahar, P. Curzon, and J. Lu:
Three Approaches to Hardware Verification: HOL, MDG and
VIS Compared;
In: G. Gopalakrishnan and P. Windley (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.]
PS File

[154] 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.
PS File

[155] P. Curzon, S. Tahar, and O. Ait-Mohamed:
Verification of the MDG Components Library in HOL;
*B-Track Proc. International Conference on Theorem Proving
in Higher-Order Logics (TPHOLs'98)*, Canberra, Australia,
September 1998, pp. 31-45.
[In: J. Grundy and M. Newey (Eds.), *Theorem Proving in Higher
Order Logics: Emerging Trends*, ANU Computer Science Technical Reports
TR-CS-98-08, The Australian National University, September 1998.]
PS File

[156] 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.
PS File

[157] Z. Zhou, X. Song, S. Tahar, E. Cerny, F. Corella and M. Langevin:
Verification of the Island Tunnel Controller using Multiway
Decision Graphs; In: M. Srivas and A. Camilleri (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.]
PS File

[158] 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.
PS File

[159] S. Tahar and P. Curzon: A Comparison of MDG and HOL for Hardware
Verification;
In: J. von Wright, J. Grundy, and J. Harrison (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.]
PS File

[160] Z. Zhou, X. Song, F. Corella, M. Langevin, E. Cerny and S. Tahar:
MDG Tools for the Verification of RTL Designs;
In: R. Alur and T. Henzinger (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.]
PS File

[161] 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.
PS File

[162] 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.
PS File

[163] S. Tahar and R. Kumar: Implementational Issues for Verifying RISC-
Pipeline Conflicts in HOL (Higher Order Logic);
In: T. Melham and J. Camilleri (Eds.), * Higher Order Logic
Theorem Proving and Its Applications*, Lecture Notes in
Computer Science 854, Springer Verlag, 1994, pp. 424-439.
[*Proc. International Conference on Higher Order Logic Theorem
Proving and Its Applications (HUG'94)*, Valletta, Malta,
September 1994.]
PS File

[164] S. Tahar and R. Kumar: Formal Verification of Pipeline Conflicts
in RISC Processors;
* Proc. European Design Automation Conference (EURO-DAC'94)*,
Grenoble, France, September 1994, IEEE Computer Society
Press, pp. 285-289.
PS File

[165] S. Tahar and R. Kumar: Implementing a Methodology for Formally
Verifying RISC Processors in HOL (Higher Order Logic);
In: J. Joyce and C. Seger (Eds.), *Higher Order Logic Theorem
Proving and Its Applications*, Lecture Notes in Computer
Science 780, Springer Verlag, 1994, pp. 281-294.
[*Proc. International Conference on Higher Order Logic Theorem
Proving and Its Applications (HUG'93)*, Vancouver, Canada,
August 1993.]
PS File

[166] S. Tahar and R. Kumar: Towards a Methodology for the Formal
Hierarchical Verification of RISC Processors;
*Proc. IEEE International Conference on Computer Design
(ICCD'93)*, Cambridge, Massachusetts, USA, October 1993,
IEEE Computer Society Press, pp. 58-62.
PS File

[167] S. Tahar and R. Kumar: A Formalization of a Hierarchical Model for
RISC Processors;
In: P. Spies (Ed.), *Proc. European Informatics Congress
Computing Systems Architecture (Euro-ARCH'93)*, Munich,
Germany, October 1993, Informatik Aktuell, Springer Verlag,
pp. 591-602.
PS File

[168] S. Tahar and R. Kumar: Ein hierarchisches modell zur formalen
Verifikation von RISC-Prozessoren (engl. A Hierarchical Model
for the formal Verification of RISC Processors);
In: T. Kropf, R. Kumar, and D. Schmid(Eds.), *Proc. GI/ITG-
Workshop Formale Methoden zum Entwurf korrekter Systeme*,
Bad-Herrenalb, Germany, March 1993, pp. 35-40.
PS File

[0] O. Ait Mohamed, C.A. Munoz, and S. Tahar (Eds.): Theorem Proving in Higher Order Logics: Emerging Trends; Technical Report 2008-1-Ait Mohamed, Concordia University, Montreal, Quebec, Canada, August 2008. [140 pages]

[0] Victor A. Carreno, César A. Munoz, and Sofiène Tahar (Eds.):
*Theorem Proving in Higher Order Logics*;
Technical Report NASA/CP-2002-211736, NASA Langley Research Center,
Hampton, Virginia, August 2002. [189 pages]
PDF File

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

[2] N. Abbasi, R. Narayanan, G. Al Sammane, M. Zaki and S. Tahar: Enabling AMS Simulation using Recurrence Notations; Technical Report, Concordia University, Department of Electrical and Computer Engineering, May 2008. [30 Pages].

[3] 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]

[4] 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]

[5] 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]

[6] 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]

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

[8] 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]

[9] 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]

[11] 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]

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

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

[14] 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] PS File PDF File URL

[15] 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] PS File PDF File URL

[16] 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] PS File PDF File URL

[17] 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] PS File PDF File URL

[18] T. Mhamdi and S. Tahar: Embedding Multiway Decision Graphs in HOL; Technical Report, Concordia University, Department of Electrical and Computer Engineering, February 2004. [20 pages] PS File PDF File URL

[19] R. Mizouni, S. tahar, and P. Curzon: A Hybrid Tool Integrating HOL Theorem Proving with MDG Model Checking; Technical Report, Concordia University, Department of Electrical and Computer Engineering, February 2004. [20 pages] PS File PDF File URL

[20] 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. [20 pages]

[21] 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]
PS File
PDF File
URL

[22] H. Peng, Y. Mokhrari, and S. Tahar:
Environment Synthesis for Compositional Model Checking;
*Technical Report*, Concordia University, Department of Electrical
and Computer Engineering, March 2002. [39 pages]

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

[24] 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] PDF File PS File URL

[25] A.T. Abde-Hamid, S. Tahar and M.E. Aboulhamid:
IP Watermarking Techniques: Survey and Comparison;
*Technical Report*, Concordia University, Department of Electrical
and Computer Engineering, May 2003. [14 pages]
PS File
URL

[26] 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]
PS File
URL

[27] 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]
PDF File
URL

[28] 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]
PDF File
URL

[29] B. Akbarpour and S. Tahar:
Formalization of Fixed-Point Arithmetic in HOL;
*Technical Report*, Concordia University, Department of Electrical
and Computer Engineering, November 2002. [32 pages]
PS File
URL

[30] M. Layouni and S. Tahar: Formal Verification of Cryptographic Protocols: A Survey; Technical Report, Concordia University, Department of Electrical and Computer Engineering, June 2002. [24 pages]

[31] 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]
PDF File

[32] 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]
PDF File

[33] 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]
PS File

[34] H. Peng, Y. Mokhtari and S. Tahar: Syntactic Model Reduction; Technical Report, Concordia University, Department of Electrical and Computer Engineering, April 2001. [39 pages] PS File URL

[35] J. Lu and S. Tahar:
Design and Verification of a Knockout ATM Switch Concentrator;
*Technical Report*, Concordia University, Department of Electrical
and Computer Engineering, February 2001. [10 pages]
PDF File
PS File
URL

[36] M. Shirazipour, Y. Mokhtari, and S. Tahar:
Model Checking and Refinement of ASM Models Using SMV;
*Technical Report*, Concordia University, Department of Electrical
and Computer Engineering, January 2001. [17 pages]
PS File
URL

[37] 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]
PDF File
PS File
URL

[38] 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. [20 pages]
PDF File
PS File
URL

[39] 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]
PDF File
PS File
URL

[40] 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. [21 pages]
PDF File
PS File

[41] 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. [12 pages]
PDF File
PS File
URL

[42] 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]
PDF File
PS File
URL

[43] F. Weng, G. Q. Xue, T. Le-Ngoc, and S. Tahar:
Frequency Hopping CDMA: A Review;
*Technical Report*, Concordia University, Department of Electrical
and Computer Engineering, September 1999. [12 pages]
PS File

[44] 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]
PS File

[45] 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]
PS File
URL

[46] 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]
PS File
URL

[47] 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]
PS File
URL

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

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

[50] Q. Xue, J. F. Weng, T. Le-Ngoc, and S. Tahar:
Multiuser Detection Techniques: An Overview;
*Technical Report*, Concordia University, Department of Electrical
and Computer Engineering, October 1998. [21 pages]
PS File

[51] F. Weng, G. Q. Xue, T. Le-Ngoc, and S. Tahar:
Multistage Interference Cancellation with Diversity Reception for
QPSK Asynchronous DS/CDMA System over Multipath Fading Channels:
Comparison of QPSK and BPSK Spreading Schemes;
*Technical Report*, Concordia University, Department of Electrical
and Computer Engineering, October 1998. [12 pages]
PS File

[52] Q. Xue, J. F. Weng, T. Le-Ngoc, and S. Tahar:
Adaptive Multistage Parallel Interference Cancellation for CDMA;
*Technical Report*, Concordia University, Department of
Electrical and Computer Engineering, September 1998. [33 pages]
PS File

[53] F. Weng, G. Q. Xue, T. Le-Ngoc, and S. Tahar:
Multistage Interference Cancellation with Diversity Reception for
Asynchronous QPSK DS/CDMA system over Multipath Fading Channels;
*Technical Report*, Concordia University, Department of Electrical
and Computer Engineering, September 1998. [44 pages]
PS File

[54] L. Cong, T. Le-Ngoc, and S. Tahar:
Study of CDMA Multimedia Services for Mobile Communications;
*Technical Report*, Concordia University, Department of Electrical
and Computer Engineering, September 1998. [19 pages]
PS File

[55] 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]
PS File
URL

[56] 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]
PS File
URL

[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]
PS File

[58] 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]
PS File
URL

[59] 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]
PS File
URL

[60] 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]
PS File

[61] 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]
PS File

[62] S. Tahar and R. Kumar:
A Practical Methodology for the Formal
Verification of RISC Processors;
*Technical Report No. FZI 9/95*, Forschungszentrum Informatik,
Haid-und-Neu Strasse 10-14, 76131 Karlsruhe, Germany, August 1995.
[49 pages]
PS File

[63] M. Dehof and S. Tahar:
Implementierung des DLX RISC-Prozessors in
einer Standardzellen-Entwurfsumgebung (engl. Implementation of
the DLX RISC Processor in a Standard-Cell Design Environment);
*Technical Report No. SFB 358-C2-1/94*, Institute for Computer
Design and Fault Tolerance, University of Karlsruhe, Germany,
March 1994. [72 pages]
PS File

Department of ECE | Faculty of ECE | Sofiène Tahar |
---|

Last Modified on