Journal Papers:
O. Barhoumi, M. Zaki and S. Tahar: A Formal Approach to Road Safety Assessment Using Traffic Conflict Techniques ; IEEE Open Journal of Vehicular Technology, Vol. 5, April 2024, pp. 606-619.
E. Deniz, A. Rashid, O. Hasan and S. Tahar: Formalization of the Telegrapher’s Equations using Higher-Order-Logic Theorem Proving ; Journal of Applied Logic, Vol. 11, No. 2, March 2024, pp. 243-282.
A. Aoun, M. Masadeh and S. Tahar: Design Space Exploration for Energy-Efficient Approximate Sobel Filter ; International Journal of Electronics and Communications, Elsevier, Vol. 172, 154887, December 2023, pp. 1-9.
M. Abdelghany, W. Ahmad, and S. Tahar: Event Tree Reliability Analysis of Safety Critical Systems using Theorem Proving ; IEEE Systems Journal, Vol. 16, No. 2, June 2022, pp. 2899-2910.
H. El-Derhalli, L. Constans, S. LeBeux, A. De Rossi, F. Raineri and S. Tahar: Towards All-optical Stochastic Computing Using Photonic Crystal Nanocavities ; ACM Journal of Emerging Technologies in Computing Systems, Vol. 18, No. 1, January 2022, pp. 16:1-16:25.
S. Najmeddin, S. Aïssa and S. Tahar: Energy-Efficient Resource Allocation in Multi-UAV Networks with NOMA ; IEEE Transactions on Green Communications and Networking, Vol. 5, No.4, December 2021, pp. 1906-1917.
H. El-Derhalli, S. LeBeux and S. Tahar: Design Space Exploration of Stochastic Computing Architectures Implemented using Integrated Optics ; IEEE Transactions on Emerging Topics in Computing, Vol. 9, No. 4, December 2021, pp 2158-2169.
M. Masadeh, Y. Elderhalli, O. Hasan and S. Tahar: A Quality-Assured Approximate Hardware Accelerators Based on Machine Learning and Dynamic Partial Reconfiguration ; ACM Journal of Emerging Technologies in Computing Systems, Vol. 17, No. 4, October 2021, pp. 57:1-57:19.
M. Masadeh, O. Hasan and S. Tahar: Machine Learning-Based Self-Tunable Design of Approximate Computing ; IEEE Transactions on VLSI, Vol. 29, No. 4, April 2021, pp. 800-813.
M. Abdelghany and S. Tahar: Cause-Consequence Diagram Reliability Analysis using Formal Techniques with Application to Electrical Power Networks ; IEEE Access, Vol. 9, January 2021, pp. 23929-23943.
M. Soualhia, F. Khoms, and S. Tahar: A Dynamic and Failure-aware Task Scheduling Framework for Hadoop ; IEEE Transactions on Cloud Computing, Vol. 8, No. 2, June 2020, pp. 553-569.
I. Seghaier, M.H. Zaki and S. Tahar: Mating Sensitivity Analysis and Statistical Verification for Efficient Yield Estimation ; IEEE Transactions on CAD of Integrated Circuits and Systems, Vol. 39, No. 2, February 2020, pp. 294-307.
M. Masadeh, O. Hasan and S. Tahar: Input-Conscious Approximate Multiply-Accumulate (MAC) Unit for Energy-Efficiency ; IEEE Access, Vol. 7, December 2019, pp. 147129-147142.
Y. Elderhalli, O. Hasan and S. Tahar: A Methodology for the Formal Verification of Dynamic Fault Trees using HOL Theorem Proving ; IEEE Access, Vol. 7, December 2019, pp. 147129-147142.
S.M. Beillahi, M.Y. Mahmoud and S. Tahar: A Modeling and Verification Framework for Optical Quantum Circuits ; Formal Aspects of Computing, Springer, Vol. 31, No. 3, June 2019, pp 321-351.
Y. Elderhalli, W. Ahmad, O. Hasan and S. Tahar: Probabilistic Analysis of Dynamic Fault Trees using HOL Theorem Proving ; Journal of Applied Logic, Vol. 6, No. 3, May 2019, pp. 467-509.
U. Siddique, M.Y. Mahmoud and S. Tahar: Formal Analysis of Discrete-Time Systems using z-Transform ; Journal of Applied Logic, Vol. 5, No. 4, June 2018, pp. 875-906.
W. Ahmed, O. Hasan, S. Tahar, and M.S. Hamdi: Formal Reliability Analysis of Oil and Gas Pipelines ; Journal of Risk and Reliability, SAGE Pub., Vol. 232, No.3, June 2018, pp. 320-334.
M. Elleuch, O. Hasan, S. Tahar and M. Abid: Formal Probabilistic Performance Verification of Randomly-scheduled Wireless Sensor Networks ; International Journal of Critical Computer-Based Systems, Inderscience, Vol. 8 No. 3/4, May 2018, pp. 311-339.
O. Lahiouel, M.H. Zaki and S. Tahar:Accelerated and Reliable Analog Circuits YieldAnalysis using SMT Solving Techniques ; IEEE Transactions on CAD of Integrated Circuits and Systems, Vol. 27, No. 3, March 2018, pp. 517-530.
M. Soualhia, F. Khomh, and S. Tahar:Task Scheduling in Big Data Platforms: A Systematic Literature Review ; Journal of Systems and Software, Elsevier, Vol. 134, December 2017, pp. 170-189.
O. Lahiouel, H. Aridhi, M.H. Zaki and S. Tahar:Exploiting Bounds Optimization for the Semi-formal Verification of Analog Circuits ; Integration, the VLSI Journal, Elsevier, Vol. 59, No. 4, September 2017, pp. 135-147
U. Siddique and S. Tahar:Formal Verification of Stability and Chaos in Periodic Optical Systems ; Journal of Computer and System Sciences, Elsevier, Vol. 88, September 2017, pp. 271-289.
A. Rashid, U. Siddique, O. Hasan and S. Tahar:Formal Reasoning about Systems Biology using Theorem Proving ; PLoS ONE, Vol. 12, No. 7, July 2017,pp. 1-27.
M. Nayrolles, A. Hamou-Lhadj, S. Tahar and A. Larsson:A Bug Reproduction Approach Based on Directed Model Checking and Crash Traces ;Journal of Software: Evolution and Process, Willey, Vol. 29, No. 3, March 2017, pp. 1-24.
M. Layouni, M.S. Hamdi and S. Tahar:Detection and Sizing of Metal-loss Defects in Oil and Gas Pipelines using Pattern-adapted Wavelets and Machine Learning ; Applied Soft Computing, Elsevier, Vol. 52, March 2017, pp. 247-261.
W. Ahmed, O. Hasan and S. Tahar:Formalization of Reliability Block Diagrams in Higher-order Logic ; Journal of Applied Logic, Elsevier, Volume 18, November 2016, pp. 19-41.
U. Siddique and S. Tahar:On the Formal Analysis of Gaussian Optical Systems in HOL ; Formal Aspects of Computing, Springer, Vol. 28, No. 5, September 2016, pp 881-907.
H. Aridhi, M.H. Zaki, and S. Tahar:Enhancing Model Order Reduction for Nonlinear Analog Circuit Simulation ; IEEE Transactions on VLSI, Vol. 24, No. 3, March 2016, pp. 1036-1049.
T.L. Ben Cheikh, A. Aguiar, S. Tahar, G. Nicolescu:Tuning Framework for Stencil Computation in Heterogeneous Parallel Platforms ; The Journal of Supercomputing, Springer, Vol. 72, No. 2, Springer, February 2016, pp 468-502.
T. Mhamdi, O. Hasan, and S. Tahar:Evaluation of Anonymity and Confidentiality Protocols using Theorem Proving ; Formal Methods in System Design, Vol. 47, No. 3, Springer, December 2015, pp 265-286.
H. Aridhi, M.H. Zaki, and S. Tahar:Fast Statistical Analysis of Nonlinear Analog Circuits Using Model Order Reduction ;Analog Integrated Circuits & Signal Processing, Vol. 85, No. 3, Springer, December 2015, pp.379-394.
H. Chaoui, N. Golbon, I. Hmouz, R. Souissi, and S. Tahar:Lyapunov-Based Adaptive State of Charge and State of Health Estimation for Lithium-Ion Batteries ; IEEE Transactions on Industrial Electronics, Vol. 62, No. 3, March 2015, pp. 1610-1618. [BEST PAPER ]
M. Elleuch, O. Hasan, S. Tahar and M. Abid:Formal Probabilistic Analysis of Detection Properties in Wireless Sensor Networks ; Formal Aspects of Computing, Springer, Vol. 27, No. 1, January 2015, pp. 79-102.
S. K. Afshar, U. Siddique, M.Y. Mahmoud, V. Aravantinos, O. Seddiki, O. Hasan and S. Tahar:Formal Analysis of Optical Systems ; Mathematics in Computer Science, Vol. 8, No. 1, Springer, May 2014, pp. 39-70.
A. Souari, A. Gawanmeh, S. Tahar, and M.L. Ammari:Design and Verification of a Frequency Domain Equalizer ; Microelectronics Journal, Vol. 45, No. 2, Elsevier, February 2014, pp. 167-178.
N. Abbasi, O. Hasan, and S. Tahar. Approach for Lifetime Reliability Analysis using Theorem Proving ; Journal of Computer and System Sciences, Elsevier, Vol. 80, No. 2, March 2014, pp. 323-345.
R. Narayanan, I. Seghaier, M. Zaki, and S. Tahar. Statistical Run-Time Verification of Analog Circuits in Presence of Noise and Process Variation ; IEEE Transactions on Very Large Scale Integration, Vol. 21, No. 10, October 2013, pp. 1811-1822.
L. Liu, O. Hasan, and S. Tahar. Formal Reasoning about Finite-state Discrete-Time Markov Chains in HOL ; Journal of Computer Science and Technology, Springer, Vol. 28, No. 2, March 2013, pp. 231-217.
T. Mhamdi, O. Hasan, and S. Tahar. Formalization of Measure and Lebesgue Integration for Probabilistic Analysis in HOL ; ACM Transactions on Embedded Computing Systems, Vol. 12, No. 1, January 2013, pp. 13.1-13.23.
A. Gawanmeh and S. Tahar. Domain Restriction Based Formal Model for Firewall Configurations ; International Journal for Information Security Research, Vol. 2, No. 2, Infonomics Society, June 2012, pp. 294-302.
A. Gawanmeh, S. Tahar, and L. Jemni Ben Ayed. Formal Verification of Secrecy in Group Key Protocols Using Event-B ; International Journal of Communications, Network and System Sciences, Vol. 5, No. 3, Scientific Research, March 2012, pp. 165-177.
A. Cui, C.-H. Chang, S. Tahar, and A. Abdel-Hamid: A Robust FSM Watermarking Scheme for IP Protection of Sequential Circuit Design ; IEEE Transactions on CAD of Integrated Circuits and Systems , Vol. 30, No. 5, May 2011, pp. 678-690.
W. Denman, M. Zaki, and S. Tahar: Formal Verification of Bond Graph Modelled Analog Circuits ; IET Circuits, Devices & Systems , Vol. 5, No. 3, May 2011, pp.243-255.
O. Hasan and S. Tahar: Reasoning about Conditional Probabilities in a Higher-order-Logic Theorem Prover ; Journal of Applied Logic, Vol. 9, No. 1, March 2011, Elsevier, pp. 23-40.
O. Hasan, J. Patel, and S. Tahar: Formal Reliability Analysis of Combinational Circuitsusing Theorem Proving ; Journal of Applied Logic, Vol. 9, No. 1, March 2011, Elsevier, pp. 41-60.
S. Abed, Y. Mokhtari, O. Ait-Mohamed, and S. Tahar: NuMDG: A New Tool for Multiway Decision Graphs Construction ; Journal of Computer Science and Technology , Vol. 26, No. 1, Springer, January 2011, pp. 139-152.
O. Hasan and S. Tahar: Formally Analyzing Expected Time Complexity of Algorithms using Theorem Proving ; Journal of Computer Science and Technology , Vol. 6, No. 5, Springer, November 2010, pp. 1306-1321.
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 , Vol. 53, No. 5, May 2010, Oxford U. Press, pp. 465-488.
O. Hasan, S. Tahar, and N. Abbasi: Formal Reliability Analysis using Theorem Proving ; IEEE Transactions on Computers , Vol. 59, No. 5, May 2010, pp. 579-592.
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.
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.
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.
M.H. Zaki, W. Denman and S. Tahar: Integrating Abstraction Techniques for Formal Verification of Analog Designs ; Journal of Aerospace Computing, Information, and Communication , Vol. 6, May 2009, pp. 373-392.
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.
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. 207-218.
O. Hasan and S. Tahar: Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL ; Journal of Automated Reasoning , Vol. 42, No. 1, Springer Verlag, January 2009, pp. 1-33.
M. Zaki, S. Tahar and G. Bois: Formal Verification of Analog and Mixed Signal Designs: A Survey ; Microelectronics Journal , Vol. 39, No. 12, Elsevier B.V. Pub., December 2008, pp. 1395-1404.
O.Hasan and S. Tahar: Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables . Journal of Automated Reasoning , Vol. 41, No. 3-4, Springer Verlag, November 2008, pp. 295-323.
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 , Vol.27, No. 9, September 2008, pp 1565-1570.
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, 2008, pp. 859.881.
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.
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.
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.
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, Springer Verlag , pp. 173-200.
A.T. Abdel-Hamid, S. Tahar, E.M. Aboulhamid: A Survey on IP Watermarking Techniques ; Design Automation for Embedded Systems , Vol. 9, No. 3, July 2005, Springer Verlag , pp. 211-227.
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.
Ying Xu, Xiaoyu Song, Eduard Cerny, Otmane Ait Mohamed: Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs (MDGs) ; Computer Journal , Vol 47, No 1, 2004, pp. 71-84.
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.
S. Tahar, M.H. Zobair, and X. Song: On the Formal Verification of a SONET Data Stream Processor ; IEE Proceedings – Computers and Digital Techniques , Vol. 151, No. 1, January 2004, pp. 71-81.
Otmane Ait Mohamed, Xiaoyu Song, Eduard Cerny: On the non-termination of MDG-based abstract state enumeration ; Theoretical Computer Science, 1-3(300): 161-179 (2003).
S. Kort, S. Tahar, and P. Curzon: Hierarchical Formal Verification Using a Hybrid Tool ; International Journal on Software Tools for Technology Transfer , Vol. 4, Springer Verlag, 2002, pp. 1-10.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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. [BEST PAPER ]