Hardware Verification Group Home > Publications >
Journal Papers
- 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.
- 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.
- 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.
- B. Akbarpour and S. Tahar: Error Analysis of Digital Filters using HOL Theorem Proving; Journal of Applied Logic, Vol. 5, No. 4, Elsevier B.V. Pub., December 2007, pp. 651-666.
- O. Hasan and S. Tahar Formalization of the Standard Uniform Random Variable; Theoretical Computer Science, Vol. 382, No. 1, Elsevier B.V. Pub., 2007, pp. 71-83.
- 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.
- 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, 2007, pp. 288-298.
- 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 Aït 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 Aït 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]