Technical Reports:

  1. H. El-Derhalli, L. Constans, S. Le Beux, A. De Rossi, F. Raineri and S. Tahar: Optical Stochastic Computing Architectures Using Photonic Crystal Nanocavities; Technical Report, Department of Electrical and Computer Engineering, Concordia University, February 2021. [34 Pages]. {Computing Research Repository (CoRR), Computer Science, Emerging Technologies, arXiv:2102.02064} [arxiv]}
  2. M. Abdelghany, and S. Tahar: Formal FT-based Cause-Consequence Reliability Analysis using Theorem Proving; Technical Report, Department of Electrical and Computer Engineering, Concordia University, January 2021. [41 Pages]. {Formal Languages and Automata Theory, arXiv.2101.07174 [arxiv]}
  3. M. Abdelghany, W. Ahmad, and S. Tahar: ETMA: A New Software for Event Tree Analysis with Application to Power Protection; Technical Report, Department of Electrical and Computer Engineering, Concordia University, June 2020. [21 Pages]. {Computing Research Repository (CoRR), Electrical Engineering and Systems Science, Signal Processing, arXiv:2006.12383} [arxiv]}
  4. M. Abdelghany, W. Ahmad, and S. Tahar: A Formally Verified HOL4 Algebra for Event Trees; Technical Report, Department of Electrical and Computer Engineering, Concordia University, April 2020. [17 Pages]. {Computing Research Repository (CoRR), Electrical Engineering and Systems Science, Systems and Control, arXiv.2004.14384} [arxiv]}
  5. M. Masadeh, O. Hasan and S. Tahar: Machine Learning-Based Self-Compensating Approximate Computing; Technical Report, Department of Electrical and Computer Engineering, Concordia University, January 2020. [6 Pages]. {Computing Research Repository (CoRR), Electrical Engineering and Systems Science, Signal Processing, arXiv.1908.01343} [arxiv]}
  6. Y. Elderhalli, O. Hasan, and S. Tahar: Dynamic Dependability Analysis of Shuffle-exchange Networks using HOL Theorem Proving; Technical Report, Department of Electrical and Computer Engineering, Concordia University, October 2019. [34 Pages]. {Computing Research Repository (CoRR), Computer Science, Emerging Technologies, arXiv.1910.11203 [arxiv]}
  7. Y. Elderhalli, O. Hasan, and S. Tahar: Integrating DFT and DRBD Formalizations in HOL4; Technical Report, Department of Electrical and Computer Engineering, Concordia University, October 2019. [13 Pages]. {Computing Research Repository (CoRR), Computer Science, Emerging Technologies, arXiv.1910.08875 [arxiv]}
  8. M. Masadeh, O. Hasan and S. Tahar: Error Analysis of Approximate Array Multipliers; Technical Report, Department of Electrical and Computer Engineering, Concordia University, August 2019. [14 Pages]. {Computing Research Repository (CoRR), Computer Science, Emerging Technologies, arXiv.1908.01343 [arxiv]}
  9. Y. Elderhalli, O. Hasan, and S. Tahar: A Formally Verified Algebraic Approach for Dynamic Reliability Block Diagrams [web page]; Technical Report, Department of Electrical and Computer Engineering, Concordia University, August 2019. [25 Pages]. {Computing Research Repository (CoRR), Computer Science, Logic in Computer Science, arXiv.1908.01930 [arxiv]}
  10. W. Ahmed, S.A. Murtza, O. Hasan, S. Tahar: On the Formalization of Importance Measures using HOL Theorem Proving; Computing Research Repository (CoRR), Computer Science, Formal Languages and Automata Theory, arXiv.1904.01605, April 2019, pp. 1-10. [arxiv]}
  11. Y. Elderhalli, W. Ahmad, O. Hasan, and S. Tahar: Formal Probabilistic Analysis of Dynamic Fault Trees in HOL4 [web page]; Technical Report, Department of Electrical and Computer Engineering, Concordia University, July 2018. [32 Pages]. {Computing Research Repository (CoRR), Computer Science, Logic in Computer Science, arXiv.1807.11576 [arxiv]}
  12. M. Masadeh, O. Hasan and S. Tahar: Comparative Study of Approximate Multipliers; Technical Report, Department of Electrical and Computer Engineering, Concordia University, March 2018. [23 Pages]. {Computing Research Repository (CoRR), Computer Science, Emerging Technologies, arXiv.1803.06587 [arxiv]}
  13. I. Seghaier, S. Tahar Intertwined Global Optimization based Reachability Analysis of Analog and Mixed Signal Designs. Technical report, Department of Electrical and Computer Engineering, Concordia University, January 2018. [23 Pages].
  14. Y. Elderhalli, O. Hasan, W. Ahmad and S. Tahar: Formal Dynamic Fault Trees Analysis Using an Integration of Theorem Proving and Model Checking.Technical Report, Department of Electrical and Computer Engineering, Concordia University, December 2017. [32 Pages].]. {Computing Research Repository (CoRR), Computer Science, Logic in Computer Science, arXiv:1712.02872 [arxiv]}
  15. L. Liu, O. Hasan, and S. Tahar, Formalization of Birth-Death and IID Processes in Higher-order Logic.Technical Report, Department of Electrical and Computer Engineering, Concordia University, November 2016. [35 Pages].
  16. S. M. Beillahi, M. Y. Mahmoud, and S. Tahar Optical Quantum Gates Formalization in HOL Light. Technical report, ECE Department, Concordia University, Montreal, QC, Canada, February 2016. [35 Pages].
  17. M. Soualhia, F. Khomh, and S. Tahar ATLAS: An Adaptive Failure-Aware Scheduler for Hadoop. Technical Report, Department of Electrical and Computer Engineering, Concordia University, November 2015. [24 Pages].{Computing Research Repository (CoRR), Computer Science, Distributed, Parallel, and Cluster Computing, arXiv:1511.01446 [arxiv]}
  18. M. Soualhia, F. Khomh, and S. Tahar Predicting Scheduling Failures in the Cloud. Technical Report, Department of Electrical and Computer Engineering, Concordia University, July 2015. [26 Pages]. {Computing Research Repository (CoRR), Computer Science, Distributed, Parallel, and Cluster Computing, arXiv:1507.03562 [arxiv]}
  19. U. Siddique and S. Tahar Stability Verification of Optical and Laser Resonators in HOL Light. Technical Report, Department of Electrical and Computer Engineering, Concordia University, November 2014. [12 Pages].
  20. S. M. Beillahi, U. Siddique and S. Tahar On the Formalization of Signal-Flow-Graph in HOL. Technical Report, Department of Electrical and Computer Engineering, Concordia University, November 2014. [24 Pages].
  21. J. G. Mani Paret and O. Ait Mohamed Generation of Evenly Distributed Input Stimuli by Domain Clustering. Technical Report, Department of Electrical and Computer Engineering, Concordia University, September 2014. [13 Pages].
  22. S. K. Afshar, V. Aravantinos, O. Hasan, and S. Tahar, A Toolbox for Complex Linear Algebra in HOL Light. Technical Report, Department of Electrical and Computer Engineering, Concordia University, May 2014. [14 Pages].
  23. S. K. Afshar, V. Aravantinos, O. Hasan, and S. Tahar: Formalization of Complex Vectors in Higher-Order Logic Technical Report, Department of Electrical and Computer Engineering, Concordia University, May 2014. [15 Pages]. {Computing Research Repository (CoRR), Computer Science, Logic in Computer Science , arXiv:1405.4034 [arxiv]}
  24. S. K. Afshar, U. Siddique, M.Y. Mahmoud, V. Aravantinos, O. Seddiki, O. Hasan, and S. Tahar: Formal Analysis of Optical SystemsTechnical Report, Department of Electrical and Computer Engineering, Concordia University, March 2014. [35 Pages]. {Computing Research Repository (CoRR), Computer Science, Logic in Computer Science, arXiv:1403.3039 arxiv]}
  25. L. Liu, O. Hasan, and S. Tahar, On the Formalization of Continuous-Time Markov Chain in HOL, Technical Report, Department of Electrical and Computer Engineering, Concordia University, April 2013. [12 Pages]
  26. N. Abbasi, O. Hasan, and S. Tahar, Formal Analysis of Soft Errors using Theorem Proving. Technical Report, Department of Electrical and Computer Engineering, Concordia University, March 2012. [21 Pages].
  27. R. Narayanan, A. Daghar, M. Zaki, and S. Tahar, Using LCSS Algorithm for Circuit Level Verification of Analog Designs. Technical Report, Department of Electrical and Computer Engineering, Concordia University, February 2012. [16 Pages].
  28. A. Souari, A. Ghawanmeh, and S.Tahar, Formal Error Analysis and Verification of the Frequency Domain Equalizer. Technical Report, Department of Electrical and Computer Engineering, Concordia University, February 2012. [26 Pages].
  29. G. Helali, O. Hasan, and S.Tahar, Formalization of the Heavy Hitter Problem in HOL. Technical Report, Department of Electrical and Computer Engineering, Concordia University, February 2012. [21 Pages].
  30. J. G. Mani Paret, and O. Ait Mohamed, Performance Analysis of Constraint Solvers. Technical Report, Department of Electrical and Computer Engineering, Concordia University, January 2012. [10 Pages].
  31. O. Lahiouel, H. Aridhi, M.H.Zaki, and S.Tahar, Tool for Modeling and Analysis of Electronic Circuits and Systems. Technical Report, Department of Electrical and Computer Engineering, Concordia University, October 2011. [21 Pages].
  32. L. Liu, O. Hasan, and S. Tahar, Formalization of Discrete-Time Markov Chain in HOL, Technical Report, Department of Electrical and Computer Engineering, Concordia University, April 2011. [15 Pages]
  33. M. Elleuch, O. Hasan, S. Tahar and M. Abid Formal Analysis of a Scheduling Algorithm for Wireless Sensor Networks. Technical Report, Department of Electrical and Computer Engineering, Concordia University, February 2011. [27 Pages].
  34. T. Mhamdi, O. Hasan, and S. Tahar, Formalization of Measure and Lebesgue Integration over Extended Reals in HOL. Technical Report, Department of Electrical and Computer Engineering, Concordia University, January 2011. [120 Pages].
  35. O. Hasan, J. Patel and S. Tahar, Accurate Reliability Analysis of Combinational Circuits using Theorem Proving.Technical Report, Department of Electrical and Computer Engineering, Concordia University, January 2010. [13 Pages].
  36. T. Mhamdi, O. Hasan, and S. Tahar, On the Formalization of the Lebesgue Integration Theory in HOL.Technical Report, Department of Electrical and Computer Engineering, Concordia University, January 2010. [25 Pages].
  37. R. Narayanan, B. Akbarpour, M. H. Zaki, S. Tahar and Lawrence C. Paulson, Automated Formal Verification of Analog/RF Circuits in the Presence of Noise.Technical Report, Department of Electrical and Computer Engineering, Concordia University, June 2009. [14 Pages].
  38. R. Narayanan, M. H. Zaki and S.Tahar, Run-Time Hypothesis Testing of Analog Circuits in Presence of Noise and Process Variations.Technical Report, Department of Electrical and Computer Engineering, Concordia University, June 2009. [21 Pages].
  39. N. Abbasi, R. Narayanan, G. Al Sammane, M. H. Zaki and S. Tahar. Enabling AMS Simulation using Recurrence Notations. Technical Report, Department of Electrical and Computer Engineering, Concordia University, May 2008. [30 Pages].
  40. R. Narayanan, N. Abbasi, M. Zaki, G. Al Sammane, and S. Tahar. On the Simulation Performance of Contemporary AMS Hardware Description Languages. Technical Report, Department of Electrical and Computer Engineering, Concordia University, October 2008. [13 Pages].
  41. Z. J. Dong, M.H. Zaki, G. Al Sammane, S. Tahar and G. Bois. A Run-Time Verfication Approach for AMS Designs. Technical Report, Department of Electrical and Computer Engineering, Concordia University, July 2007. [16 Pages].
  42. 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]
  43. 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].
  44. 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].
  45. Gawanmeh, A. Bouhoula and Sofiene Tahar: Rank Functions based Inference System for Group Key Management Protocols Verification. Technical Report, Concordia University, Department of Electrical and Computer Engineering, March 2007.
  46. 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]
  47. O.Hasan and S. Tahar : Formalization of Continuous Probability Distributions ; Technical Report, Concordia University, Department of Electrical and Computer Engineering, February 2007. [42 pages]
  48. 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]
  49. 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].
  50. A. Gawanmeh and Sofiene Tahar: Rank Theorems for Forward Secrecy in Group Key Management Protocols. Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2006.
  51. A. Gawanmeh and Sofiene Tahar: Formal Specification Requirements for Group Key Management Protocols. Technical Report, Concordia University, Department of Electrical and Computer Engineering, January 2006.
  52. M.H. Zaki, S. Tahar, G. Bois: A Survey on Formal Methods for Analog and Mixed Signal Designs, Technical Report, ECE Dept, Concordia University, 2006 [16 Pages].
  53. 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]
  54. A. Habibi and S. Tahar: AsmL Fixpoint Semantics; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2004. [16 pages]
  55. A. Habibi and S. Tahar: SystemC Fixpoint Semantics; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2004. [16 pages]
  56. 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]
  57. 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]
  58. 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]
  59. 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]
  60. T. Mhamdi, and S. Tahar: Embedding Multiway Decision Graphs in HOL; Technical Report, Concordia University, Department of Electrical andComputer Engineering, February 2004. [20 pages]
  61. H. Peng, Y. Mokhrari, and S. Tahar: Environment Synthesis for Compositional Model Checking; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2003. [?? pages]
  62. 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]
  63. H. Peng, Y. Mokhrari, and S. Tahar: Compositional Verification of an ATM Switch Fabric from Nortel Networks: A Case Study; Technical Report, Concordia University, Department of Electrical and Computer Engineering, October 2003. [?? pages]
  64. A. Gawanmeh, S. Tahar and Kirsten Winter: Formal Verification of ASM Designs using the MDG Tool; Technical Report, Concordia University, Department of Electrical and Computer Engineering, June 2003. [28 pages]
  65. 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]
  66. 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]
  67. 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]
  68. 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]
  69. B. Akbarpour and S. Tahar: Formalization of Fixed-Point Arithmetic in HOL, Technical Report, Concordia University, Department of Electrical and Computer Engineering, September 2002.
  70. 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]
  71. 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]
  72. 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]
  73. H. Peng, Y. Mokhtari and S. Tahar: Improving Cone of Influence Reduction; Technical Report, Concordia University, Department of Electrical and Computer Engineering, April 2001. [12 pages]
  74. J. Lu and S. Tahar: Design and Verification of a Knockout ATM Concentrator; Technical Report, Concordia University, Department of Electrical and Computer Engineering, Feb 2001. [10 pages]
  75. M. Shirazipour, Y. Mokhtari, and S. Tahar: Model Checking and Refinement of ASM Models Using SMV; Technical Report, Concordia University, Department of Electrical and ComputerEngineering,January 2001. [17 pages]
  76. 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]
  77. L. Barakatain, S. Tahar, Jean-Marc Gendreau and Jean Lamarche: Model Checking of the Transmit Master/Receive Slave (TMRS) using FormalCheck; Technical Report, Concordia University, Department of Electrical and Computer Engineering, October 1999. [17 pages]
  78. 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]
  79. V.K. Pisini, S. Tahar, P. Curzon, O. Ait-Mohamed, and X. Song : Integration of HOL and MDG for Hardware Verification; Technical Report, Concordia University, Department of Electrical and Computer Engineering, November 1999. [20 pages]
  80. A. Mir, S. Balakrishnan, and S. Tahar: Model and Verification of an Embedded System using Cadence SMV; Technical Report, Concordia University, Department of Electrical and Computer Engineering, September 1999. [14 pages]
  81. J. Lu and S. Tahar: Modeling and Verification of the Fairisle ATM Null Port Controller in VIS; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 1999. [18 pages]
  82. J. Lu and S. Tahar: Model Checking of the RCMP-800 Input FIFO in VIS; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 1999. [9 pages]
  83. 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]
  84. 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]
  85. 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]
  86. 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]
  87. 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]
  88. H. Peng and S. Tahar: A Survey on Compositional Verification; Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 1998. [17 pages]
  89. H. T. Bui, B. Khalaf and S. Tahar: Table-Driven Floating-Point Exponential Function; Technical Report, Concordia University, Department of Electrical and Computer Engineering, September 1998. [19 pages]
  90. 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]
  91. 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]
  92. 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]
  93. 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]
  94. 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]
  95. 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]
  96. 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]