| 2025 | VECoS | $\mathbb {FETMA}$: A Tool for Functional Block Diagram and Event Tree Based Safety Analysis. | Mohamed Abdelghany, Adnan Rashid, Sofine Tahar |
| 2025 | VECoS | On the Formalization of Pseudoinverse of the Laplacian Matrix in HOL. | Kubra Aksoy, Adnan Rashid, Sofine Tahar |
| 2024 | ICFEM | Formal Kinematic Analysis of Epicyclic Bevel Gear Trains. | Kubra Aksoy, Adnan Rashid, Sofine Tahar |
| 2024 | ICFEM | Formalizing Potential Flows Using the HOL Light Theorem Prover. | Elif Deniz, Sofine Tahar |
| 2024 | VECoS | Formal Verification of Coupled Transmission Lines using Theorem Proving. | Elif Deniz, Adnan Rashid, Sofine Tahar |
| 2023 | ISCC | Formal Analysis of an IoT-Based Healthcare Application. | Maissa Elleuch, Sofine Tahar |
| 2021 | VTC | Energy-Efficient Wireless Powered Communications with NOMA in Multi-UAV Aided Networks. | Saif Najmeddin, Sonia Assa, Sofine Tahar |
| 2020 | DATE | OSCAR: An Optical Stochastic Computing AcceleRator for Polynomial Functions. | Hassnaa El-Derhalli, Sbastien Le Beux, Sofine Tahar |
| 2020 | GLOBECOM | Energy-Efficient Resource Allocation for UAV-Enabled Information and Power Transfer with NOMA. | Saif Najmeddin, Sonia Assa, Sofine Tahar |
| 2019 | DATE | Stochastic Computing with Integrated Optics. | Hassnaa El-Derhalli, Sbastien Le Beux, Sofine Tahar |
| 2019 | DATE | Using Machine Learning for Quality Configurable Approximate Computing. | Mahmoud Masadeh, Osman Hasan, Sofine Tahar |
| 2019 | ICFEM | A Formally Verified Algebraic Approach for Dynamic Reliability Block Diagrams. | Yassmeen Elderhalli, Osman Hasan, Sofine Tahar |
| 2019 | ICSE | On the formalization of importance measures using HOL theorem proving. | Waqar Ahmad, Shahid Ali Murtza, Osman Hasan, Sofine Tahar |
| 2019 | WCNC | Energy-Efficient Resource Allocation for DAV-Enabled Wireless Powered Communications. | Saif Najmeddin, Ali Bayat, Sonia Assa, Sofine Tahar |
| 2019 | SEFM | Formal Verification of Rewriting Rules for Dynamic Fault Trees. | Yassmeen Elderhalli, Matthias Volk, Osman Hasan, Joost-Pieter Katoen, Sofine Tahar |
| 2017 | DATE | Enhancing analog yield optimization for variation-aware circuits sizing. | Ons Lahiouel, Mohamed H. Zaki, Sofine Tahar |
| 2017 | SETTA | Formal Analysis of Information Flow in HOL. | Ghassen Helali, Sofine Tahar, Osman Hasan, Tsvetan Dunchev |
| 2017 | VECoS | Intertwined Global Optimization Based Reachability Analysis. | Ibtissem Seghaier, Sofine Tahar |
| 2016 | CAV | Formal Analysis of Engineering Systems Based on Signal-Flow-Graph Theory. | Sidi Mohamed Beillahi, Umair Siddique, Sofine Tahar |
| 2016 | ISCAS | Cross recurrence verification technique for process variation-resilient analog circuits. | Ibtissem Seghaier, Mohamed H. Zaki, Sofine Tahar |
| 2016 | VECoS | Formal Probabilistic Analysis of Lifetime for a WSN-based Monitoring Application. | Maissa Elleuch, Osman Hasan, Sofine Tahar, Mohamed Abid |
| 2015 | DAC | Towards enhancing analog circuits sizing using SMT-based techniques. | Ons Lahiouel, Mohamed H. Zaki, Sofine Tahar |
| 2015 | FMICS | On the Formal Verification of Optical Quantum Gates in HOL. | Mohamed Yousri Mahmoud, Prakash Panangaden, Sofine Tahar |
| 2015 | FMICS | On the Formal Analysis of Photonic Signal Processing Systems. | Umair Siddique, Sidi Mohamed Beillahi, Sofine Tahar |
| 2015 | HPCC | Predicting Scheduling Failures in the Cloud: A Case Study with Google Clusters and Hadoop on Amazon EMR. | Mbarka Soualhia, Foutse Khomh, Sofine Tahar |
| 2015 | ICFEM | Formal Analysis of Power Electronic Systems. | Sidi Mohamed Beillahi, Umair Siddique, Sofine Tahar |
| 2015 | IPCCC | ATLAS: An AdapTive faiLure-Aware Scheduler for Hadoop. | Mbarka Soualhia, Foutse Khomh, Sofine Tahar |
| 2015 | IV | Self-Organizing Map-Based Feature Visualization and Selection for Defect Depth Estimation in Oil and Gas Pipelines. | Abduljalil Mohamed, Mohamed Salah Hamdi, Sofine Tahar |
| 2015 | LPAR | Towards Formal Reliability Analysis of Logistics Service Supply Chains using Theorem Proving. | Waqar Ahmad, Osman Hasan, Sofine Tahar |
| 2015 | WiMob | Formal reliability analysis of wireless sensor network data transport protocols using HOL. | Waqar Ahmad, Osman Hasan, Sofine Tahar |
| 2014 | DATE | Towards the formal analysis of microresonators based photonic systems. | Umair Siddique, Sofine Tahar |
| 2014 | HealthCom | Formal reliability analysis of a typical FHIR standard based e-Health system using PRISM. | Usman Pervez, Osman Hasan, Khalid Latif, Sofine Tahar, Amjad Gawanmeh, Mohamed Salah Hamdi |
| 2014 | ICFEM | On the Formal Analysis of HMM Using Theorem Proving. | Liya Liu, Vincent Aravantinos, Osman Hasan, Sofine Tahar |
| 2014 | IRI | Towards ray optics formalization of optical imaging systems. | Umair Siddique, Sofine Tahar |
| 2014 | ITP | Implicational Rewriting Tactics in HOL. | Vincent Aravantinos, Sofine Tahar |
| 2014 | ITP | Formal Verification of Optical Quantum Flip Gate. | Mohamed Yousri Mahmoud, Vincent Aravantinos, Sofine Tahar |
| 2014 | ITP | On the Formalization of Z-Transform in HOL. | Umair Siddique, Mohamed Yousri Mahmoud, Sofine Tahar |
| 2013 | ITP | Formal Reasoning about Classified Markov Chains in HOL. | Liya Liu, Osman Hasan, Vincent Aravantinos, Sofine Tahar |
| 2013 | WETICE | Towards the Formal Performance Analysis of Wireless Sensor Networks. | Maissa Elleuch, Osman Hasan, Sofine Tahar, Mohamed Abid |
| 2012 | DATE | Towards improving simulation of analog circuits using model order reduction. | Henda Aridhi, Mohamed H. Zaki, Sofine Tahar |
| 2012 | DATE | Verifying jitter in an analog and mixed signal design using dynamic time warping. | Rajeev Narayanan, Alaeddine Daghar, Mohamed H. Zaki, Sofine Tahar |
| 2012 | ICFEM | Quantitative Analysis of Information Flow Using Theorem Proving. | Tarek Mhamdi, Osman Hasan, Sofine Tahar |
| 2011 | ATVA | Formalization of Finite-State Discrete-Time Markov Chains in HOL. | Liya Liu, Osman Hasan, Sofine Tahar |
| 2011 | DATE | Ensuring correctness of analog circuits in presence of noise and process variations using pattern matching. | Rajeev Narayanan, Mohamed H. Zaki, Sofine Tahar |
| 2011 | ICCD | Welcome to ICCD 2011! | Georgi Gaydadjiev, Sofine Tahar, Greg Byrd, Klaus Schneider |
| 2011 | ICFEM | Formal Analysis of a Scheduling Algorithm for Wireless Sensor Networks. | Maissa Elleuch, Osman Hasan, Sofine Tahar, Mohamed Abid |
| 2011 | ITP | Formalization of Entropy Measures in HOL. | Tarek Mhamdi, Osman Hasan, Sofine Tahar |
| 2010 | AICCSA | Performance analysis of real-time rewriting models. | Jounaidi Ben Hassan, Osman Hasan, Tarek Sadani, Sofine Tahar |
| 2010 | DATE | Formal verification of analog circuits in the presence of noise and process variation. | Rajeev Narayanan, Behzad Akbarpour, Mohamed H. Zaki, Sofine Tahar, Lawrence C. Paulson |
| 2010 | ICCD | Welcome to ICCD 2010! | Peter-Michael Seidel, Georgi Gaydadjiev, Sofine Tahar, Lars J. Svensson |
| 2010 | ITP | On the Formalization of the Lebesgue Integration Theory in HOL. | Tarek Mhamdi, Osman Hasan, Sofine Tahar |
| 2010 | WoLLIC | Formal Lifetime Reliability Analysis Using Continuous Random Variables. | Naeem Abbasi, Osman Hasan, Sofine Tahar |
| 2009 | FM | Formal Reasoning about Expectation Properties for Continuous Random Variables. | Osman Hasan, Naeem Abbasi, Behzad Akbarpour, Sofine Tahar, Reza Akbarpour |
| 2009 | FMCAD | Formal verification of analog designs using MetiTarski. | William Denman, Behzad Akbarpour, Sofine Tahar, Mohamed H. Zaki, Lawrence C. Paulson |
| 2009 | IFM | Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays. | Osman Hasan, Naeem Abbasi, Sofine Tahar |
| 2009 | ISCC | Radio Access Network traffic generation for Mobile Switching Center. | Suliman Albasheir, Sofine Tahar, Claude Gauthier, Jean Roussel Personna |
| 2008 | ICTAC | A New Approach for the Construction of Multiway Decision Graphs. | Yassine Mokhtari, Sa'ed Abed, Otmane At Mohamed, Sofine Tahar, Xiaoyu Song |
| 2008 | ISPASS | Performance Analysis of ARQ Protocols using a Theorem Prover. | Osman Hasan, Sofine Tahar |
| 2008 | LCN | Event-B based invariant checking of secrecy in group key protocols. | Amjad Gawanmeh, Sofine Tahar, Leila Jemni Ben Ayed |
| 2007 | AINA | Rank Theorems for Forward Secrecy in Group Key Management Protocols. | Amjad Gawanmeh, Sofine Tahar |
| 2007 | CADE | Formalization of Continuous Probability Distributions. | Osman Hasan, Sofine Tahar |
| 2007 | DATE | A symbolic methodology for the verification of analog and mixed signal designs. | Ghiath Al Sammane, Mohamed H. Zaki, Sofine Tahar |
| 2007 | FDL | Autometic Generation of SystemC Transactors from AsmL Specification. | Tareq Hasan Khan, Ali Habibi, Sofine Tahar, Otmane At Mohamed |
| 2007 | FDL | Towards Assertion Based Verification of Analog and Mixed Signal Designs Using PSL. | Ghiath Al Sammane, Mohamed H. Zaki, Zhi Jie Dong, Sofine Tahar |
| 2007 | FMCAD | Combining Symbolic Simulation and Interval Arithmetic for the Verification of AMS Designs. | Mohamed H. Zaki, Ghiath Al Sammane, Sofine Tahar, Guy Bois |
| 2007 | ICCS | Formal Verification of Analog and Mixed Signal Designs in Mathematica. | Mohamed H. Zaki, Ghiath Al Sammane, Sofine Tahar |
| 2007 | IFM | Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function. | Osman Hasan, Sofine Tahar |
| 2007 | ISoLA | Qualitative Abstraction based Verification for Analog Circuits. | Mohamed H. Zaki, Sofine Tahar, Guy Bois |
| 2006 | DATE | Generating finite state machines from SystemC. | Ali Habibi, Haja Moinudeen, Sofine Tahar |
| 2006 | DATE | Efficient assertion based verification using TLM. | Ali Habibi, Sofine Tahar, Amer Samarah, Donglin Li, Otmane At Mohamed |
| 2006 | DATE | On the numerical verification of probabilistic rewriting systems. | Jounadi Ben Hassen, Sofine Tahar |
| 2006 | FMCAD | Formal Analysis and Verification of an OFDM Modem Design using HOL. | Abu Nasser Mohammed Abdullah, Behzad Akbarpour, Sofine Tahar |
| 2006 | FMCAD | Design for Verification of the PCI-X Bus. | Haja Moinudeen, Ali Habibi, Sofine Tahar |
| 2005 | ATVA | An Approach for the Verification of SystemC Designs Using AsmL. | Ali Habibi, Sofine Tahar |
| 2005 | DATE | A Public-Key Watermarking Technique for IP Designs. | Amr Talaat Abdel-Hamid, Sofine Tahar, El Mostapha Aboulhamid |
| 2005 | DATE | Design for Verification of SystemC Transaction Level Models. | Ali Habibi, Sofine Tahar |
| 2004 | ATVA | Providing Automated Verification in HOL Using MDGs. | Tarek Mhamdi, Sofine Tahar |
| 2004 | ATVA | First-Order LTL Model Checking Using MDGs. | Fang Wang, Sofine Tahar, Otmane At Mohamed |
| 2004 | DATE | On the Design and Verification Methodology of the Look-Aside Interface. | Ali Habibi, Asif Iqbal Ahmed, Otmane At Mohamed, Sofine Tahar |
| 2004 | FDL | Enabling SystemC Verification using Abstract State Machines. | Amjad Gawanmeh, Ali Habibi, Sofine Tahar |
| 2004 | FMCAD | A Methodology for the Formal Verification of FFT Algorithms in HOL. | Behzad Akbarpour, Sofine Tahar |
| 2004 | ISCAS | Formal verification of an SoC platform protocol converter. | Jounadi Ben Hassen, Sofine Tahar |
| 2003 | DSD | The Application of Formal Verification to SPW Designs. | Behzad Akbarpour, Sofine Tahar |
| 2003 | ICFEM | Modeling System C Fixed-Point Arithmetic in HOL. | Behzad Akbarpour, Sofine Tahar |
| 2003 | ICFEM | Compositional Verification of a Switch Fabric from Nortel Networks. | Hong Peng, Sofine Tahar, Yassine Mokhtari |
| 2003 | SEFM | Formal Verification of ASM Designs Using the MDG Tool. | Amjad Gawanmeh, Sofine Tahar, Kirsten Winter |
| 2002 | DSD | Formal Verification of a DSP Chip Using an Iterative Approach. | Ali Habibi, Sofine Tahar, Adel Ghazel |
| 2002 | ICCD | Environment Synthesis for Compositional Model Checking. | Hong Peng, Yassine Mokhtari, Sofine Tahar |
| 2002 | ICFEM | Enabling Hardware Verification through Design Changes. | Amr Talaat Abdel-Hamid, Sofine Tahar, John Harrison |
| 2002 | ICFEM | Formal Verification of a SONET Telecom System Block. | M. Hasan Zobair, Sofine Tahar |
| 2002 | IFM | Formalization of Cadence SPW Fixed-Point Arithmetic in HOL. | Behzad Akbarpour, Abdelkader Dekdouk, Sofine Tahar |
| 2002 | IFM | Formally Linking MDG and HOL Based on a Verified MDG System. | Haiyan Xiong, Paul Curzon, Sofine Tahar, Ann Blandford |
| 2000 | ICFEM | SPIN vs. VIS: A Case Study on the Formal Verification of the ATMR Protocol. | Hong Peng, Sofine Tahar, Ferhat Khendek |
| 1999 | PDPTA | Multithreading-based Coverification Technique of HW/SW Systems. | Mostafa Azizi, El Mostapha Aboulhamid, Sofine Tahar |
| 1998 | FMCAD | Three Approaches to Hardware Verification: HOL, MDG and VIS Compared. | Sofine Tahar, Paul Curzon, Jianping Lu |
| 1998 | ICCD | Model checking of a real ATM switch. | Jianping Lu, Sofine Tahar, Dan Voicu, Xiaoyu Song |
| 1996 | CAV | MDG Tools for the Verification of RTL Designs. | K. D. Anon, N. Boulerice, Eduard Cerny, Francisco Corella, Michel Langevin, Xiaoyu Song, Sofine Tahar, Ying Xu, Zijian Zhou |
| 1996 | FMCAD | Formal Verification of the Island Tunnel Controller Using Multiway Decision Graphs. | Zijian Zhou, Xiaoyu Song, Sofine Tahar, Eduard Cerny, Francisco Corella, Michel Langevin |
| 1996 | ICCD | Behavioral Verification of an ATM Switch Fabric using Implicit Abstract State Enumeration. | Michel Langevin, Sofine Tahar, Zijian Zhou, Xiaoyu Song, Eduard Cerny |
| 1993 | ICCD | Towards a Methodology for the Formal Hierarchical Verification. | Sofine Tahar, Ramayya Kumar |