Sofiène Tahar

319 papers A* 2A 17B 29C 54Misc 4Journal 103Unranked 104

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Formal Safety Guarantees for Autonomous Vehicles using Barrier Certificates. CoRR Oumaima Barhoumi, Mohamed H. Zaki, Sofiène Tahar
2026	J	`jnl`	On the Formalization of Network Topology Matrices in HOL. CoRR Kubra Aksoy, Adnan Rashid, Osman Hasan, Sofiène Tahar
2025	J	`jnl`	A Comparative Study of Oscillatory Perturbations in Car-Following Models. CoRR Oumaima Barhoumi, Ghazal Farhani, Taufiq Rahman, Mohamed H. Zaki, Sofiène Tahar
2025	J	`jnl`	Extending XReason: Formal Explanations for Adversarial Detection. CoRR Amira Jemaa, Adnan Rashid, Sofiène Tahar
2025	—	`conf`	Formal Analysis of Electrical Circuit Network Topologies Using Theorem Proving. SysCon Kubra Aksoy, Adnan Rashid, Osman Hasan, Sofiène Tahar
2025	—	`conf`	Formally Constrained Reinforcement Learning for Traffic Signal Control at Intersections. SysCon Oumaima Barhoumi, Mohamed H. Zaki, Sofiène Tahar
2025	J	`jnl`	Fuel Consumption in Platoons: A Literature Review. CoRR Oumaima Barhoumi, Ghazal Farhani, Taufiq Rahman, Mohamed H. Zaki, Sofiène Tahar, Fadi Araji
2025	J	`jnl`	ML-based Load Value Approximator for Efficient Multimedia Processing. ACM Trans. Multim. Comput. Commun. Appl. Alain Aoun, Mahmoud Masadeh, Sofiène Tahar
2025	J	`jnl`	Proof Recommendation System for the HOL4 Theorem Prover. CoRR Nour Dekhil, Adnan Rashid, Sofiène Tahar
2024	C	`conf`	A Framework for Formal Probabilistic Risk Assessment Using HOL Theorem Proving. CICM Mohamed Abdelghany, Adnan Rashid, Sofiène Tahar
2024	—	`conf`	Arithmetic Calculus Modeling for Approximate Circuits. ICM Alain Aoun, Mahmoud Masadeh, Osman Hasan, Sofiène Tahar
2024	J	`jnl`	Dynamic dependability analysis of shuffle-exchange networks. Formal Methods Syst. Des. Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar
2024	—	`conf`	Energy-Efficient Approximate Squaring Unit. ICM Mahmoud Masadeh, Alain Aoun, Sofiène Tahar
2024	—	`conf`	Formal Analysis of Vehicular Crash Severity Using KeYmaera X. SCSS Oumaima Barhoumi, Mohamed H. Zaki, Sofiène Tahar
2024	C	`conf`	Formal Kinematic Analysis of Epicyclic Bevel Gear Trains. ICFEM Kubra Aksoy, Adnan Rashid, Sofiène Tahar
2024	—	`conf`	Formal Verification of ABCD Parameters Based Models for Transmission Lines. SCSS Elif Deniz, Adnan Rashid, Osman Hasan, Sofiène Tahar
2024	C	`conf`	Formal Verification of Coupled Transmission Lines using Theorem Proving. VECoS Elif Deniz, Adnan Rashid, Sofiène Tahar
2024	C	`conf`	Formalizing Potential Flows Using the HOL Light Theorem Prover. ICFEM Elif Deniz, Sofiène Tahar
2024	C	`conf`	HOL4PRS: Proof Recommendation System for the HOL4 Theorem Prover. CICM Nour Dekhil, Adnan Rashid, Sofiène Tahar
2024	—	`conf`	Machine Learning based Memory Load Value Predictor for Multimedia Applications. ICM Alain Aoun, Mahmoud Masadeh, Sofiène Tahar
2023	—	`conf`	A Machine Learning Based Load Value Approximator Guided by the Tightened Value Locality. ACM Great Lakes Symposium on VLSI Alain Aoun, Mahmoud Masadeh, Sofiène Tahar
2023	C	`conf`	Formal Analysis of an IoT-Based Healthcare Application. ISCC Maissa Elleuch, Sofiène Tahar
2023	C	`ed.`	Formal Methods and Software Engineering - 24th International Conference on Formal Engineering Methods, ICFEM 2023, Brisbane, QLD, Australia, November 21-24, 2023, Proceedings ICFEM Yi Li, Sofiène Tahar
2022	J	`jnl`	Event Tree Reliability Analysis of Safety-Critical Systems Using Theorem Proving. IEEE Syst. J. Mohamed Abdelghany, Waqar Ahmad, Sofiène Tahar
2022	—	`conf`	Formal Probabilistic Risk Assessment of a Nuclear Power Plant. FTSCS Mohamed Abdelghany, Sofiène Tahar
2022	—	`conf`	Formalization of Functional Block Diagrams Using HOL Theorem Proving. SBMF Mohamed Abdelghany, Sofiène Tahar
2022	—	`conf`	On the Design of Approximate Sobel Filter. ICM Alain Aoun, Mahmoud Masadeh, Sofiène Tahar
2022	C	`conf`	On the Formalization of the Heat Conduction Problem in HOL. CICM Elif Deniz, Adnan Rashid, Osman Hasan, Sofiène Tahar
2022	J	`jnl`	On the Formalization of the Heat Conduction Problem in HOL. CoRR Elif Deniz, Adnan Rashid, Osman Hasan, Sofiène Tahar
2022	J	`jnl`	Towards All-optical Stochastic Computing Using Photonic Crystal Nanocavities. ACM J. Emerg. Technol. Comput. Syst. Hassnaa El-Derhalli, Léa Constans, Sébastien Le Beux, Alfredo De Rossi, Fabrice Raineri, Sofiène Tahar
2021	J	`jnl`	A Quality-assured Approximate Hardware Accelerators-based on Machine Learning and Dynamic Partial Reconfiguration. ACM J. Emerg. Technol. Comput. Syst. Mahmoud Masadeh, Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar
2021	J	`jnl`	Cause-Consequence Diagram Reliability Analysis Using Formal Techniques With Application to Electrical Power Networks. IEEE Access Mohamed Abdelghany, Sofiène Tahar
2021	J	`jnl`	Design Space Exploration of Stochastic Computing Architectures Implemented Using Integrated Optics. IEEE Trans. Emerg. Top. Comput. Hassnaa El-Derhalli, Sébastien Le Beux, Sofiène Tahar
2021	—	`conf`	Dynamic Fault Tree Models for FPGA Fault Tolerance and Reliability. ISVLSI Yassmeen Elderhalli, Nahla A. El-Araby, Osman Hasan, Axel Jantsch, Sofiène Tahar
2021	J	`jnl`	Energy-Efficient Resource Allocation in Multi-UAV Networks With NOMA. IEEE Trans. Green Commun. Netw. Saif Najmeddin, Sonia Aïssa, Sofiène Tahar
2021	—	`conf`	Energy-Efficient Wireless Powered Communications with NOMA in Multi-UAV Aided Networks. VTC Fall Saif Najmeddin, Sonia Aïssa, Sofiène Tahar
2021	—	`conf`	Failure Analysis of Hadoop Schedulers using an Integration of Model Checking and Simulation. SCSS Mbarka Soualhia, Foutse Khomh, Sofiène Tahar
2021	J	`jnl`	Formal FT-based Cause-Consequence Reliability Analysis using Theorem Proving. CoRR Mohamed Abdelghany, Sofiène Tahar
2021	C	`conf`	Formalization of RBD-Based Cause Consequence Analysis in HOL. CICM Mohamed Abdelghany, Sofiène Tahar
2021	J	`jnl`	Machine-Learning-Based Self-Tunable Design of Approximate Computing. IEEE Trans. Very Large Scale Integr. Syst. Mahmoud Masadeh, Osman Hasan, Sofiène Tahar
2021	J	`jnl`	Optical Stochastic Computing Architectures Using Photonic Crystal Nanocavities. CoRR Hassnaa El-Derhalli, Léa Constans, Sébastien Le Beux, Alfredo De Rossi, Fabrice Raineri, Sofiène Tahar
2020	J	`jnl`	A Dynamic and Failure-Aware Task Scheduling Framework for Hadoop. IEEE Trans. Cloud Comput. Mbarka Soualhia, Foutse Khomh, Sofiène Tahar
2020	J	`jnl`	A Formally Verified HOL4 Algebra for Event Trees. CoRR Mohamed Abdelghany, Waqar Ahmad, Sofiène Tahar
2020	C	`conf`	A Framework for Formal Dynamic Dependability Analysis Using HOL Theorem Proving. CICM Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar
2020	—	`conf`	Decision Tree-based Adaptive Approximate Accelerators for Enhanced Quality. SysCon Mahmoud Masadeh, Alain Aoun, Osman Hasan, Sofiène Tahar
2020	J	`jnl`	ETMA: A New Software for Event Tree Analysis with Application to Power Protection. CoRR Mohamed Abdelghany, Waqar Ahmad, Sofiène Tahar, Sowmith Nethula
2020	—	`conf`	ETMA: An Efficient Tool for Event Trees Modeling and Analysis. SysCon Mohamed Abdelghany, Waqar Ahmad, Sofiène Tahar, Sowmith Nethula
2020	B	`conf`	Energy-Efficient Resource Allocation for UAV-Enabled Information and Power Transfer with NOMA. GLOBECOM Saif Najmeddin, Sonia Aïssa, Sofiène Tahar
2020	J	`jnl`	Formal Verification of Cyber-Physical Systems using Theorem Proving (Invited Paper). CoRR Adnan Rashid, Umair Siddique, Sofiène Tahar
2020	J	`jnl`	Formal reliability and failure analysis of ethernet based communication networks in a smart grid substation. Formal Aspects Comput. Waqar Ahmad, Osman Hasan, Sofiène Tahar
2020	—	`conf`	Highly-Reliable Approximate Quadruple Modular Redundancy with Approximation-Aware Voting. ICM Mahmoud Masadeh, Alain Aoun, Osman Hasan, Sofiène Tahar
2020	—	`conf`	Machine Learning-Based Self-Compensating Approximate Computing. SysCon Mahmoud Masadeh, Osman Hasan, Sofiène Tahar
2020	J	`jnl`	Mating Sensitivity Analysis and Statistical Verification for Efficient Yield Estimation. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Ibtissem Seghaier, Mohamed H. Zaki, Sofiène Tahar
2020	A	`conf`	OSCAR: An Optical Stochastic Computing AcceleRator for Polynomial Functions. DATE Hassnaa El-Derhalli, Sébastien Le Beux, Sofiène Tahar
2019	C	`conf`	A Formally Verified Algebraic Approach for Dynamic Reliability Block Diagrams. ICFEM Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar
2019	J	`jnl`	A Formally Verified HOL Algebra for Dynamic Reliability Block Diagrams. CoRR Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar
2019	J	`jnl`	A Methodology for the Formal Verification of Dynamic Fault Trees Using HOL Theorem Proving. IEEE Access Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar
2019	J	`jnl`	A modeling and verification framework for optical quantum circuits. Formal Aspects Comput. Sidi Mohamed Beillahi, Mohamed Yousri Mahmoud, Sofiène Tahar
2019	J	`jnl`	Dynamic Dependability Analysis of Shuffle-exchange Networks using HOL Theorem Proving. CoRR Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar
2019	B	`conf`	Energy-Efficient Resource Allocation for DAV-Enabled Wireless Powered Communications. WCNC Saif Najmeddin, Ali Bayat, Sonia Aïssa, Sofiène Tahar
2019	J	`jnl`	Error Analysis of Approximate Array Multipliers. CoRR Mahmoud Masadeh, Osman Hasan, Sofiène Tahar
2019	—	`conf`	Formal Verification of Cyber-Physical Systems Using Theorem Proving. FTSCS Adnan Rashid, Umair Siddique, Sofiène Tahar
2019	B	`conf`	Formal Verification of Rewriting Rules for Dynamic Fault Trees. SEFM Yassmeen Elderhalli, Matthias Volk, Osman Hasan, Joost-Pieter Katoen, Sofiène Tahar
2019	J	`jnl`	Input-Conscious Approximate Multiply-Accumulate (MAC) Unit for Energy-Efficiency. IEEE Access Mahmoud Masadeh, Osman Hasan, Sofiène Tahar
2019	J	`jnl`	Integrating DFT and DRBD Formalizations in HOL4. CoRR Yassmeen Elderhalli, Osman Hasan, Sofiène Tahar
2019	—	`ed.`	Joint Proceedings of the CME-EI, FMM, CAAT, FVPS, M3SRD, OpenMath Workshops, Doctoral Program and Work in Progress at the Conference on Intelligent Computer Mathematics 2018 co-located with the 11th Conference on Intelligent Computer Mathematics (CICM 2018), Hagenberg, Austria, August 13-17, 2018. CICM Workshops Osman Hasan, Abdou Youssef, Adam Naumowicz, William M. Farmer, Cezary Kaliszyk, Diane Gallois-Wong, Florian Rabe, Gabriel Dos Reis, Grant O. Passmore, James H. Davenport, Markus Pfeiffer, Michael Kohlhase, Serge Autexier, Sofiène Tahar, Thomas Koprucki, Umair Siddique, Walther Neuper, Wolfgang Windsteiger, Wolfgang Schreiner, Wolfram Sperber, Zoltán Kovács
2019	J	`jnl`	On the Formalization of Importance Measures using HOL Theorem Proving. CoRR Waqar Ahmed, Shahid Ali Murtza, Osman Hasan, Sofiène Tahar
2019	—	`conf`	On the formalization of importance measures using HOL theorem proving. FormaliSE@ICSE Waqar Ahmad, Shahid Ali Murtza, Osman Hasan, Sofiène Tahar
2019	J	`jnl`	Probabilistic Analysis of Dynamic Fault Trees using HOL Theorem Proving. FLAP Yassmeen Elderhalli, Waqar Ahmad, Osman Hasan, Sofiène Tahar
2019	A	`conf`	Stochastic Computing with Integrated Optics. DATE Hassnaa El-Derhalli, Sébastien Le Beux, Sofiène Tahar
2019	J	`jnl`	Stochastic Computing with Integrated Optics. CoRR Hassnaa El-Derhalli, Sébastien Le Beux, Sofiène Tahar
2019	A	`conf`	Using Machine Learning for Quality Configurable Approximate Computing. DATE Mahmoud Masadeh, Osman Hasan, Sofiène Tahar
2018	J	`jnl`	Accelerated and Reliable Analog Circuits Yield Analysis Using SMT Solving Techniques. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Ons Lahiouel, Mohamed H. Zaki, Sofiène Tahar
2018	—	`conf`	Approximation-Conscious IC Testing. ICM Mahmoud Masadeh, Osman Hasan, Sofiène Tahar
2018	—	`conf`	Comparative Study of Approximate Multipliers. ACM Great Lakes Symposium on VLSI Mahmoud Masadeh, Osman Hasan, Sofiène Tahar
2018	J	`jnl`	Comparative Study of Approximate Multipliers. CoRR Mahmoud Masadeh, Osman Hasan, Sofiène Tahar
2018	—	`conf`	Discriminating Chaos from Non-Gaussian Noise on Analog Circuits. NEWCAS Ibtissem Seghaier, Sofiène Tahar
2018	J	`jnl`	Formal Analysis of Discrete-Time Systems using z-Transform. FLAP Umair Siddique, Mohamed Yousri Mahmoud, Sofiène Tahar
2018	—	`conf`	Formal Dynamic Fault Trees Analysis Using an Integration of Theorem Proving and Model Checking. NFM Yassmeen Elderhalli, Osman Hasan, Waqar Ahmad, Sofiène Tahar
2018	J	`jnl`	Formal Probabilistic Analysis of Dynamic Fault Trees in HOL4. CoRR Yassmeen Elderhalli, Waqar Ahmad, Osman Hasan, Sofiène Tahar
2018	J	`jnl`	Formal probabilistic performance verification of randomly-scheduled wireless sensor networks. Int. J. Crit. Comput. Based Syst. Maissa Elleuch, Osman Hasan, Sofiène Tahar, Mohamed Abid
2018	—	`conf`	Reliability Analysis of CMOS Rambus Oscillator under Device Mismatch Effects. NEWCAS Ibtissem Seghaier, Sofiène Tahar
2017	J	`jnl`	A bug reproduction approach based on directed model checking and crash traces. J. Softw. Evol. Process. Mathieu Nayrolles, Abdelwahab Hamou-Lhadj, Sofiène Tahar, Alf Larsson
2017	J	`jnl`	Detection and sizing of metal-loss defects in oil and gas pipelines using pattern-adapted wavelets and machine learning. Appl. Soft Comput. Mohamed Layouni, Mohamed Salah Hamdi, Sofiène Tahar
2017	J	`jnl`	Dynamic Fault Trees Analysis using an Integration of Theorem Proving and Model Checking. CoRR Yassmeen Elderhalli, Osman Hasan, Waqar Ahmad, Sofiène Tahar
2017	A	`conf`	Enhancing analog yield optimization for variation-aware circuits sizing. DATE Ons Lahiouel, Mohamed H. Zaki, Sofiène Tahar
2017	J	`jnl`	Exploiting bounds optimization for the semi-formal verification of analog circuits. Integr. Ons Lahiouel, Henda Aridhi, Mohamed H. Zaki, Sofiène Tahar
2017	Misc	`conf`	Formal Analysis of Information Flow in HOL. SETTA Ghassen Helali, Sofiène Tahar, Osman Hasan, Tsvetan Dunchev
2017	J	`jnl`	Formal verification of stability and chaos in periodic optical systems. J. Comput. Syst. Sci. Umair Siddique, Sofiène Tahar
2017	—	`conf`	Formalization of Birth-Death and IID processes in higher-order logic. SysCon Liya Liu, Osman Hasan, Sofiène Tahar
2017	C	`conf`	Intertwined Global Optimization Based Reachability Analysis. VECoS Ibtissem Seghaier, Sofiène Tahar
2017	J	`jnl`	Task Scheduling in Big Data Platforms: A Systematic Literature Review. J. Syst. Softw. Mbarka Soualhia, Foutse Khomh, Sofiène Tahar
2017	C	`ed.`	Verification and Evaluation of Computer and Communication Systems - 11th International Conference, VECoS 2017, Montreal, QC, Canada, August 24-25, 2017, Proceedings VECoS Kamel Barkaoui, Hanifa Boucheneb, Ali Mili, Sofiène Tahar
2016	C	`conf`	Cross recurrence verification technique for process variation-resilient analog circuits. ISCAS Ibtissem Seghaier, Mohamed H. Zaki, Sofiène Tahar
2016	J	`jnl`	Enhancing Model Order Reduction for Nonlinear Analog Circuit Simulation. IEEE Trans. Very Large Scale Integr. Syst. Henda Aridhi, Mohamed H. Zaki, Sofiène Tahar
2016	—	`conf`	Formal Analysis of Engineering Systems Based on Signal-Flow-Graph Theory. NSV@CAV Sidi Mohamed Beillahi, Umair Siddique, Sofiène Tahar
2016	C	`conf`	Formal Dependability Modeling and Analysis: A Survey. CICM Waqar Ahmad, Osman Hasan, Sofiène Tahar
2016	J	`jnl`	Formal Dependability Modeling and Analysis: A Survey. CoRR Waqar Ahmad, Osman Hasan, Sofiène Tahar
2016	C	`conf`	Formal Probabilistic Analysis of Lifetime for a WSN-based Monitoring Application. VECoS Maissa Elleuch, Osman Hasan, Sofiène Tahar, Mohamed Abid
2016	—	`conf`	Formal Probabilistic Analysis of a WSN-Based Monitoring Framework for IoT Applications. FTSCS Maissa Elleuch, Osman Hasan, Sofiène Tahar, Mohamed Abid
2016	C	`conf`	Formalization of Normal Random Variables in HOL. CICM Muhammad Qasim, Osman Hasan, Maissa Elleuch, Sofiène Tahar
2016	J	`jnl`	Formalization of Reliability Block Diagrams in Higher-order Logic. J. Appl. Log. Waqar Ahmad, Osman Hasan, Sofiène Tahar
2016	—	`conf`	Hierarchical Verification of Quantum Circuits. NFM Sidi Mohamed Beillahi, Mohamed Yousri Mahmoud, Sofiène Tahar
2016	J	`jnl`	On the formal analysis of Gaussian optical systems in HOL. Formal Aspects Comput. Umair Siddique, Sofiène Tahar
2016	J	`jnl`	Tuning framework for stencil computation in heterogeneous parallel platforms. J. Supercomput. Taieb Lamine Ben Cheikh, Alexandra Aguiar, Sofiène Tahar, Gabriela Nicolescu
2015	—	`conf`	A Machine Learning Approach for Big Data in Oil and Gas Pipelines. FiCloud Abduljalil Mohamed, Mohamed Salah Hamdi, Sofiène Tahar
2015	—	`conf`	A Statistical Approach to Probe Chaos from Noise in Analog and Mixed Signal Designs. ISVLSI Ibtissem Seghaier, Mohamed H. Zaki, Sofiène Tahar
2015	C	`conf`	ATLAS: An AdapTive faiLure-Aware Scheduler for Hadoop. IPCCC Mbarka Soualhia, Foutse Khomh, Sofiène Tahar
2015	J	`jnl`	ATLAS: An Adaptive Failure-aware Scheduler for Hadoop. CoRR Mbarka Soualhia, Foutse Khomh, Sofiène Tahar
2015	C	`conf`	Enabling Symbolic and Numerical Computations in HOL Light. CICM Ons Seddiki, Cvetan Dunchev, Sanaz Khan Afshar, Sofiène Tahar
2015	J	`jnl`	Evaluation of anonymity and confidentiality protocols using theorem proving. Formal Methods Syst. Des. Tarek Mhamdi, Osman Hasan, Sofiène Tahar
2015	C	`conf`	Formal Analysis of Power Electronic Systems. ICFEM Sidi Mohamed Beillahi, Umair Siddique, Sofiène Tahar
2015	—	`conf`	Formal modeling and verification of integrated photonic systems. SysCon Umair Siddique, Osman Hasan, Sofiène Tahar
2015	J	`jnl`	Formal probabilistic analysis of detection properties in wireless sensor networks. Formal Aspects Comput. Maissa Elleuch, Osman Hasan, Sofiène Tahar, Mohamed Abid
2015	B	`conf`	Formal reliability analysis of wireless sensor network data transport protocols using HOL. WiMob Waqar Ahmad, Osman Hasan, Sofiène Tahar
2015	C	`conf`	Formalizing Physics: Automation, Presentation and Foundation Issues. CICM Cezary Kaliszyk, Josef Urban, Umair Siddique, Sanaz Khan Afshar, Cvetan Dunchev, Sofiène Tahar
2015	A	`conf`	JCHARMING: A bug reproduction approach using crash traces and directed model checking. SANER Mathieu Nayrolles, Abdelwahab Hamou-Lhadj, Sofiène Tahar, Alf Larsson
2015	J	`jnl`	Lyapunov-Based Adaptive State of Charge and State of Health Estimation for Lithium-Ion Batteries. IEEE Trans. Ind. Electron. Hicham Chaoui, Navid Golbon, Imad Hmouz, Ridha Souissi, Sofiène Tahar
2015	C	`conf`	On the Formal Analysis of Photonic Signal Processing Systems. FMICS Umair Siddique, Sidi Mohamed Beillahi, Sofiène Tahar
2015	C	`conf`	On the Formal Verification of Optical Quantum Gates in HOL. FMICS Mohamed Yousri Mahmoud, Prakash Panangaden, Sofiène Tahar
2015	—	`ch.`	On the Formalization of Cardinal Points of Optical Systems. Formalisms for Reuse and Systems Integration Umair Siddique, Sofiène Tahar
2015	J	`jnl`	Predicting Scheduling Failures in the Cloud. CoRR Mbarka Soualhia, Foutse Khomh, Sofiène Tahar
2015	—	`conf`	Predicting Scheduling Failures in the Cloud: A Case Study with Google Clusters and Hadoop on Amazon EMR. HPCC/CSS/ICESS Mbarka Soualhia, Foutse Khomh, Sofiène Tahar
2015	C	`conf`	Self-Organizing Map-Based Feature Visualization and Selection for Defect Depth Estimation in Oil and Gas Pipelines. IV Abduljalil Mohamed, Mohamed Salah Hamdi, Sofiène Tahar
2015	—	`conf`	Statistically Validating the Impact of Process Variations on Analog and Mixed Signal Designs. ACM Great Lakes Symposium on VLSI Ibtissem Seghaier, Mohamed H. Zaki, Sofiène Tahar
2015	—	`conf`	Time Performance Formal Evaluation of Complex Systems. SBMF Valdivino Alexandre de Santiago Jr., Sofiène Tahar
2015	—	`conf`	Towards Formal Reliability Analysis of Logistics Service Supply Chains using Theorem Proving. IWIL@LPAR Waqar Ahmad, Osman Hasan, Sofiène Tahar
2015	A*	`conf`	Towards enhancing analog circuits sizing using SMT-based techniques. DAC Ons Lahiouel, Mohamed H. Zaki, Sofiène Tahar
2015	C	`conf`	Towards the Formalization of Fractional Calculus in Higher-Order Logic. CICM Umair Siddique, Osman Hasan, Sofiène Tahar
2015	J	`jnl`	Towards the Formalization of Fractional Calculus in Higher-Order Logic. CoRR Umair Siddique, Osman Hasan, Sofiène Tahar
2014	C	`conf`	A Framework for Formal Reasoning about Geometrical Optics. CICM Umair Siddique, Sofiène Tahar
2014	—	`conf`	A qualitative simulation approach for verifying PLL locking property. ACM Great Lakes Symposium on VLSI Ibtissem Seghaier, Henda Aridhi, Mohamed H. Zaki, Sofiène Tahar
2014	—	`conf`	A semi-formal approach for analog circuits behavioral properties verification. ACM Great Lakes Symposium on VLSI Ons Lahiouel, Henda Aridhi, Mohamed H. Zaki, Sofiène Tahar
2014	—	`conf`	A survey on the application of Neural Networks in the safety assessment of oil and gas pipelines. CIES Mohamed Layouni, Sofiène Tahar, Mohamed Salah Hamdi
2014	J	`jnl`	An approach for lifetime reliability analysis using theorem proving. J. Comput. Syst. Sci. Naeem Abbasi, Osman Hasan, Sofiène Tahar
2014	J	`jnl`	Design and verification of a frequency domain equalizer. Microelectron. J. Anis Souari, Amjad Gawanmeh, Sofiène Tahar, Mohamed Lassaad Ammari
2014	—	`conf`	Enablingy the DC solutions characterization using a fuzzy approach. NEWCAS Ons Lahiouel, Henda Aridhi, Mohamed H. Zaki, Sofiène Tahar
2014	J	`jnl`	Formal Analysis of Optical Systems. CoRR Sanaz Khan Afshar, Umair Siddique, Mohamed Yousri Mahmoud, Vincent Aravantinos, Ons Seddiki, Osman Hasan, Sofiène Tahar
2014	J	`jnl`	Formal Analysis of Optical Systems. Math. Comput. Sci. Sanaz Khan Afshar, Umair Siddique, Mohamed Yousri Mahmoud, Vincent Aravantinos, Ons Seddiki, Osman Hasan, Sofiène Tahar
2014	B	`conf`	Formal Verification of Optical Quantum Flip Gate. ITP Mohamed Yousri Mahmoud, Vincent Aravantinos, Sofiène Tahar
2014	C	`conf`	Formal reliability analysis of a typical FHIR standard based e-Health system using PRISM. Healthcom Usman Pervez, Osman Hasan, Khalid Latif, Sofiène Tahar, Amjad Gawanmeh, Mohamed Salah Hamdi
2014	C	`conf`	Formalization of Complex Vectors in Higher-Order Logic. CICM Sanaz Khan Afshar, Vincent Aravantinos, Osman Hasan, Sofiène Tahar
2014	J	`jnl`	Formalization of Complex Vectors in Higher-Order Logic. CoRR Sanaz Khan Afshar, Vincent Aravantinos, Osman Hasan, Sofiène Tahar
2014	—	`conf`	Formalization of Zsyntax to Reason About Molecular Pathways in HOL4. SBMF Sohaib Ahmad, Osman Hasan, Umair Siddique, Sofiène Tahar
2014	—	`conf`	Generation of reduced analog circuit models using transient simulation traces. ACM Great Lakes Symposium on VLSI Paul Winkler, Henda Aridhi, Mohamed H. Zaki, Sofiène Tahar
2014	B	`conf`	Implicational Rewriting Tactics in HOL. ITP Vincent Aravantinos, Sofiène Tahar
2014	C	`conf`	On the Formal Analysis of HMM Using Theorem Proving. ICFEM Liya Liu, Vincent Aravantinos, Osman Hasan, Sofiène Tahar
2014	B	`conf`	On the Formalization of Z-Transform in HOL. ITP Umair Siddique, Mohamed Yousri Mahmoud, Sofiène Tahar
2014	—	`conf`	On the Quantum Formalization of Coherent Light in HOL. NASA Formal Methods Mohamed Yousri Mahmoud, Sofiène Tahar
2014	—	`conf`	Performance evaluation of time and frequency domain equalizers. CCECE Anis Souari, Mohamed Lassaad Ammari, Amjad Gawanmeh, Sofiène Tahar
2014	—	`conf`	Real time verification of firewalls with dynamic rulebase update. CCECE Amjad Gawanmeh, Sofiène Tahar
2014	Misc	`conf`	Towards ray optics formalization of optical imaging systems. IRI Umair Siddique, Sofiène Tahar
2014	C	`conf`	Towards the Formal Reliability Analysis of Oil and Gas Pipelines. CICM Waqar Ahmad, Osman Hasan, Sofiène Tahar, Mohammad Salah Hamdi
2014	J	`jnl`	Towards the Formal Reliability Analysis of Oil and Gas Pipelines. CoRR Waqar Ahmad, Osman Hasan, Sofiène Tahar, Mohammad Salah Hamdi
2014	A	`conf`	Towards the formal analysis of microresonators based photonic systems. DATE Umair Siddique, Sofiène Tahar
2014	—	`conf`	Towards the formal verification of optical interconnects. NEWCAS Sanaz Khan Afshar, Osman Hasan, Sofiène Tahar
2013	—	`conf`	Formal Analysis of Information Flow Using Min-Entropy and Belief Min-Entropy. SBMF Ghassen Helali, Osman Hasan, Sofiène Tahar
2013	—	`conf`	Formal Analysis of Memory Contention in a Multiprocessor System. SBMF Liya Liu, Osman Hasan, Sofiène Tahar
2013	J	`jnl`	Formal Reasoning About Finite-State Discrete-Time Markov Chains in HOL. J. Comput. Sci. Technol. Liya Liu, Osman Hasan, Sofiène Tahar
2013	B	`conf`	Formal Reasoning about Classified Markov Chains in HOL. ITP Liya Liu, Osman Hasan, Vincent Aravantinos, Sofiène Tahar
2013	—	`conf`	Formal Stability Analysis of Optical Resonators. NASA Formal Methods Umair Siddique, Vincent Aravantinos, Sofiène Tahar
2013	—	`conf`	Formalization of Infinite Dimension Linear Spaces with Application to Quantum Theory. NASA Formal Methods Mohamed Yousri Mahmoud, Vincent Aravantinos, Sofiène Tahar
2013	J	`jnl`	Formalization of Measure Theory and Lebesgue Integration for Probabilistic Analysis in HOL. ACM Trans. Embed. Comput. Syst. Tarek Mhamdi, Osman Hasan, Sofiène Tahar
2013	J	`jnl`	Statistical Run-Time Verification of Analog Circuits in Presence of Noise and Process Variation. IEEE Trans. Very Large Scale Integr. Syst. Rajeev Narayanan, Ibtissem Seghaier, Mohamed H. Zaki, Sofiène Tahar
2013	C	`conf`	Towards the Formal Performance Analysis of Wireless Sensor Networks. WETICE Maissa Elleuch, Osman Hasan, Sofiène Tahar, Mohamed Abid
2012	—	`conf`	Formal Analysis of Soft Errors using Theorem Proving. SCSS Naeem Abbasi, Osman Hasan, Sofiène Tahar
2012	—	`conf`	Formal Probabilistic Analysis of a Wireless Sensor Network for Forest Fire Detection. SCSS Maissa Elleuch, Osman Hasan, Sofiène Tahar, Mohamed Abid
2012	—	`conf`	Formal error analysis and verification of a frequency domain equalizer. NEWCAS Anis Souari, Sofiène Tahar, Amjad Gawanmeh
2012	—	`conf`	Formal verification of the heavy hitter problem. CCECE Ghassen Helali, Sofiène Tahar, Osman Hasan
2012	—	`conf`	Novel algorithm for detecting conflicts in firewall rules. CCECE Amjad Gawanmeh, Sofiène Tahar
2012	—	`conf`	On the Formal Analysis of Geometrical Optics in HOL. Automated Deduction in Geometry Umair Siddique, Vincent Aravantinos, Sofiène Tahar
2012	—	`conf`	On the Verification of a WiMax Design Using Symbolic Simulation. SCSS Salim Ismail Al-Akhras, Sofiène Tahar, Gabriela Nicolescu, Michel Langevin, Pierre G. Paulin
2012	—	`conf`	Parallelization strategies of the canny edge detector for multi-core CPUs and many-core GPUs. NEWCAS Taieb Lamine Ben Cheikh, Giovanni Beltrame, Gabriela Nicolescu, Farida Cheriet, Sofiène Tahar
2012	C	`conf`	Quantitative Analysis of Information Flow Using Theorem Proving. ICFEM Tarek Mhamdi, Osman Hasan, Sofiène Tahar
2012	A	`conf`	Towards improving simulation of analog circuits using model order reduction. DATE Henda Aridhi, Mohamed H. Zaki, Sofiène Tahar
2012	—	`conf`	Using LCSS algorithm for circuit level verification of analog designs. NEWCAS Rajeev Narayanan, Alaeddine Daghar, Mohamed H. Zaki, Sofiène Tahar
2012	A	`conf`	Verifying jitter in an analog and mixed signal design using dynamic time warping. DATE Rajeev Narayanan, Alaeddine Daghar, Mohamed H. Zaki, Sofiène Tahar
2011	J	`jnl`	A Robust FSM Watermarking Scheme for IP Protection of Sequential Circuit Design. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Aijiao Cui, Chip-Hong Chang, Sofiène Tahar, Amr Talaat Abdel-Hamid
2011	A	`conf`	Ensuring correctness of analog circuits in presence of noise and process variations using pattern matching. DATE Rajeev Narayanan, Mohamed H. Zaki, Sofiène Tahar
2011	C	`conf`	Formal Analysis of a Scheduling Algorithm for Wireless Sensor Networks. ICFEM Maissa Elleuch, Osman Hasan, Sofiène Tahar, Mohamed Abid
2011	J	`jnl`	Formal reliability analysis of combinational circuits using theorem proving. J. Appl. Log. Osman Hasan, Jigar Patel, Sofiène Tahar
2011	J	`jnl`	Formal verification of bond graph modelled analogue circuits. IET Circuits Devices Syst. William Denman, Mohamed H. Zaki, Sofiène Tahar
2011	B	`conf`	Formalization of Entropy Measures in HOL. ITP Tarek Mhamdi, Osman Hasan, Sofiène Tahar
2011	B	`conf`	Formalization of Finite-State Discrete-Time Markov Chains in HOL. ATVA Liya Liu, Osman Hasan, Sofiène Tahar
2011	—	`conf`	Modeling and verification of firewall configurations using domain restriction method. ICITST Amjad Gawanmeh, Sofiène Tahar
2011	J	`jnl`	NuMDG: A New Tool for Multiway Decision Graphs Construction. J. Comput. Sci. Technol. Sa'ed Abed, Yassine Mokhtari, Otmane Aït Mohamed, Sofiène Tahar
2011	J	`jnl`	Reasoning about conditional probabilities in a higher-order-logic theorem prover. J. Appl. Log. Osman Hasan, Sofiène Tahar
2011	—	`conf`	Towards Flight Control Verification Using Automated Theorem Proving. NASA Formal Methods William Denman, Mohamed H. Zaki, Sofiène Tahar, Luis Rodrigues
2011	C	`conf`	Welcome to ICCD 2011! ICCD Georgi Gaydadjiev, Sofiène Tahar, Greg Byrd, Klaus Schneider
2010	—	`conf`	10271 Abstracts Collection - Verification over discrete-continuous boundaries. Verification over discrete-continuous boundaries Bernd Becker, Luca Cardelli, Holger Hermanns, Sofiène Tahar
2010	C	`conf`	Formal Lifetime Reliability Analysis Using Continuous Random Variables. WoLLIC Naeem Abbasi, Osman Hasan, Sofiène Tahar
2010	—	`conf`	Formal Probabilistic Analysis: A Higher-Order Logic Based Approach. ASM Osman Hasan, Sofiène Tahar
2010	J	`jnl`	Formal Reliability Analysis Using Theorem Proving. IEEE Trans. Computers Osman Hasan, Sofiène Tahar, Naeem Abbasi
2010	A	`conf`	Formal verification of analog circuits in the presence of noise and process variation. DATE Rajeev Narayanan, Behzad Akbarpour, Mohamed H. Zaki, Sofiène Tahar, Lawrence C. Paulson
2010	J	`jnl`	Formally Analyzing Expected Time Complexity of Algorithms Using Theorem Proving. J. Comput. Sci. Technol. Osman Hasan, Sofiène Tahar
2010	B	`conf`	On the Formalization of the Lebesgue Integration Theory in HOL. ITP Tarek Mhamdi, Osman Hasan, Sofiène Tahar
2010	C	`conf`	Performance analysis of real-time rewriting models. AICCSA Jounaidi Ben Hassan, Osman Hasan, Tarek Sadani, Sofiène Tahar
2010	J	`jnl`	Using Stochastic Differential Equation for Verification of Noise in Analog/RF Circuits. J. Electron. Test. Rajeev Narayanan, Mohamed H. Zaki, Sofiène Tahar
2010	—	`ed.`	Verification over discrete-continuous boundaries, 04.07. - 09.07.2010 Verification over discrete-continuous boundaries Bernd Becker, Luca Cardelli, Holger Hermanns, Sofiène Tahar
2010	J	`jnl`	Verifying a Synthesized Implementation of IEEE-754 Floating-Point Exponential Function using HOL. Comput. J. Behzad Akbarpour, Amr Talaat Abdel-Hamid, Sofiène Tahar, John Harrison
2010	C	`conf`	Welcome to ICCD 2010! ICCD Peter-Michael Seidel, Georgi Gaydadjiev, Sofiène Tahar, Lars J. Svensson
2009	—	`conf`	Formal Analysis of Optical Waveguides in HOL. TPHOLs Osman Hasan, Sanaz Khan Afshar, Sofiène Tahar
2009	B	`conf`	Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays. IFM Osman Hasan, Naeem Abbasi, Sofiène Tahar
2009	B	`conf`	Formal Reasoning about Expectation Properties for Continuous Random Variables. FM Osman Hasan, Naeem Abbasi, Behzad Akbarpour, Sofiène Tahar, Reza Akbarpour
2009	B	`conf`	Formal verification of analog designs using MetiTarski. FMCAD William Denman, Behzad Akbarpour, Sofiène Tahar, Mohamed H. Zaki, Lawrence C. Paulson
2009	J	`jnl`	Integrating Abstraction Techniques for Formal Verification of Analog Designs. J. Aerosp. Comput. Inf. Commun. Mohamed H. Zaki, William Denman, Sofiène Tahar, Guy Bois
2009	J	`jnl`	Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL. J. Autom. Reason. Osman Hasan, Sofiène Tahar
2009	C	`conf`	Radio Access Network traffic generation for Mobile Switching Center. ISCC Suliman Albasheir, Sofiène Tahar, Claude Gauthier, Jean Roussel Personna
2009	J	`jnl`	Rank Functions Based Inference System for Group Key Management Protocols Verification. Int. J. Netw. Secur. Amjad Gawanmeh, Adel Bouhoula, Sofiène Tahar
2008	C	`conf`	A New Approach for the Construction of Multiway Decision Graphs. ICTAC Yassine Mokhtari, Sa'ed Abed, Otmane Aït Mohamed, Sofiène Tahar, Xiaoyu Song
2008	—	`conf`	Error Analysis and Verification of an IEEE 802.11 OFDM Modem using Theorem Proving. FMWS@CONCUR Abu Nasser Mohammed Abdullah, Behzad Akbarpour, Sofiène Tahar
2008	B	`conf`	Event-B based invariant checking of secrecy in group key protocols. LCN Amjad Gawanmeh, Sofiène Tahar, Leila Jemni Ben Ayed
2008	J	`jnl`	Formal verification of ASMs using MDGs. J. Syst. Archit. Amjad Gawanmeh, Sofiène Tahar, Kirsten Winter
2008	J	`jnl`	Formal verification of analog and mixed signal designs: A survey. Microelectron. J. Mohamed H. Zaki, Sofiène Tahar, Guy Bois
2008	—	`conf`	Fragile IP Watermarking Techniques. AHS Amr Talaat Abdel-Hamid, Sofiène Tahar
2008	J	`jnl`	IP Watermarking Using Incremental Technology Mapping at Logic Synthesis Level. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Aijiao Cui, Chip-Hong Chang, Sofiène Tahar
2008	B	`conf`	Performance Analysis of ARQ Protocols using a Theorem Prover. ISPASS Osman Hasan, Sofiène Tahar
2008	—	`conf`	Probabilistic Analysis of Wireless Systems Using Theorem Proving. FMWS@CONCUR Osman Hasan, Sofiène Tahar
2008	—	`ed.`	Theorem Proving in Higher Order Logics, 21st International Conference, TPHOLs 2008, Montreal, Canada, August 18-21, 2008. Proceedings TPHOLs Otmane Aït Mohamed, César A. Muñoz, Sofiène Tahar
2008	J	`jnl`	Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables. J. Autom. Reason. Osman Hasan, Sofiène Tahar
2007	J	`jnl`	A Design for Verification Approach Using an Embedding of PSL in aSML. J. Circuits Syst. Comput. Amjad Gawanmeh, Sofiène Tahar, Haja Moinudeen, Ali Habibi
2007	A	`conf`	A symbolic methodology for the verification of analog and mixed signal designs. DATE Ghiath Al Sammane, Mohamed H. Zaki, Sofiène Tahar
2007	C	`conf`	Autometic Generation of SystemC Transactors from AsmL Specification. FDL Tareq Hasan Khan, Ali Habibi, Sofiène Tahar, Otmane Aït Mohamed
2007	B	`conf`	Combining Symbolic Simulation and Interval Arithmetic for the Verification of AMS Designs. FMCAD Mohamed H. Zaki, Ghiath Al Sammane, Sofiène Tahar, Guy Bois
2007	J	`jnl`	Error analysis of digital filters using HOL theorem proving. J. Appl. Log. Behzad Akbarpour, Sofiène Tahar
2007	J	`jnl`	Formal Specification and Verification of the Intrusion-Tolerant Enclaves Protocol. Int. J. Netw. Secur. Mohamed Layouni, Jozef Hooman, Sofiène Tahar
2007	Misc	`conf`	Formal Verification of Analog and Mixed Signal Designs in Mathematica. International Conference on Computational Science (2) Mohamed H. Zaki, Ghiath Al Sammane, Sofiène Tahar
2007	A	`conf`	Formalization of Continuous Probability Distributions. CADE Osman Hasan, Sofiène Tahar
2007	J	`jnl`	Formalization of the Standard Uniform random variable. Theor. Comput. Sci. Osman Hasan, Sofiène Tahar
2007	J	`jnl`	Providing a formal linkage between MDG and HOL. Formal Methods Syst. Des. Haiyan Xiong, Paul Curzon, Sofiène Tahar, Ann Blandford
2007	C	`conf`	Qualitative Abstraction based Verification for Analog Circuits. ISoLA Mohamed H. Zaki, Sofiène Tahar, Guy Bois
2007	—	`conf`	Rank Theorems for Forward Secrecy in Group Key Management Protocols. AINA Workshops (1) Amjad Gawanmeh, Sofiène Tahar
2007	C	`conf`	Towards Assertion Based Verification of Analog and Mixed Signal Designs Using PSL. FDL Ghiath Al Sammane, Mohamed H. Zaki, Zhi Jie Dong, Sofiène Tahar
2007	—	`conf`	Verification of Expectation Properties for Discrete Random Variables in HOL. TPHOLs Osman Hasan, Sofiène Tahar
2007	B	`conf`	Verification of Probabilistic Properties in HOL Using the Cumulative Distribution Function. IFM Osman Hasan, Sofiène Tahar
2006	—	`conf`	A practical approach for monitoring analog circuits. ACM Great Lakes Symposium on VLSI Mohamed H. Zaki, Sofiène Tahar, Guy Bois
2006	J	`jnl`	An approach for the formal verification of DSP designs using Theorem proving. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Behzad Akbarpour, Sofiène Tahar
2006	—	`conf`	Automated Coverage Directed Test Generation Using a Cell-Based Genetic Algorithm. HLDVT Amer Samarah, Ali Habibi, Sofiène Tahar, Nawwaf Kharma
2006	J	`jnl`	Design and verification of SystemC transaction-level models. IEEE Trans. Very Large Scale Integr. Syst. Ali Habibi, Sofiène Tahar
2006	B	`conf`	Design for Verification of the PCI-X Bus. FMCAD Haja Moinudeen, Ali Habibi, Sofiène Tahar
2006	A	`conf`	Efficient assertion based verification using TLM. DATE Ali Habibi, Sofiène Tahar, Amer Samarah, Donglin Li, Otmane Aït Mohamed
2006	—	`conf`	Finite State Machine IP Watermarking: A Tutorial. AHS Amr Talaat Abdel-Hamid, Sofiène Tahar, El Mostapha Aboulhamid
2006	B	`conf`	Formal Analysis and Verification of an OFDM Modem Design using HOL. FMCAD Abu Nasser Mohammed Abdullah, Behzad Akbarpour, Sofiène Tahar
2006	—	`conf`	Generating finite state machines from SystemC. DATE Designers' Forum Ali Habibi, Haja Moinudeen, Sofiène Tahar
2006	J	`jnl`	Hybrid verification integrating HOL theorem proving with MDG model checking. Microelectron. J. Rabeb Mizouni, Sofiène Tahar, Paul Curzon
2006	A	`conf`	On the numerical verification of probabilistic rewriting systems. DATE Jounaïdi Ben Hassen, Sofiène Tahar
2006	—	`conf`	Towards a Faster Simulation of SystemC Designs. ISVLSI Ali Habibi, Haja Moinudeen, Amer Samarah, Sofiène Tahar
2005	A	`conf`	A Public-Key Watermarking Technique for IP Designs. DATE Amr Talaat Abdel-Hamid, Sofiène Tahar, El Mostapha Aboulhamid
2005	B	`conf`	An Approach for the Verification of SystemC Designs Using AsmL. ATVA Ali Habibi, Sofiène Tahar
2005	—	`conf`	AsmL Semantics in Fixpoint. Abstract State Machines Ali Habibi, Sofiène Tahar
2005	A	`conf`	Design for Verification of SystemC Transaction Level Models. DATE Ali Habibi, Sofiène Tahar
2005	—	`conf`	Embedding and Verification of PSL using AsmL. Abstract State Machines Amjad Gawanmeh, Ali Habibi, Sofiène Tahar
2005	J	`jnl`	Formalization of Fixed-Point Arithmetic in HOL. Formal Methods Syst. Des. Behzad Akbarpour, Sofiène Tahar, Abdelkader Dekdouk
2005	—	`conf`	On the Transformation of SystemC to AsmL Using Abstract Interpretation. AIOOL@VMCAI Ali Habibi, Sofiène Tahar
2005	—	`conf`	On the formal verification of a SystemC Packet switch model. ICECS Ali Habibi, Sofiène Tahar
2004	B	`conf`	A Methodology for the Formal Verification of FFT Algorithms in HOL. FMCAD Behzad Akbarpour, Sofiène Tahar
2004	J	`jnl`	A Survey on IP Watermarking Techniques. Des. Autom. Embed. Syst. Amr Talaat Abdel-Hamid, Sofiène Tahar, El Mostapha Aboulhamid
2004	—	`conf`	Assertion based verification of PSL for SystemC designs. SoC Ali Habibi, Amjad Gawanmeh, Sofiène Tahar
2004	—	`conf`	Design for verification of a PCI bus in SystemC. SoC Karim Oumalou, Ali Habibi, Sofiène Tahar
2004	C	`conf`	Enabling SystemC Verification using Abstract State Machines. FDL Amjad Gawanmeh, Ali Habibi, Sofiène Tahar
2004	—	`conf`	Error Analysis of Digital Filters Using Theorem Proving. TPHOLs Behzad Akbarpour, Sofiène Tahar
2004	B	`conf`	First-Order LTL Model Checking Using MDGs. ATVA Fang Wang, Sofiène Tahar, Otmane Aït Mohamed
2004	—	`conf`	Formal verification of an SoC platform protocol converter. ISCAS (5) Jounaïdi Ben Hassen, Sofiène Tahar
2004	J	`jnl`	MDG-Based State Enumeration By Retiming And Circuit Transformation. J. Circuits Syst. Comput. Otmane Aït Mohamed, Xiaoyu Song, Eduard Cerny, Sofiène Tahar, Zijian Zhou
2004	A	`conf`	On the Design and Verification Methodology of the Look-Aside Interface. DATE Ali Habibi, Asif Iqbal Ahmed, Otmane Aït Mohamed, Sofiène Tahar
2004	B	`conf`	Providing Automated Verification in HOL Using MDGs. ATVA Tarek Mhamdi, Sofiène Tahar
2004	—	`conf`	Towards an efficient assertion based verification of SystemC designs. HLDVT Ali Habibi, Sofiène Tahar
2003	—	`conf`	A Survey oA Survey on System-On-a-Chip Designn System-On-a-Chip Design. IWSOC Ali Habibi, Sofiène Tahar
2003	J	`jnl`	Comparison of SPIN and VIS for protocol verification. Int. J. Softw. Tools Technol. Transf. Hong Peng, Sofiène Tahar, Ferhat Khendek
2003	C	`conf`	Compositional Verification of a Switch Fabric from Nortel Networks. ICFEM Hong Peng, Sofiène Tahar, Yassine Mokhtari
2003	B	`conf`	Formal Verification of ASM Designs Using the MDG Tool. SEFM Amjad Gawanmeh, Sofiène Tahar, Kirsten Winter
2003	J	`jnl`	Hierarchical formal verification using a hybrid tool. Int. J. Softw. Tools Technol. Transf. Skander Kort, Sofiène Tahar, Paul Curzon
2003	—	`conf`	IP Watermarking Techniques: Survey and Comparison. IWSOC Amr Talaat Abdel-Hamid, Sofiène Tahar, El Mostapha Aboulhamid
2003	—	`conf`	Interfacing ASM with the MDG Tool. Abstract State Machines Amjad Gawanmeh, Sofiène Tahar, Kirsten Winter
2003	—	`conf`	Language emptiness checking using MDGs. ACM Great Lakes Symposium on VLSI Fang Wang, Sofiène Tahar
2003	C	`conf`	Modeling System C Fixed-Point Arithmetic in HOL. ICFEM Behzad Akbarpour, Sofiène Tahar
2003	—	`conf`	On the Correctness of an Intrusion-Tolerant Group Communication Protocol. CHARME Mohamed Layouni, Jozef Hooman, Sofiène Tahar
2003	C	`conf`	The Application of Formal Verification to SPW Designs. DSD Behzad Akbarpour, Sofiène Tahar
2002	C	`conf`	Enabling Hardware Verification through Design Changes. ICFEM Amr Talaat Abdel-Hamid, Sofiène Tahar, John Harrison
2002	C	`conf`	Environment Synthesis for Compositional Model Checking. ICCD Hong Peng, Yassine Mokhtari, Sofiène Tahar
2002	C	`conf`	Formal Verification of a DSP Chip Using an Iterative Approach. DSD Ali Habibi, Sofiène Tahar, Adel Ghazel
2002	C	`conf`	Formal Verification of a SONET Telecom System Block. ICFEM M. Hasan Zobair, Sofiène Tahar
2002	B	`conf`	Formalization of Cadence SPW Fixed-Point Arithmetic in HOL. IFM Behzad Akbarpour, Abdelkader Dekdouk, Sofiène Tahar
2002	B	`conf`	Formally Linking MDG and HOL Based on a Verified MDG System. IFM Haiyan Xiong, Paul Curzon, Sofiène Tahar, Ann Blandford
2002	—	`ed.`	Theorem Proving in Higher Order Logics, 15th International Conference, TPHOLs 2002, Hampton, VA, USA, August 20-23, 2002, Proceedings TPHOLs Victor Carreño, César A. Muñoz, Sofiène Tahar
2001	—	`conf`	Hierarchical Verification Using an MDG-HOL Hybrid Tool. CHARME Iskander Kort, Sofiène Tahar, Paul Curzon
2001	J	`jnl`	Performance of various multistage interference cancellation schemes for asynchronous QPSK/DS/CDMA over multipath Rayleigh fading channels. IEEE Trans. Commun. Jian F. Weng, Tho Le-Ngoc, Guo Q. Xue, Sofiène Tahar
2001	—	`conf`	Practical approaches to the verification of a telecom megacell using FormalCheck. ACM Great Lakes Symposium on VLSI Leila Barakatain, Sofiène Tahar, Jean Lamarche, Jean-Marc Gendreau
2000	J	`jnl`	An analytical model for performance evaluation of parallel interference cancellers in CDMA systems. IEEE Commun. Lett. Guoqiang Xue, Jian F. Weng, Tho Le-Ngoc, Sofiène Tahar
2000	—	`conf`	Analysis of Multilevel-Quantized Soft-Limiting Detector for an FH-SSMA System. ICC (3) Jian F. Weng, Guo Q. Xue, Tho Le-Ngoc, Sofiène Tahar
2000	—	`conf`	Formal hardware verification by integrating HOL and MDG. ACM Great Lakes Symposium on VLSI V. K. Pisini, Sofiène Tahar, Paul Curzon, Otmane Aït Mohamed, Xiaoyu Song
2000	J	`jnl`	Multilevel quantized soft-limiting detector for an FH-SSMA system. J. Commun. Networks Jian F. Weng, Tho Le-Ngoc, Guo Q. Xue, Sofiène Tahar
2000	C	`conf`	SPIN vs. VIS: A Case Study on the Formal Verification of the ATMR Protocol. ICFEM Hong Peng, Sofiène Tahar, Ferhat Khendek
2000	—	`conf`	Sequential and Distributed Simulations Using Java Threads. PARELEC Mostafa Azizi, El Mostapha Aboulhamid, Sofiène Tahar
1999	—	`conf`	A Hierarchical Approach to the Formal Verification of Embedded Systems Using MDGs. Great Lakes Symposium on VLSI Subhashini Balakrishnan, Sofiène Tahar
1999	—	`conf`	Adaptive multistage parallel interference cancellation for CDMA. ICC Guoqiang Xue, Jianfeng Weng, Tho Le-Ngoc, Sofiène Tahar
1999	J	`jnl`	Adaptive multistage parallel interference cancellation for CDMA. IEEE J. Sel. Areas Commun. Guoqiang Xue, Jianfeng Weng, Tho Le-Ngoc, Sofiène Tahar
1999	J	`jnl`	Comparing HOL and MDG: a Case Study on the Verification of an ATM Switch Fabric. Nord. J. Comput. Sofiène Tahar, Paul Curzon
1999	—	`conf`	Importing MDG Verification Results into HOL. TPHOLs Haiyan Xiong, Paul Curzon, Sofiène Tahar
1999	J	`jnl`	Modeling and formal verification of the Fairisle ATM switch fabricusing MDGs. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. Sofiène Tahar, Xiaoyu Song, Eduard Cerny, Zijian Zhou, Michel Langevin, Otmane Aït Mohamed
1999	—	`conf`	Multistage interference cancellation with diversity reception for QPSK asynchronous DS/CDMA system over multipath fading channels. ICC Jianfeng Weng, Guoqiang Xue, Tho Le-Ngoc, Sofiène Tahar
1999	J	`jnl`	Multistage interference cancellation with diversity reception for asynchronous QPSK DS/CDMA systems over multipath fading channels. IEEE J. Sel. Areas Commun. Jianfeng Weng, Guoqiang Xue, Tho Le-Ngoc, Sofiène Tahar
1999	Misc	`conf`	Multithreading-based Coverification Technique of HW/SW Systems. PDPTA Mostafa Azizi, El Mostapha Aboulhamid, Sofiène Tahar
1998	J	`jnl`	A Practical Methodology for the Formal Verification of RISC Processors. Formal Methods Syst. Des. Sofiène Tahar, Ramayya Kumar
1998	C	`conf`	Model checking of a real ATM switch. ICCD Jianping Lu, Sofiène Tahar, Dan Voicu, Xiaoyu Song
1998	—	`conf`	Practical Approaches to the Automatic Verification of an ATM Switch Fabric Using VIS. Great Lakes Symposium on VLSI Jianping Lu, Sofiène Tahar
1998	B	`conf`	Three Approaches to Hardware Verification: HOL, MDG and VIS Compared. FMCAD Sofiène Tahar, Paul Curzon, Jianping Lu
1997	—	`conf`	Verification with Abstract State Machines Using MDGs. Formal Hardware Verification Eduard Cerny, Francisco Corella, Michel Langevin, Xiaoyu Song, Sofiène Tahar, Zijian Zhou
1996	—	`conf`	A Comparison of MDG and HOL for Hardware Verification. TPHOLs Sofiène Tahar, Paul Curzon
1996	C	`conf`	Behavioral Verification of an ATM Switch Fabric using Implicit Abstract State Enumeration. ICCD Michel Langevin, Sofiène Tahar, Zijian Zhou, Xiaoyu Song, Eduard Cerny
1996	—	`conf`	Formal Verification of an ATM Switch Fabric using Multiway Decision Graphs. Great Lakes Symposium on VLSI Sofiène Tahar, Zijian Zhou, Xiaoyu Song, Eduard Cerny, Michel Langevin
1996	B	`conf`	Formal Verification of the Island Tunnel Controller Using Multiway Decision Graphs. FMCAD Zijian Zhou, Xiaoyu Song, Sofiène Tahar, Eduard Cerny, Francisco Corella, Michel Langevin
1996	A*	`conf`	MDG Tools for the Verification of RTL Designs. CAV K. D. Anon, N. Boulerice, Eduard Cerny, Francisco Corella, Michel Langevin, Xiaoyu Song, Sofiène Tahar, Ying Xu, Zijian Zhou
1995	—	`—`	Eine Methode zur formalen Verifikation von RISC-Prozessoren. Sofiène Tahar
1995	J	`jnl`	Formal Specification and Verification Techniques for RISC Pipeline Conflicts. Comput. J. Sofiène Tahar, Ramayya Kumar
1994	—	`conf`	Formal verification of pipeline conflicts in RISC processors. EURO-DAC Ramayya Kumar, Sofiène Tahar
1994	—	`conf`	Implementational Issues for Verifying RISC-Pipeline Conflicts in HOL. TPHOLs Sofiène Tahar, Ramayya Kumar
1993	—	`conf`	Implementing a Methodology for Formally Verifying RISC Processors in HOL. HUG Sofiène Tahar, Ramayya Kumar
1993	C	`conf`	Towards a Methodology for the Formal Hierarchical Verification. ICCD Sofiène Tahar, Ramayya Kumar