Publications







Books
Book Chapters
Journal Papers
Conference Papers
Techinical Reports



Books

[1] Osman Hasan and Sofiène Tahar: Probabilistic Analysis using Theorem Proving; VDM Verlag, 2008. (ISBN: 3-639-09472-7) [164 pages] URL URL

[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


Conference Proceedings Papers

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


Technical Reports

[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

You are visitor #
Last Modified on