- G. Helali, S. Tahar, O. Hasan, and T. Dunchev: Formal Analysis of Information Flow in HOL; In: K. Guldstrand, L.O. Sokolsky, and J. Wang (Eds.), Dependable Software Engineering: Theories, Tools, and Applications, Lecture Notes in Computer Science 10606, Springer Verlag, 2017, pp. 283-299. [Proc. International Symposium on Dependable Software Engineering: Theories, Tools, and Applications (SETTA'17), Changsha, China, October 2017]
- I. Seghaier and S. Tahar: Intertwined Global Optimization based Reachability Analysis; In: K. Barkaoui, H. Boucheneb, A. Mili, and S. Tahar (Eds.), Verification and Evaluation of Computer and Communication Systems, Lecture Notes in Computer Science 10466, Springer Verlag, 2017, pp. 139-154. [Proc. International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS'17), Montreal, Canada, August 2017]
- L. Liu, O. Hasan, and S. Tahar: Formalization of Birth-Death and IID Processes in Higher-order Logic; [Proc. IEEE International Systems Conference (SysCon'17), Montreal, Quebec, Canada, April 2017, pp. 559-565.]
- O. Lahiouel, M.H. Zaki, ans S. Tahar: Enhancing Analog Yield Optimization for Variation-aware Circuits Sizing; [Proc. IEEE/ACM Design Automation and Test in Europe (DATE'17), Lausanne, Switzerland, March 2017, pp. 1273-1276.]
- M. Elleuch, O. Hasan, S. Tahar and M. Abid: Formal Probabilistic Analysis of a WSN-based Monitoring Framework for IoT Applications;In: C. Artho and P.C. Olveczky (Eds.), Formal Techniques for Safety-Critical Systems, Communications in Computer and Information Science 694, Springer, 2017, pp. 93-108. [Proc. International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS'16), Tokyo, Japan, November 2016]
- A. Ahmed, O. Hasan, S. Tahar, and A. Mohamed: Formal Verification of Energy Consumption for an EEG Monitoring Wireless Body Area Sensor Network; [Proc. IEEE International Conference on Open-Source Systems and Technologies (ICOSST'16), Lahore, Pakistan, December 2016, pp. 18-22.]
- M. Elleuch, O. Hasan, S. Tahar and M. Abid: Towards the Formal Performance Analysis of Wireless Sensor Networks; In: M. Ghaze and M. Jmaiel (Eds.), Verification and Evaluation of Computer and Communication Systems, CEUR Workshop Proceedings 1689, 2016, pp.23-58. [Proc. International Workshop on Verification and Evaluation of Computer and Communication Systems (VECoS'16), La Marsa, Tunisia, October 2016]
- W. Ahmed, O. Hasan and S. Tahar: Towards Formal Reliability Analysis of Logistics Service Supply Chains using Theorem Proving; In: B. Konev, S. Schulz and L. Simon (Eds.), International Workshop on the Implementation of Logics, EPiC Series in Computing 40, 2016, pp. 1-14. [Proc. International Workshop on the Implementation of Logics (IWIL'15), Suva, November 2015]
- M. Qasim, O. Hasan, M. Elleuch and S. Tahar: Formalization of Normal Random Variables in HOL; In: M. Kohlhase, M. Johansson, B. Miller, L. de Moura, L., F. Tompa (Eds.), Intelligent Computer Mathematics, Lecture Notes in Computer Science Volume 9791, pp. 44-59. [Proc. Conference of Intelligent Computer Mathematics (CICM'16), Bialystok, Poland, July 2016]
- W. Ahmed, O. Hasan, and S. Tahar: Formal Dependability Modeling and Analysis: A Survey; In: M. Kohlhase, M. Johansson, B. Miller, L. de Moura, L., F. Tompa (Eds.), Intelligent Computer Mathematics, Lecture Notes in Computer Science Volume 9791, pp. 132-147. [Proc. Conference of Intelligent Computer Mathematics (CICM'16), Bialystok, Poland, July 2016]
- S. M. Beillahi, M.Y. Mahmoud and S. Tahar: Hierarchical Verification of Quantum Circuits In: S. Rayadurgam and O. Tkachuk (Eds.), NASA Formal Methods Symposium, Lecture Notes in Computer Science 9690, Springer Verlag, 2016, pp. 344-352. [Proc. NASA Formal Methods Symposium (NFM'16), Minneapolis, MN, USA, June, 2016]
- I. Seghaier, M. H. Zaki and S. Tahar: Cross Recurrence Verification Technique for Process Variation-Resilient Analog Circuits;[Proc. IEEE International Symposium on Circuits and Systems (ISCAS'16), Montreal, Quebec, Canada, May 2016, pp. 1294-1297].
- M. Soualhia, F. Khomh, and S. Tahar: ATLAS: An Adaptive Failure-Aware Scheduler for Hadoop; [Proc. IEEE International Performance Computing and Communications Conference (IPCCC'15), Nanjing, China, December 2015, pp. 1-8.].
- S. M. Beillahi, U. Siddique and S. Tahar: Formal Analysis of Power Electronic Systems. In: M. Butler S. Conchon and F. Zaïdi (Eds.), Formal Methods and Software Engineering, Lecture Notes in Computer Science 9407, 2015, pp. 270-286. [Proc. International Conference on Formal Engineering Methods (ICFEM'15), Paris, France, November, 2015]
- A. Mohamed, M.S. Hamdi and S. Tahar: An Adaptive Neuro-Fuzzy Inference System-based Approach for Oil and Gas Pipeline Defect Depth Estimation; [Proc. IEEE SAI Intelligent Systems Conference (IntelliSys'15), London, UK, November 2015. pp. 35-42.].
- W. Ahmed, O. Hasan and S. Tahar: Formal Reliability Analysis of Wireless Sensor Network Data Transport Protocols using HOL; [ Proc. IEEE International Conference on Wireless and Mobile Computing, Networking and Communications (WiMob'15), Abu Dhabi, UAE, October 2015, pp. 225-2325].
- V.A. De Santiago and S. Tahar: Time Performance Formal Evaluation of Complex Systems; In: M. Cornelio and B. Roscoe (Eds.), Formal Methods: Foundations and Applications, Lecture Notes in Computer Science 9526, Springer Verlag, 2016, pp. 162-177. [Proc. Brazilian Symposium on Formal Methods (SBMF'15), Belo Horizonte, Brazil, September, 2015]. [
**3rd BEST PAPER**] - M. Soualhia, F. Khomh, and S. Tahar: Predicting Scheduling Failures in the Cloud: A Case Study with Google Clusters and Hadoop on Amazon EMR; [Proc. IEEE High Performance Computing and Communications (HPCC'15), New York, USA, August 2015, pp. 58-65]
- A. Mohamed, M. S. Hamdi and S. Tahar: A Machine Learning Approach for Big Data in Oil and Gas Pipelines; [Proc. IEEE International Conference on Future Internet of Things and Cloud (FiCloud'15), Rome, Italy, August, 2015, pp. 585-590]
- A. Mohamed, M. S. Hamdi and S. Tahar: Self-Organizing Map-Based Feature Visualization and Selection for Defect Depth Estimation in Oil and Gas Pipelines; [Proc. IEEE International Conference Information Visualisation (iV'15), Barcelona, Spain, July 2015, pp. 235-240]
- C. Kaliszyk, J. Urban, U. Siddique, S. Khan-Afshar, C. Dunchev and S. Tahar: Formalizing Physics: Automation, Presentation and Foundation Issues; In: M. Kerber, J. Carette, C. Kaliszyk, F. Rabe and V. Sorge (Eds.), Intelligent Computer Mathematics, Lecture Notes in Computer Science Volume 9150, pp 288-295 [Proc. Conference of Intelligent Computer Mathematics (CICM'15), Washington, DC, July, 2015]
- U. Siddique, O. Hasan and S. Tahar: Towards the Formalization of Fractional Calculus in Higher-Order Logic; In: M. Kerber, J. Carette, C. Kaliszyk, F. Rabe and V. Sorge (Eds.), Intelligent Computer Mathematics, Lecture Notes in Computer Science Volume 9150, pp 316-324 [Proc. Conference of Intelligent Computer Mathematics (CICM'15), Washington, DC, July, 2015]
- O. Seddiki, C. Dunchev, S. Khan-Afshar, S. Tahar: Enabling Symbolic and Numerical Computations in HOL Light; In: M. Kerber, J. Carette, C. Kaliszyk, F. Rabe and V. Sorge (Eds.), Intelligent Computer Mathematics, Lecture Notes in Computer Science Volume 9150, pp 353-358 [Proc. Conference of Intelligent Computer Mathematics (CICM'15), Washington, DC, July, 2015] [
**BEST PAPER**] - I. Seghaier, M.H. Zaki and S. Tahar: A Statistical Approach to Probe Chaos from Noise in Analog and Mixed Signal Designs.; [ Proc. IEEE Computer Society Annual Symposium on VLSI (ISVLSI '15), Montpellier, France, July 2015, pp. 237-242. [
**BEST PAPER**] - O. Lahiouel, M. H. Zaki, and S. Tahar: Towards Enhancing Analog Circuits Sizing using SMT-based Techniques.; [Proc. Design Automation Conference (DAC '15), San Francisco, California, USA, June 2015, pp. 1-6]
- U. Siddique, S. M. Beillahi and S. Tahar: On the Formal Analysis of Photonic Signal Processing Systems; In: M. Nunes and M. Gudemann (Eds.), Formal Methods for Industrial Critical Systems, Lecture Notes in Computer Science 9128, 2015, pp. 162-177. [Proc. Formal Methods for Industrial Critical Systems (FMICS'15), Oslo, Norway, June, 2015]
- M. Y. Mahmoud, P. Panangaden, and S. Tahar: On the Formal Verification of Optical Quantum Gates in HOL; In: M. Nunes and M. Gudemann (Eds.), Formal Methods for Industrial Critical Systems, Lecture Notes in Computer Science 9128, 2015, pp. 198-211. [Proc. Formal Methods for Industrial Critical Systems (FMICS'15), Oslo, Norway, June, 2015]
- I. Seghaier, M. H. Zaki, and S. Tahar:Statistically Validating the Impact of Process Variations on Analog and Mixed Signal Designs. [Proc. Great Lakes Symposium on VLSI (GLSVLSI'15), Pittsburgh, Pennsylvania, USA, May 2015, pp. 99-102.]
- S.M. Beillahi, M.Y. Mahmoud and S. Tahar:A Tool for the Formal Verification of Quantum Optical Computing Systems. [Proc. Automated Reasoning Workshop (ARW'15), Birmingham, United Kingdom, April, 2015, pp. 25-26.]
- U. Siddique, O. Hasan, and S. Tahar: Formal Modeling and Verification of Integrated Photonic Systems. [Proceedings of IEEE International Systems Conference (SysCon'15), Vancouver, B.C., Canada, April 2015, pp. 562-569.]
- M. Nayrolles, A. Hamou-Lhadj, S. Tahar and A. Larsson: JCHARMING: A Bug Reproduction Approach Using Crash Traces and Directed Model Checking. Proc. IEEE International Conference on Software Analysis, Evolution, and Reengineering (SANER’15), Montreal, Quebec, Canada, March 2015, pp. 101-110. [
**BEST PAPER**] ; - U. Siddique and S. Tahar: On the Formalization of Cardinal Points of Optical Systems [In: T. Bouabana-Tebibel and H. S. Rubin (Eds.), Formalisms for Reuse and Systems Integration, Advances in Intelligent Systems and Computing, Volume 346, Springer 2015, pp. 79-102]
- O. Hasan, W. Ahmed, S. Tahar and M. S. Hamdi: Reliability Block Diagrams based Analysis: A Survey, Numerical Analysis and Applied Mathematics , AIP Conference Proceedings Vol. 1648, 2014, pp. 850129.1-4. [Proc. International Conference of Numerical Analysis and Applied Mathematics (ICNAAM'14), Rhodes, Greece, September 2014]
- U. Siddique and S. Tahar: Towards Ray Optics Formalization of Optical Imaging Systems [Proceedings of IEEE International Conference on Information Reuse and Integration (IRI'14), San Francisco, California, USA, 2014, pp. 378-385.]
- M. Layouni, S. Tahar and M.S. Hamdi: On the Application of Neural Networks in the Safety Assessment of Oil and Gas Pipelines: A Survey;Proc. IEEE Symposium on Computational Intelligence for Engineering Solutions (CIES’14), Orlando, Florida, USA, December 2014, pp. 95-102.
- L. Liu, V. Aravantinos, O. Hasan, and S. Tahar: On the Formal Analysis of HMM using Theorem Proving; In: S. Merz and J. Pang (Eds.), Formal Methods and Software Engineering, Lecture Notes in Computer Science 8829, Springer Verlag, 2014, pp. 316.331. [Proc. International Conference on Formal Engineering Methods (ICFEM.14), Luxembourg, Luxembourg, November 2014.]
- U. Pervez, O. Hasan, K. Latif, S. Tahar, A. Gawanmeh, and M.S. Hamdi: Formal Reliability Analysis of a Typical FHIR Standard based E-Health System using PRISM; Proc. IEEE International Conference on e-Health Networking, Applications and Services (HEALTHCOM’14), Natal, Brazil, October 2014, pp. 43-48
- S. Ahmad, O. Hasan, U. Siddique and S. Tahar: Formalization of Zsyntax to Reason About Molecular Pathways in HOL4; In: C. Braga N. Mart-Oliet (Eds.), Formal Methods: Foundations and Applications, Lecture Notes in Computer Science 8941, Springer Verlag, 2014, pp 32-47. [Proc. of The Brazilian Symposium on Formal Methods (SBMF'14), Maceio, Alagoas, Brazil, September 2014]
- S.K. Afshar, O. Hasan and S. Tahar: Formal Analysis of Electromagnetic Optics; [In: G.G. Gregory, A.J. Davis (Eds.), Novel Optical Systems Design and Optimization XVII (SPIE'14), Proceedings of SPIE 9193, 2014, pp. 91930A1-91930A14]
- U. Siddique, M. Y. Mahmoud and S. Tahar: On the Formalization of Z-Transform in HOL G. Klein and R. Gamboa (Eds.), Interactive Theorem Proving,Lecture Notes in Computer Science Volume 8558, 2014, pp 483-498. [Proc. Conference on Interactive Theorem Proving (ITP'14), Vienna, Austria, July 2014]
- M. Y. Mahmoud, V. Aravantinos and S. Tahar: Formal Verification of Optical Quantum Flip Gate G. Klein and R. Gamboa (Eds.), Interactive Theorem Proving, Lecture Notes in Computer Science Volume 8558, 2014, pp 358-373. [Proc. Conference on Interactive Theorem Proving (ITP'14), Vienna, Austria, July 2014]
- V. Aravantinos and S. Tahar: Implicational Rewriting Tactics in HOL G. Klein and R. Gamboa (Eds.), Interactive Theorem Proving, Lecture Notes in Computer Science Volume 8558, 2014, pp 45-60. [Proc. Conference on Interactive Theorem Proving (ITP'14), Vienna, Austria, July 2014]
- S. M. Beillahi, U. Siddique and S. Tahar: Towards the Application of Formal Methods in Process Engineering[Proc. 2nd International Workshop on Fun With Formal Methods , Vienna, Austria, July 2014, pp 1-11]
- S. Khan-Afshar, V. Aravantinos, O. Hasan, and S. Tahar: Formalization of Complex Vectors in Higher-Order Logic S.M. Watt et al. (Eds.), Intelligent Computer Mathematics, Lecture Notes in Computer Science 8543, Springer, 2014, pp 123-137. [Proc. Conference on Intelligent Computer Mathematics (CICM'14), Coimbra, Portugal, July 2014]
- U. Siddique and S. Tahar: A Framework for Formal Reasoning about Geometrical Optics S.M. Watt et al. (Eds.), Intelligent Computer Mathematics, Lecture Notes in Computer Science 8543, Springer, 2014, pp 453-456. [Proc. Conference on Intelligent Computer Mathematics (CICM'14), Coimbra, Portugal, July 2014]
- W. Ahmed, O. Hasan, S. Tahar, M. S. Hamdi: Towards the Formal Reliability Analysis of Oil and Gas Pipelines S.M. Watt et al. (Eds.), Intelligent Computer Mathematics, Lecture Notes in Computer Science 8543, Springer, 2014, pp 30-44. [Proc. Conference on Intelligent Computer Mathematics (CICM'14), Coimbra, Portugal, July 2014]
- O.Lahiouel, H. Aridhi, M. H. Zaki, and S. Tahar: Enabling the DC Solutions Characterization using a Fuzzy Approach[Proc. IEEE New Circuits and Systems Conference (NEWCAS'14), Trois-Rivières, Quebec, Canada, June 2014, pp. 161-164.]
- S. K. Afshar, O. Hasan, and S. Tahar: Towards the Formal Verification of Optical Interconnects[Proc. IEEE New Circuits and Systems Conference (NEWCAS'14), Trois-Rivières, Quebec, Canada, June 2014, pp. 157-160.]
- P. Winkler, H. Aridhi, M. H. Zaki, and S. Tahar: Generation of Reduced Analog Circuit Models Using Transient Simulation Traces [Proc. Great Lakes Symposium on VLSI (GLSVLSI'14), Houston, Texas, USA, May 2014, pp. 305-310.]
- I. Seghaier, H. Aridhi, M. H. Zaki, and S. Tahar: A Qualitative Simulation Approach for Verifying PLL Locking Property [Proc. Great Lakes Symposium on VLSI (GLSVLSI'14), Houston, Texas, USA, May 2014, pp. 317-322.]
- O.Lahiouel, H. Aridhi, M. H. Zaki, and S. Tahar: A Semi-Formal Approach for Analog Circuits Behavioral Properties Verification [Proc. Great Lakes Symposium on VLSI (GLSVLSI'14), Houston, Texas, USA, May 2014, pp. 247-248.]
- A. Souari, M.L. Ammari, A. Gawanmeh, and S. Tahar: Performance Evaluation of Time and Frequency Domain Equalizers [Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'14), Toronto, Ontario, Canada, May 2014, pp. 1213-1218.]
- A. Gawanmeh and S. Tahar: Real Time Verification of Firewalls with Dynamic Rulebase Update [Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'14), Toronto, Ontario, Canada, May 2014, pp. 276-281.]
- M. Y. Mahmoud, and S. Tahar: On the Quantum Formalization of Coherent Light in HOL [In: J. M. Badger, K. Y. Rozier (Eds.), NASA Formal Methods Symposium (NFM'14), Lecture Notes in Computer Science 8430 , Springer Verlag, 2014, pp. 128-142]
- U. Siddique and S. Tahar: Towards the Formal Analysis of Microresonators based Photonic Systems [In: IEEE/ACM Design Automation and Test in Europe (DATE'14), Dresden, Germany, March 2014, pp. 1-6]
- G. Helali, O. Hasan, and S. Tahar: Formal Analysis of Information Flow Using Min-Entropy and Belief Min-Entropy In: J. Iyoda and L. de Moura (Eds.) Formal Methods: Foundations and Applications, Lecture Notes in Computer Science 8195, Springer Verlag, 2013, pp. 131-146. [Proc. of The Brazilian Symposium on Formal Methods (SBMF'13), Brasilia, Brazil, September 2014]. [
**BEST PAPER**] - L. Liu, O. Hasan, and S. Tahar: Formal Analysis of Memory Contention in a Multiprocessor System In: J. Iyoda and L. de Moura (Eds.) Formal Methods: Foundations and Applications, Lecture Notes in Computer Science 8195, Springer Verlag, 2013, pp. 195-210. [Proc. of The Brazilian Symposium on Formal Methods (SBMF'13), Brasilia, Brazil, September 2014]
- M. Elleuch, O. Hasan, S. Tahar and M. Abid: Towards the Formal Performance Analysis of Wireless Sensor Networks [Proc. IEEE International Workshop on Enabling Technologies: Infrastructures for Collaborative Enterprises (WETICE.13), Hammamet, Tunisia, June 2013, pp. 365-370] [
**BEST PAPER**] - M. Elleuch, O. Hasan, S. Tahar and M. Abid: Formal Probabilistic Analysis of a Wireless Sensor Network for Forest Fire Detection [In. A. Bouhoula, T. Ida and F. Kamareddine (Eds.), Symbolic Computation in Software Science (SCSS'12), Electronic Proceedings in Theoretical Computer Science 122, 2013, pp. 1-9.]
- S. Al-Akhras, S. Tahar, G. Nicolescu, M. Langevin and P. Paulin: On the Verification of a WiMax Design using Symbolic Simulation [In. A. Bouhoula, T. Ida and F. Kamareddine (Eds.), Symbolic Computation in Software Science (SCSS'12), Electronic Proceedings in Theoretical Computer Science 122, 2013, pp. 23.37.]
- N. Abbasi, O. Hasan and S. Tahar: Formal Analysis of Soft Errors using Theorem Proving [In. A. Bouhoula, T. Ida and F. Kamareddine (Eds.), Symbolic Computation in Software Science (SCSS'12), Electronic Proceedings in Theoretical Computer Science 122, 2013, p. 75.84.]
- U. Siddique, V. Aravantinos, and S. Tahar: A New Approach for the Verification of Optical Systems [In: J. Sasin and R.N. Youngworth (Eds.), Optical System Alignment, Tolerancing, and Verification VII (SPIE'13), Proceedings of SPIE 8844, 2013, pp. 88440G1-88440G-14]
- U. Siddique, V. Aravantinos, and S. Tahar: On the Formal Analysis of Geometrical Optics in HOL [In: T. Ida and J. Fleuriot (Eds.), Automated Deduction in Geometry, Lecture Notes in Computer Science 7993, Springer Verlag, 2013, pp. 161-180.]
- L. Liu, O. Hasan, V. Aravantinos, and S. Tahar: Formal Reasoning about Classified Markov Chains in HOL [In: S. Blazy, C. Paulin-Mohring, D. Pichardie, Interactive Theorem Proving (ITP.13), Lecture Notes in Computer Science 7998, Springer Verlag, 2013, pp. 295-310.]
- U. Siddique, V. Aravantinos, and S. Tahar: Formal Stability Analysis of Optical Resonators [In: G. Brat, N. Rungta, and A. Venet (Eds.), NASA Formal Methods Symposium (NFM'13), Lecture Notes in Computer Science 7871, Springer Verlag, 2013, pp. 368-382.]
- M.Y. Mahmoud, V. Aravantinos, and S. Tahar: Formalization of Infinite Dimension Linear Spaces with Application to Quantum Theory [In: G. Brat, N. Rungta, and A. Venet (Eds.), NASA Formal Methods Symposium (NFM'13), Lecture Notes in Computer Science 7871, Springer Verlag, 2013, pp. 413-427.]
- M.Y. Mahmoud, V. Aravantinos and S. Tahar: Towards the Formal Verification of Quantum Optical Systems [Proc. International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS.12), Kyoto, Japan, November 2012, pp. 147-151.]
- T. Mhamdi, O. Hasan, and S. Tahar: Quantitative Analysis of Information Flow using Theorem Proving [In: T. Aoki and K. Tagushi (Eds.), Formal Methods and Software Engineering (ICFEM'12), Lecture Notes in Computer Science 7635, Springer Verlag, 2012, pp. 119-134.]
- U. Siddique, V. Aravantinos and S. Tahar: Higher-Order Logic Formalization of Geometrical Optics [In: T. Ida and J. Fleuriot (Eds.), Automated Deduction in Geometry (ADG'12), Informatics Research Report, School of Informatics, University of Edinburgh, Edinburgh, UK, September 2012, pp. 184-196.]
- R. Narayanan, A. Daghar, M. H. Zaki and S. Tahar: Using LCSS Algorithm for Circuit Level Verification of Analog Designs [Proc. IEEE New Circuits and Systems Conference (NEWCAS'12), Montreal, Quebec, Canada, June 2012, pp. 185-188.]
- A. Souari, S. Tahar and A. Gawanmeh: Formal Error Analysis and Verification of a Frequency Domain Equalizer [Proc. IEEE New Circuits and Systems Conference (NEWCAS'12), Montreal, Quebec, Canada, June 2012, pp. 189-192.]
- T.L. Ben Cheikh, G. Beltrame, G. Nicolescu, F. Cheriet, and S. Tahar: Parallelization Strategies of the Canny Edge Detector for Multi-Core CPUs and Many-Core GPUs [Proc. IEEE New Circuits and Systems Conference (NEWCAS'12), Montreal, Quebec, Canada, June 2012, pp. 49-52]
- A. Gawanmeh and S. Tahar:A Novel Algorithm for Detecting Conflicts in Firewall Rules [Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'12), Montreal, Quebec, Canada, May 2012]
- G. Helali, O. Hasan, and S. Tahar:Formal Verification of the Heavy Hitter Problem [Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'12), Montreal, Quebec, Canada, May 2012]
- H. Aridhi, M. H. Zaki and S. Tahar:Towards Improving Simulation of Analog Circuits Using Model Order Reduction [Proc. IEEE/ACM Design Automation and Test in Europe (DATE'12), Dresden, Germany, March 2012, pp. 1337-1342.]
- R. Narayanan, A. Daghar, M. H. Zaki and S. Tahar: Verifying Jitter in an Analog and Mixed Signal Design Using Dynamic Time Warping [Proc. IEEE/ACM Design Automation and Test in Europe (DATE'12), Dresden, Germany, March 2012, pp. 1413-1416.]
- L. Liu, O. Hasan, and S. Tahar:Formalization of Finite-state Discrete-Time Markov Chains in HOL Automated Technology for Verification and Analysis, Lecture Notes in Computer Sciences 6996, Springer-Verlag, 2011, pp. 90-104. [ Proc. 9th International Symposium on Automated Technology for Verification and Analysis (ATVA '2011), Taipei, Taiwan, November 2011.]
- M. Elleuch, O. Hasan, S. Tahar and M. Abid:Formal Analysis of a Scheduling Algorithm for Wireless Sensor Networks International Conference on Formal Engineering Methods, Lecture Notes in Computer Science 6191, Springer Verlag, 2011, pp. 388-403. [Proc. 13th International Conference on Formal Engineering Methods (ICFEM '2011), Durham, United Kingdom, October 2011.]
- A. Gawanmeh and S. Tahar:Modeling and Verification of Firewall Configurations Using Domain Restriction Method [Proc. Computer Society Press, IEEE/ACM International Conference on Internet Technology and Secured Transactions (ICITST'2011), Dubai, UAE, December 2011, pp. 642.647.]
- T. Mhamdi, O. Hasan, and S. Tahar: Formalization of Entropy Measures in HOL M. V. Eekelen, H. Geuvers, J. Schmaltz and F. Wiedijk (Eds.), Interactive Theorem Proving, Lecture Notes in Computer Science 6898, Springer Verlag, 2011, pp. 233-248. [Proc. Second International Conference on Interactive Theorem Proving (ITP 2011), Berg en Dal, The Netherlands, August 2011.]
- W. Denman, M. H. Zaki, S. Tahar and L. Rodrigues:Towards Flight Control Verification using Automated Theorem Proving M.G. Bobaru, K. Havelund, G.J. Holzmann, R. Joshi (Eds.), NASA Formal Methods, Lecture Notes in Computer Science 6617, Springer Verlag, 2011, pp. 84-97. [Proc. Third International NASA Formal Methods (NFM 2011), Pasadena, CA, USA, April 2011.]
- R. Narayanan, M. Zaki, and S. Tahar: Ensuring Correctness of Analog Circuits in the Presence of Noise and Process Variation Using Pattern Matching [Proc. IEEE/ACM Design Automation and Test in Europe (DATE'11), Grenoble, France, March 2011, pp. 1188-1191.]
- N. Abbasi, O. Hasan, S. Tahar: Formal Lifetime Reliability Analysis using Continuous Random Variables A. Dawar, R. Queiroz (Eds.), Logic, Language, Information and Computation, Lecture Notes in Artificial Intelligence 6188, Springer Verlag, 2010, pp. 84-97. [Proc. 17th International Workshop on Logic, Languages, Information and Computing (WoLLIC-2010), Brasilia, Brazil, July 2010.]
- T. Mhamdi, O. Hasan, and S. Tahar: On the Formalization of the Lebesgue Integration Theory in HOL M. Kaufmann, L. C. Paulson (Eds.), Interactive Theorem Proving, Lecture Notes in Computer Science 6172, Springer Verlag, 2010, pp. 387-402. [Proc. First International Conference on Interactive Theorem Proving (ITP 2010), Edinburgh, UK, July 2010.]
- O. Hasan, J. Patel, and S. Tahar: On the Accurate Reliability Analysis of Combinational Circuits using Theorem Proving [Proc. IEEE New Circuits and Systems Conference (NEWCAS'10), Montreal, Quebec,Canada, June 2010, pp. 273-276.]
- J. Ben Hassan, O. Hasan, T. Sadani, and S. Tahar: Performance Analysis of Real-Time Rewriting Models [
*Proc. International Conference on Computer Systems and Applications (AICCSA'2010)*, 2010 ACS/IEEE, , Hammamet Tunisia, May 16-19th, 2010.] - R. Narayanan, M. Zaki, B. Akbarpour, S. Tahar, and L. Paulson: Formal Verification of Analog/RF Circuits in the Presence of Noise and Process Variation [
*Proc. IEEE/ACM Design Automation and Test in Europe (DATE'10)*, Dresden, Germany, March 2010, pp. 1309-1312.] - O. Hasan and S. Tahar: Formal Probabilistic Analysis: The Higher-Order Logic Based Approach M. Frappier, U. Glaeser, S. Khurshid, R. Laleau, and S. Reeves (Eds.),
*Abstract Satte Machines, Alloy, B and Z*, Lecture Notes in Computer Science 5977, Springer Verlag, 2010, pp. 2-19. [*Proc. International Conference on Abstract Satte Machines, Alloy, B and Z (ABZ'10)*, Orford, Quebec, Canada, February 2010.] - Z. Wang, M. Zaki, S. Tahar: Statistical Runtime Verification of Analog and Mixed Designs [Proc. IEEE International Conference on Signals, Circuits and Systems (SCS.09), Djerba, Tunisia, November 2009, pp. 1-6.]
- W. Denman, B. Akbarpour, S. Tahar, M. Zaki, L. Paulson: Formal Verification of Analog Designs using MetiTarski [Proc. IEEE International Conference on Formal Methods in CAD (FMCAD'09), Austin, Texas, USA, November 2009, pp. 93-100, IEEE Computer Society Press.]
- O. Hasan, N. Abbasi, B. Akbarpour, S. Tahar, and R. Akbarpour: Formal Reasoning about Expectation Properties for Continuous Random Variables A. Cavalcanti and D. Dams (Eds.), Formal Methods, Lecture Notes in Computer Science 5850, Springer Verlag, 2009, pp. 435-450. [Proc. International Symposium on Formal Methods (FM'09) , Eindhoven, The Netherlands, November 2009.]
- O. Hasan, S.K. Afshar, and S. Tahar: Formal Analysis of Optical Waveguides in HOL S. Berghofer et al. (Eds.), Theorem Proving in Higher-Order Logics, Lecture Notes in Computer Science 5674, Springer Verlag, 2009, pp. 228-243. [Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'09), Munich, Germany, August 2009.]
- S. Albasheir, S. Tahar, C. Gauthier, and J. Personna: Radio Access Network Traffic Generation for Mobile Switching Center [Proc. IEEE Symposium on Computers and Communications (ISCC'09), Sousse, Tunisia, July 2009, pp. 705-710.]
- Z. Wang, N. Abbasi, R. Narayanan, G. Al Sammane, M. Zaki, and S. Tahar : Verification of Analog and Mixed Signal Designs using Online Monitoring [Proc. IEEE International Mixed-Signals, Sensors, and Systems Test Workshop (IMS3TW'09), Scottsdale, Arizona, USA, June 2009, pp. 1-8.]
- A.M. Taha, A.T. Abdel-Hamid, and S. Tahar: Formal Verification of IEEE 802.16 Security Sublayer Using Scyther Tool [Proc. IFIP International Conference on Network and Service Security (N2S'09), Paris, France, June 2009, pp. 1-6.]
- R. Narayanan, M. Zaki, and S. Tahar: Using Stochastic Differential Equation for Assertion Based Verification of Noise in Analog/RF Circuits [Proc. IEEE International Mixed-Signals, Sensors, and Systems Test Workshop (IMS3TW'09), Scottsdale, Arizona, USA, June 2009, pp. 1-8.]
- A.M. Taha, A.T. Abdel-Hamid, and S. Tahar: Formal Analysis of the Handover Schemes in Mobile WiMAX Networks [Proc. IEEE International Conference on Wireless and Optical Communications Networks (WCON'09), Cairo, Egypt, April 2009, pp. 1-5.]
- N. Abbasi, O. Hasan and S. Tahar: Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays M. Leuschel and H. Wehrheim (Eds.), Integrated Formal Methods, Lecture Notes in Computer Science 5423, Springer Verlag, 2009, pp. 277-291. [Proc. International Conference on Integrated Formal Methods (IFM'09), Dusseldorf, Germany, February 2009.]
- R. Narayanan, N. Abbasi, M. Zaki, G. Al Sammane, and S. Tahar: On the Simulation Performance of Contemporary AMS Hardware Description Languages [Proc. IEEE International Conference on Microelectronics (ICM'08), Sharjah, UAE, December 2008, pp. 390-393.]
- A. Gawanmeh, L. Jemni and S. Tahar: Event-B based Invariant Checking of Secrecy in Group Key Protocols [Proc. IEEE LCN Workshop on Network Security (WNS'08), Montreal, Quebec, Canada, October 2008, IEEE Computer Society Press.]
- Y. Mokhtari, S. Abed, O. Ait Mohamed, S. Tahar, and X. Song: A New Approach for the Construction of Multiway Decision Graphs J.S. Fitzgerald, A.E. Haxthausen, and H. Yenigun (Eds.), Theoretical Aspects of Computing, Lecture Notes in Computer Science 5160, Springer Verlag 2008, pp. 228-242. [Proc. International Colloquium on Theoretical Aspects of Computing (ICTAC'08), Istanbul, Turkey, September 2008.]
- O. Hasan and S. Tahar: Probabilistic Analysis of Wireless Systems using Theorem Proving [Proc. Formal Methods in Wireles Systems (FMWS'08), Toronto, Ontario, Canada, August 2008, pp. 3-18.]
- A. Nasser, B. Akbarpour and S. Tahar: Error Analysis and Verification of an IEEE 802.11 OFDM Modem using Theorem Proving [Proc. Formal Methods in Wireles Systems (FMWS'08), Toronto, Ontario, Canada, August 2008, 43-63.]
- A.T. Abdel-Hamid and S. Tahar: Fragile IP Watermarking Techniques [Proc. NASA/ESA Conference on Adaptive Hardware and Systems (AHS'08), July 2008, Noordwijk, The Netherlands, IEEE Computer Society Press, pp. 513-519.]
- R. Narayanan, N. Abbasi, G. Al Sammane, M. Zaki, and S. Tahar: A Comparative Study of AMS Circuit Simulation in VHDL-AMS and SystemC-AMS [Proc. International Conference on Embedded Systems & Critical Applications (ICESCA'08), Gammarth, Tunisia, May 2008, pp. 23-28.]
- W. Denman, M. Zaki and S. Tahar: A Bond Graph Approach for the Constraint based Verification of Analog Circuits [Proc. Workshop on Formal Verification of Analog Circuit (FAC'08), July 2008, Princeton, New Jersey, USA, pp. 1-28.]
- O. Hasan and S. Tahar: Performance Analysis of ARQ Protocols using a Theorem Prover IEEE International Symposium on Performance Analysis of Systems and Software (ISPASS’08), Austin, Texas, USA, April 2008, IEEE Computer Society Press, pp 85-94.
- M. Zaki, S. Tahar, and G. Bois: Qualitative Abstraction based Verification for Analog Circuits [Proc. Workshop On Leveraging Applications of Formal Methods, Verification and Validation (ISOLA'07), Poitier, France, December 2007, pp. 147-158]
- T.H. Khan, A. Habibi, S. Tahar and O. A. Mohamed:Automatic Generation of SystemC Transactors from Graphical FSM In Proc. IEEE International Conference on Microelectronics (ICM’07), Cairo, Egypt, December 2007. pp. 271-274.
- Z.J. Dong, M.H. Zaki, G. Al Sammane, S. Tahar and G. Bois: Checking Properties of PLL Designs using Run-time Verification; Proc. IEEE International Conference on Microelectronics (ICM’07), Cairo, Egypt, December 2007, pp. 129-132.
- O.Hasan and S. Kort. Automated Formal Synthesis of Wallace Tree Multipliers [Proc. IEEE Midwest Symposium on Circuits & Systems (MWSCAS'07), Montreal, Quebec, Canada, August 2007, pp. 293-296.]
- M. Zaki, G. Al Sammane, S. Tahar, and G. Bois: Combining Symbolic Simulation and Interval Arithmetic for the Verification of AMS Designs [Proc. IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD'07), Austin, Texas, USA, November 2007, IEEE Computer Society Press. pp. 207-215.]
- O. Hasan and S. Tahar: Verification of Tail Distribution Bounds in a Theorem Prover T.E.Simos, G. Psihoyios and Ch. Tsitouras (Eds.), Numerical Analysis and Applied Mathematics, AIP Conference Proceedings Vol.936, 2007, pp. 259-262. [Proc. International Conference of Numerical Analysis and Applied Mathematics (ICNAAM'07), Corfu, Greece, September 2007.]
- G. Al Sammane, M.H. Zaki, Z.J. Dong and S. Tahar: Towards Assertion Based Verification of Analog and Mixed Signal Designs Using PSL [Proc. Languages for Formal Specification and Verification, Forum on Specification & Design Languages (FDL'07), Barcelona, Spain, September 2007, pp. 293-298.]
- T.H. Khan, A. Habibi, S. Tahar and O. Ait Mohamed: Automatic Generation of SystemC Transactors from AsmL Specification [Proc. Languages for Formal Specification and Verification, Forum on Specification & Design Languages (FDL'07), Barcelona, Spain, September 2007. pp. 104-109.]
- O. Hasan and S. Tahar: Verification of Expectation Properties for Discrete Random Variables in HOL K.Schneider and J.Brandt (Eds.), Theorem Proving in Higher-Order Logics, Lecture Notes in Computer Science 4732, Springer Verlag, 2007, pp. 119-134. [Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'07), Kaiserslautern, Germany, September 2007.]
- Z.J. Dong, M. Zaki, G. Al Sammane, S. Tahar, and G. Bois: Run-Time Verification using the VHDL-AMS Simulation Environment [Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'07), Montreal, Quebec, Canada, August 2007, pp. 1513-1516.]
- G. Al Sammane, M. Zaki, S. Tahar, and G. Bois: Constraint-Based Verification of Delta Sigma Modulators Using Interval Analysis [Proc. IEEE Midwest Symposium on Circuits & Systems (MISWEST'07), Montreal, Quebec, Canada, August 2007, pp. 726-729.]
- O. Hasan and S. Tahar: Formalization of Continuous Probability Distributions F. Pfenning (Ed.), Automated Deduction, Lecture Notes in Computer Science 4603, Springer Verlag, 2007, pp. 2-18. [Proc. 21st Conference on Automated Deduction (CADE-21), Bremen, Germany, July 2007.]
- O. Hasan and S. Tahar: Verification of Probabilistic Properties in the HOL Theorem Prover J. Davies and J. Gibbons (Eds.), Integrated Formal Methods, Lecture Notes in Computer Science 4591, Springer Verlag, 2007, pp. 333-352. [Proc. International Conference on Integrated Formal Methods (IFM'07), Oxford, UK, July 2007.]
- M. Zaki, G. Al Sammane, and S. Tahar: Formal Verification of Analog and Mixed Signal Designs in Mathematica Y. Shi et al. (Eds.), Computational Science, Lecture Notes in Computer Science 4488, Springer Verlag, 2007, pp. 263-267. [Proc. International Conference on Computational Science (ICCS'07), Beijing, China, May 2007]
- M. Zaki, S. Tahar, and G. Bois: A Symbolic Approach for the Safety Verification of Continuous Systems [Proc. International Conference on Computational Science (ICCS'07), Beijing, China, May 2007, pp. 93-100.]
- A. Gawanmeh and S. Tahar: Rank Theorems for Forward Secrecy in Group Key Management Protocols [Proc. IEEE International Conference on Advanced Information Networking and Applications Workshops (AINAW'07), Niagara Falls, Canada, May 2007, pp. 18-23. IEEE Computer Society Press.]
- G. Al Sammane, M. Zaki, and S. Tahar: A Symbolic Methodology for the Verification of Analog and Mixed Signal Designs [Proc. IEEE/ACM Design Automation and Test in Europe (DATE'07), Nice, France, April 2007, pp. 249-254.]
- Y.J. Shin, A. Habibi, and S. Tahar: A SystemC Transaction Level Model for MIPS R3000 Processor [Proc. Sciences of Electronics, Technologies of Information and Telecommunications (SETIT'07), Hammamet, Tunisia, March 2007, pp. 1-8.]
- A. Gawanmeh, A. Habibi, and S. Tahar: Embedding and Verification of PSL using ASM; Proc. IEEE International Workshop on System-on-Chip (IWSOC’06), Cairo, Egypt, December 2006, pp. 125-130, IEEE Computer Society Press.
- A. Samara, A. Habibi, and S. Tahar: Automated Coverage Directed Test Generation Using Cell-Based Genetic Algorithm [Proc. IEEE International High Level Design Validation and Test Workshop (HLDVT'06), Monterey, California, USA, November 2006, pp. 19-26, IEEE Computer Society Press.]
- N. Abdullah, B. Akbarpour, and S. Tahar: Formal Analysis and Verification of an OFDM Modem Design using HOL [Proc. IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD'06), San Jose, California, USA, November 2006, pp. 189-190, IEEE Computer Society Press.]
- H. Moinudeen, A. Habibi, and S. Tahar: Design for Verification of the PCI-X Bus [Proc. IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD'06), San Jose, California, USA, November 2006, pp. 187-188, IEEE Computer Society Press.]
- M. Zaki, S. Tahar, and G. Bois: Abstraction Based Verification of Analog Circuits Using Computer Algebra and Constraint Solving [Proc. IEEE International Workshop on Symbolic Methods and Applications to Circuit Design (SMACD'06), Florence, Italy, October 2006, pp. 1-8.]
- A.T. Abdel-Hamid, S. Tahar, and E.M. Aboulhamid: Finite State Machine IP Watermarking: A Tutorial [Proc. First NASA/ESA Conference on Adaptive Hardware and Systems (AHS 2006), June 2006, Istanbul, Turkey, pp. 457-464, IEEE Computer Society Press.]
- M. Zaki, S. Tahar, and G. Bois: Formal Verification of Analog and Mixed Signal Designs: Survey and Comparison [Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'06), Gatineau, Quebec, Canada, June 2006, pp. 281-284.]
- H. Moinudeen, A. Habibi, and S. Tahar: Model Based Verification of SystemC Designs [Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'06), Gatineau, Quebec, Canada, June 2006, pp. 289-292.]
- M. Zaki, S. Tahar, and G. Bois: A Practical Approach for Monitoring Analog Circuits [Proc. ACM 16th Great Lakes Symposium on VLSI (GLS-VLSI'06), Philadelphia, Pennsylvania, USA, April 2006, ACM Publications, pp. 330-335.]
- A. Habibi, H. Moinudeen, A. Samara, S. Tahar: Towards a Faster Simulation of SystemC Designs [Proc. IEEE Computer Society Annual Symposium on VLSI (ISVLSI'06), Karlsruhe, Germany, March 2006, pp. 418-419, IEEE Computer Society Press.]
- A. Habibi, S.Tahar, A. Samara, D. Li, O. Ait-Mohamed: Efficient Assertion Based Verification using TLM [Proc. IEEE/ACM Design Automation and Test in Europe (DATE'06), Munich, Germany, March 2006, pp. 106-111.]
- A. Habibi, H. Moinudeen and S. Tahar: Generating Finite State Machines from SystemC [Proc. IEEE/ACM Design Automation and Test in Europe (DATE'06), Munich, Germany, March 2006, pp. 76-81.]
- J. Ben Hassen and S. Tahar: On the Numerical Verification of Probabilistic Rewriting Systems [Proc. IEEE/ACM Design Automation and Test in Europe (DATE'06), Munich, Germany, March 2006, pp. 1223-1224.]
- A. Habibi and S. Tahar: On the Formal Verification of a SystemC Packet Switch Model [Proc. IEEE International Conference on Electronics, Circuits and Systems (ICECS'05), Gammarth, Tunisia, December 2005, Vol. 1, pp. 252-255.]
- A. Habibi and S. Tahar: An Approach for the Verification of SystemC Designs using AsmL D.A. Peled. and Y.-K. Tsay (Eds.), Automated Technology for Verification and Analysis, Lecture Notes in Computer Science 3707, Springer Verlag, 2005, pp. 69-83. [Proc. International Symposium on Automated Technology for Verification and Analysis (ATVA'05), Taipei, Taiwan, October 2005]
- M. Zaki, S. Tahar, and G. Bois: On the formal Analysis of Analog Systems using Interval Abstraction [Proc. NETCA Workshop on Verification and Theorem Proving for Continuous Systems, Oxford, UK, August 2005, pp. 42-56.]
- B. Akbarpour and S. Tahar: Incorporating Formal Methods in the Design Flow of DSP Systems [Proc. NETCA Workshop on Verification and Theorem Proving for Continuous Systems, Oxford, UK, August 2005, pp. 31-41.]
- Donglin li, A.I. Ahmed, and O. Ait Mohamed. STE Based Verification of Look-Aside Interface [Proc. IEEE Canadian Conference on Electrical and Computer Engineering (CCECE'05), Saskatoon, Saskatchewan, Canada, May 2005.]
- A. Habibi and S. Tahar: A Framework for the Verification of SystemC Transaction Level Models [Proc. 2005 Micronet Annual Workshop, Ottawa, Canada, May 2005, pp. 99-100.]
- A. Habibi and S. Tahar: Design for Verification of SystemC Transaction Level Models [Proc. IEEE/ACM Design Automation and Test in Europe (DATE'05), Munich, Germany, March 2005, pp. 560-566.]
- A. Habibi, A.I. Ahmed, O. Ait-Mohamed and S. Tahar: On the Design and Verification of the Look-Ahead Interface [Proc. IEEE/ACM Design Automation and Test in Europe (DATE'05), Munich, Germany, March 2005, pp. 290-296.]
- A. Abdel-Hamid, S. Tahar, and E.M. Aboulhamid: A Public-Key Watermarking Technique for IP Designs [Proc. IEEE/ACM Design Automation and Test in Europe (DATE'05), Munich, Germany, March 2005, pp. 330-336.]
- A. Gawanmeh, A. Habibi, and S. Tahar: Embedding and Verification of PSL using ASM [Proc. International Conference on Abstract State Machines (ASM'05), Paris, France, March 2005, pp. 201-215.]
- A. Habibi, and S. Tahar: AsmL Semantics in Fixpoint [Proc. International Conference on Abstract State Machines (ASM'05), Paris, France, March 2005, pp 233-245.]
- H. Moinudeen, A. Habibi, and S. Tahar: An Executable Specification of the PCI-X Bus Standard in AsmL [Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'05), Saskatoon, Saskatchewan, Canada, May 2005, pp. 1247-1250.]
- A. Merhebi and O. Ait Mohamed. FPGA Implementation of a Modular and Pipelined WF Scheduler for high speed OC192 Networks Conference GLSVLSI 2005 (Great Lakes Symposium on VLSI circuits) Chicago USA.
- A. Habibi and S. Tahar: On the Transformation of SystemC to AsmL using Abstract Interpretation [Proc. Int. Workshop on Abstract Interpretation for Object Oriented Languages (AIOOL'05), Paris, France, January 2005, pp. 1-11.]
- R. Mizouni, S. Tahar and P. Curzon: A Hybrid Tool Integrating HOL Theorem Proving with MDG Model Checking [Proc. IEEE International Conference on Microelectronics (ICM'04), Tunis, Tunisia, December 2004, pp. 392-395.]
- F. Fereydouni-forouzand and O. Ait Mohamed. An FPGA Implementation of a Modified Version of a RED Algorithm [Proc. IEEE International Conference on Field Programmable Technology (FPT'04), December 2004.]
- A. Merhebi and O. Ait Mohamed. A Scalable and Pipelined FPGA implementation of an OC192 WF Scheduler [Proc. IEEE International Conference on Field Programmable Technology (FPT'04), December 2004.]
- T. Mhamdi and S. Tahar: Providing Automated Verification in HOL using MDGs F. Wang (Ed.), Automated Technology for Verification and Analysis, Lecture Notes in Computer Science 3299, Springer Verlag, 2004, pp. 278-293. [Proc. International Symposium on Automated Technology for Verification and Analysis (ATVA'04), Taipei, Taiwan, November 2004]
- F. Wang, S. Tahar, and O. Ait Mohamed: First-order LTL Model Checking using MDGs F. Wang (Ed.), Automated Technology for Verification and Analysis, Lecture Notes in Computer Science 3299, Springer Verlag, 2004, pp. 441-455. [Proc. International Symposium on Automated Technology for Verification and Analysis (ATVA'04), Taipei, Taiwan, November 2004]
- B. Akbarpour and S. Tahar: A Methodology for the Formal Verification of FFT Algorithms in HOL A. Hu and A. Martin (Eds.), Formal Methods in Computer-Aided Design, Lecture Notes in Computer Science 3312, Springer Verlag, 2004, pp. 37-51. [Proc. International Conference on Formal Methods in Computer-Aided Design (FMCAD'04), Austin, Texas, USA, November 2004
- A. Habibi and S. Tahar: Towards an Efficient Assertion Based Verification of SystemC Designs [Proc. IEEE International High Level Design Validation and Test Workshop (HLDVT'04), Sonoma Valley, California, USA, November 2004, pp. 19-22.]
- A. Habibi, A. Gawanmeh and S. Tahar: Assertion Based Verification of PSL for SystemC Designs [Proc. IEEE International Symposium on System-on-Chip (SOC'04), Tampere, Finland, November 2004, pp. 177-180.]
- K. Oumalou, A. Habibi and S. Tahar: Design for verification of a PCI bus in SystemC [Proc. IEEE International Symposium on System-on-Chip (SOC'04), Tampere, Finland, November 2004, pp. 201-204.]
- A. Gawanmeh, A. Habibi and S. Tahar: Enabling SystemC Verification using Abstract State Machines [Proc. Languages for Formal Specification and Verification, Forum on Specification & Design Languages (FDL'04), Lille, France, September 2004, pp. 649-661.]
- B. Akbarpour and S. Tahar: Error Analysis of Digital Filters using Theorem Proving; In: K. Slind and G. Gopalakrishnan (Eds.), Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 3223, Springer Verlag, 2004, pp. 1-16. [Proc. International Conference on Theorem Proving in Higher in Higher-Order Logics (TPHOLs'04), Park City, Utah, USA, September 2004]
- T. Mhamdi and S. Tahar: Embedding Multiway Decision Graphs in HOL; B-Track [Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'04), Park City, Utah, USA, September 2004, pp. 121-136]
- S. Jahanpoor and O. Ait Mohamed:Automatic Generation of Model Checking Properties and Constraints from Production Based Specification [Proc. IEEE Midwest Symposium on Circuits and Systems (MWSCAS'04), July 2004.]
- M. Zaki, Y. Mokhtari and S. Tahar: SynAbs: Model Reduction Tool for Verilog Verification [Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'04), Montreal, Quebec, Canada, June 2004, pp. 57-60.]
- A. Habibi, S. Tahar and L. Halleb: Formal Verification of a Bus Structure Modeled in SystemC [Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'04), Montreal, Quebec, Canada, June 2004, pp. 61-64.]
- D. Li, M. HU, and O. Ait Mohamed:Built-In Self-Test Design of Motion Estimation Computing Array. [Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'04), Montreal, Quebec, Canada, June 2004, pp 349-352.]
- M. Krykhtin, Y. Mokhtari, O. Ait Mohamed, and X. Song:Towards Software Model Checking using MDGs [Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'04), Montreal, Quebec, Canada, June 2004, pp 345-348.]
- A.T. Abdel-Hamid, S. Tahar and E.M. Aboulhamid: A Tool for Automatic Watermarking of IP Designs [Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS'04), Montreal, Quebec, Canada, June 2004, pp. 381-384.]
- J. Ben Hassen and S. Tahar: Formal Verification of an SoC Platform Converter [Proc. IEEE International Symposium on Circuits and Systems (ISCAS'04), Vancouver, B.C., Canada, May 2004, Vol. 5, pp. 313-316.]
- A. Habibi and S. Tahar: On the Extension of SystemC by SystemVerilog Assertions [Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'04), Niagara Falls, Ontario, Canada, May 2004, Vol. 4, pp. 1869-1872.]
- A. Abdel-Hamid, M. Zaki, and S. Tahar: A tool for Converting Finite State Machine to VHDL [Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'04), Niagara Falls, Ontario, Canada, May 2004, Vol. 4, pp. 1907-1910 .]
- F. Wang, S. Tahar, and O. Ait Mohamed: Automaton based Model Checking Using Multiway Decision Graphs [Proc. 2004 Micronet Annual Workshop, Alymer, Canada, April 2004, pp. 133-134.]
- P. Hong, S. Tahar, and Y. Mokhtari: Compositional Verification of a Switch Fabric from Nortel Networks J. Dong and J. Woodcock (Eds.), Formal Engineering Methods, Lecture Notes in Computer Science 2885, pp. 560-578, Springer Verlag, 2003. [Proc. International Conference on Formal Engineering Methods (ICFEM'03), Singapore, November 2003.]
- B. Akbarpour and S. Tahar: Modeling SystemC Fixed-Point Arithmetic in HOL J. Dong and J. Woodcock (Eds.), Formal Engineering Methods, Lecture Notes in Computer Science 2885, pp. 206-225, Springer Verlag, 2003. [Proc. International Conference on Formal Engineering Methods (ICFEM'03), Singapore, November 2003.]
- M. Layouni, J. Hooman, and S. Tahar: On the correctness of an Intrusion-Tolerant Group Communication Protocol D. Geist, E. Tronci (Eds.), Correct Hardware Design and Verification Methods, Lecture Notes in Computer Science 2860, pp. 231-246, Springer Verlag, 2003. [Proc. 12th IFIP Conf. on Correct Hardware Design and Verification Methods (CHARME'03), L'Aquila, Italy, October 2003.]
- A. Gawanmeh, S. Tahar, and K. Winter; A Tool for Verifying ASM Models using Multiway Decision Graphs [Proc. 2003 Micronet Annual Workshop, Toronto, Canada, October 2003, pp. 127-128.]
- A. Gawanmeh, S. Tahar, and K. Winter: Formal Verification of ASM Designs using the MDG Tool [Proc. IEEE International Conference on Software Engineering and Formal Methods (SEFM'03), Brisbane, Australia, September 2003, pp. 210-219, IEEE Computer Society Press.]
- M. Layouni, J. Hooman, and S. Tahar: Modeling and Verification of Leaders Agreement in the Intrusion-Tolerant Enclaves Using PVS B-Track Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs’03), Roma, Italy, September 2003, pp145-158. [D. Basin and B. Wolff (Eds.), TPHOLs 2003 Emerging Trends Proceedings, Technical Report No. 187, Institut of Informatics, Albert-Ludwigs University, Freiburg, Germany.]
- B. Akbarpour and S. Tahar: The Application of Formal Verification to SPW Designs [Proc. EUROMICRO Symposium on Digital System Design (DSD'03), Belek, Turkey, September 2003, pp. 325 -332, IEEE Computer Society Press.]
- R. Mizouni, S. Tahar, and P. Curzon: On the Embedding of MDG Specification Languages in HOL [Proc. IEEE International Conference on Computer Systems and Applications (AICCSA'03), Tunis, Tunisia, July 2003, pp. 71-78. IEEE Computer Society Press.]
- A.T. Abdel-Hamid, S. Tahar, and E.M. Abulhamid: IP Watermarking Techniques: Survey and Comparison [Proc. IEEE 3rd International Workshop on System-on-Chip (IWSOC'03), Calgary, Alberta, Canada, June-July 2003, pp. 60-65, IEEE Computer Society Press.]
- A. Habibi and S. Tahar: A Survey on System-On-a-Chip Design Languages [Proc. IEEE 3rd International Workshop on System-on-Chip (IWSOC'03), Calgary, Alberta, Canada, June-July 2003, pp. 212-215, IEEE Computer Society Press.]
- M. Zaki, Y. Mokhtari, and S. Tahar: A Path Dependency Graph for Verilog Program Analysis Proc. IEEE Northeast Workshop on Circuits and Systems (NEWCAS’03), Montreal, Quebec, Canada, June 2003, pp. 109-112.]
- F. Wang, A. Habibi, and S. Tahar: Translating LTL Specification to MDG-HDL [Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'03), Montreal, Quebec, Canada, May 2003, Vol. 2, pp. 1369-1373.]
- M. Zaki and S. Tahar: Syntax Code Analysis and Generation for Verilog [Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'03), Montreal, Quebec, Canada, May 2003, Vol. 1, pp. 235-240.]
- J. Lu and S. Tahar: Modeling and Verification of an ATM Port Controller in VIS [Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'03), Montreal, Quebec, Canada, May 2003, Vol. 1, pp. 241-245.]
- F. Wang and S. Tahar: Language Emptiness Checking using MDGs [Proc. ACM 13th Great Lakes Symposium on VLSI (GLS-VLSI'03), Washington D.C., USA, April 2003, pp. 88-91, ACM Publications.]
- A.T. Abdel-Hamid, S. Tahar, and J. HarrisonHierarchical Approach for the Verification of an IEEE-754 Floating-Point Function [Proc. 2002 Micronet Annual Workshop, Alymer, Canada, April 2002, pp. 107-108.]
- A. Gawanmeh, S. Tahar and K. Winter: Interfacing ASMs with the MDG Tool E. Boerger, A. Gargantini, E. Riccobene (Eds.) Abstract State Machines - Advances in Theory and Applications, Lecture Notes in Computer Science 2589, Springer Verlag, 2003, pp. 278-292. [Proc. International Conference on Abstract State Machines (ASM'03), Taormina, Italy, March 2003.]
- A.T. Abdel-Hamid, S. Tahar, and J. Harrison: Enabling Hardware Verification through Design Changes C. George and H. Miao (Eds.), Formal Methods in Software Engineering, Lecture Notes in Computer Science 2495, Springer Verlag, 2002, pp. 459-470. [Proc. International Conference on Formal Engineering Methods (ICFEM'02), Shanghai, China, October 2002.]
- M.H. Zobair and S. Tahar: Formal Verification of a SONET Telecom System Block [Proc. International Conference on Formal Engineering Methods (ICFEM'02), Lecture Notes in Computer Science, Springer Verlag, Shanghai, China, October 2002.]
- H. Peng, Y. Mokhtari, and S. Tahar: Environment Synthesis for Compositional Model Checking [Proc. IEEE International Conference on Computer Design (ICCD'02), Freiburg, Germany, September 2002, IEEE Computer Society Press, pp 70-75.]
- A. Habibi, S. Tahar, and A. Ghazel: Formal Verification of a DSP Chip Using an Iterative Approach [Proc. EUROMICRO Symposium on Digital System Design (DSD'02), Dortmund, Germany, September 2002, pp. 12-19.]
- B. Akbarpour, S. Tahar, and A. Dekdouk: Formalization of Cadence SPW Fixed-Point Arithmetic in HOL M. Butler, L. Petre, and K. Sere (Eds.), Integrated Formal Methods, Lecture Notes in Computer Science 2335, Springer Verlag, 2002, pp. 185-204. [Proc. International Conference on Integrated Formal Methods (IFM'02), Turku, Finland, May 2002.]
- H. Xiong, P. Curzon, S. Tahar, and A. Blandford: Formally Linking MDG and HOL Based on a Verified MDG System M. Butler, L. Petre, and K. Sere (Eds.), Integrated Formal Methods, Lecture Notes in Computer Science 2335, Springer Verlag, 2002, pp. 205-224. [Proc. International Conference on Integrated Formal Methods (IFM'02), Turku, Finland, May 2002.]
- A. Habibi, S. Tahar, and A. Ghazel: Behavioral Modeling and Verification of the ADSP-2100 Processor using HOL [Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'02), Winnipeg, Manitoba, Canada, May 2002, Vol. 2, pp. 614-619.]
- F. Wang, S. Tahar, and E. Cerny: Towards Language Emptiness Model Checking for MDGs [Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'02), Winnipeg, Manitoba, Canada, May 2002, Vol. 2, pp. 590-595.]
- A. Habibi, S. Tahar, and A. Ghazel: A Progressive Methodology for the Verification of a DSP Chip [Proc. ACM 12th Great Lakes Symposium on VLSI (GLS-VLSI'02), New York City, New York, USA, April 2002.]
- J. Lu and S. Tahar: On the Model Checking of the RCMP-800 Input FIFO [Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'02), Winnipeg, Manitoba, Canada, May 2002, Vol. 1, pp. 578-583.]
- P. Curzon and S. Tahar: Automating the Verification of Parameterized Hardware using a Hybrid Tool [Proc. IEEE 13th International Conference on Microelectronics (ICM'01), Rabat, Morocco, October 2001, pp. 257-260.]
- J. Lu and S. Tahar: Design and Verification of a Knockout ATM Concentrator [Proc. IEEE 13th International Conference on Microelectronics (ICM'01), Rabat, Morocco, October 2001, pp. 261-264.]
- L. Barakatain and S. Tahar: Functional Verification of a SCI-PHY Level 2 Protocol Engine [Proc. IEEE International Conference on Information, Communications & Signal Processing (ICICS'01), Singapore, October 2001.]
- P. Hong, Y. Mokhtari, and S. Tahar: Model Reduction Based on Value Dependency [Proc. IEEE International ASIC/SOC Conference (ASIC'01), Washington, DC, USA, September 2001, pp. 220-224.]
- H. Xiong, P. Curzon, S. Tahar, and A. Blandford: Proving Existential Theorems when Importing Results from MDG to HOL B-Track Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs’01), Edinburgh, Scotland, UK, September 2001, pp. 384-399. In: R.J. Boulton and P.B. Jackson (Eds.), [TPHOLs 2001: Supplemental Proceedings, Informatic Reprot Series EDI-INF-RR-0046, Division of Informatics, University of Edinburgh, Edinburgh, UK, September 2001.]
- A.T. Abdel-Hamid, S. Tahar, and J. Harrison: Hierarchical Verification of the Implementation of the IEEE-754 Table-Driven Floating-Point Exponential Function using HOL B-Track Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs’01), Edinburgh, Scotland, UK, September 2001, pp. 1-16. [In: R.J. Boulton and P.B. Jackson (Eds.), TPHOLs 2001: Supplemental Proceedings, Informatic Reprot Series EDI-INF-RR-0046, Division of Informatics, University of Edinburgh, Edinburgh, UK, September 2001.]
- S. Kort, S. Tahar, and P. Curzon: Hierarchical Verification Using an MDG-HOL Hybrid Tool Margaria, T. and Melham, T. (Eds.), Correct Hardware Design and Verification Methods, Lecture Notes in Computer Science 2144, Springer Verlag, 2001, pp. 244-258. [Proc. 11th IFIP Conference on Correct Hardware Design and Verification Methods (CHARME'2001), Livingston, Scotland, UK, September 2001.] [
**BEST PAPER**] - L. Baratain and S. Tahar: Model Checking of the Fairisle ATM Switch Fabric using FormalCheck [Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'01), Toronto, Ontario, Canada, May 2001.]
- M.H. Zobair and S. Tahar: Modeling and Formal Verification of a Telecom System Block using MDGs [Proc. 2001 Micronet Annual Workshop, Alymer, Canada, April 2001, pp. 161-162.]
- L. Barakatain, S. Tahar, J. Lamarche, and J-M Gendreau: Practical Approaches to the Model Checking of a Telecom Megacell using FormalCheck [Proc. ACM 11th Great Lakes Symposium on VLSI (GLS-VLSI'01), West Lafayette, Indiana, USA, March 2001, ACM Publications, pp. 1-6.] [
**BEST PAPER**] - Y. Mokhtari, M. Shirazipour, and S. Tahar: A Case Study on Model Checking and Refinement of Abstract State Machines [Proc. Eight International Conference on Computer Aided Systems Theory (EUROCAST'01), Las Palmas de Gran Canaria, Canary Islands, Spain, February 2001, pp. 239-242.]
- P. Hong and S. Tahar: Hardware Modeling and Verifiation of an ATM Ring MAC Protocol [Proc. IEEE 12th International Conference on Microelectronics (ICM'00), Teheran, Iran, November 2000, pp. 21-24.]
- P. Hong, S. Tahar, and F. Khendek: SPIN vs. VIS: A Case Study on the Formal Verification of the ATMR Protocol [Proc. IEEE International Conference on Formal Engineering Methods (ICFEM'2000), York, UK, September 2000, IEEE Computer Society Press, pp. 79-87.]
- H. Xiong, P. Curzon, S. Tahar, and A. Blandford: Embedding and Verification of an MDG-HDL Translator in HOL; B-Track Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs’2000), Portland, Oregon, USA, August 2000, pp. 237-248.
- M. Azizi, E.-M. Aboulhamid, and S. Tahar: Sequential and Distributed Simulations using Java Threads [Proc. IEEE International Conference on Parallel Computing in Electrical Engineering (PARELEC'2000), Trois-Rivieres, Quebec, Canada, August 2000, pp. 237-241. IEEE Computer Society.]
- M. Hasan, S. Tahar, and P. Curzon: Impact of Design Changes on Verification Using MDGs [Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'00), Halifax, Nova Scotia, Canada, May 2000, pp. 173-178.]
- A. A. Mir, S. Balakrishnan, and S. Tahar: Modeling and Verification of an Embedded System using Cadence SMV [Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'00), Halifax, Nova Scotia, Canada, May 2000, pp. 179-183.]
- S. Kort, S. Tahar, P. Curzon, X. Song: HOL-MDG: A Hybrid Tool for Forma1 Verification [Proc. 2000 Micronet Annual Workshop, Ottawa, Canada, April 2000, pp. 131-132.]
- V.K. Pisini, S. Tahar, P. Curzon, O. Ait-Mohamed and X. Song: Formal Hardware Verification by Integrating HOL and MDG [Proc. ACM 10th Great Lakes Symposium on VLSI (GLS-VLSI'00), Chicago, Illinois, USA, March 2000, ACM Publications, pp. 23-28.]
- H. Peng and S. Tahar: Compositional Verification of IP Based Designs [Proc. IFIP International Worshop on IP Based Synthesis and System Design, Grenoble, France, December 1999, pp. 189-193.]
- M. Palanisamy and S. Tahar: Formal Verification of the RCMP Egress Routing Logic [Proc. IEEE 11th International Conference on Microelectronics (ICM'99), Kuwait City, Kuwait, November 1999, pp. 89-92.]
- H. Xiong, P. Curzon, and S. Tahar: Importing MDG Results into HOL Bertot, Y.; Dowek, G.; Hirschowitz, A.; Paulin, C. and Theryvon, L. (Eds.), Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 1690, Springer Verlag, 1999, pp. 293-310 [Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'99), Nice, France, September 1999.]
- M. Azizi, E.-M. Aboulhamid and S. Tahar: Properties Coverification for HW/SW Systems [Proc. 2nd Electronic Circuits and Systems Conference (ECS'99),pp. 81-84, Bratislava, Slovakia, September 1999.]
- M. Azizi, E.-M. Aboulhamid, and S. Tahar: Multithreading-Based Co-Verification Technique of HW/SW Systems [Proc. International Conference on Parallel and Distributed Processing Techniques and Applications (PDPTA'99), CSREA Press, Vol. VI, pp. 1999-2005, Las Vegas, Nevada, USA, June/July 1999.]
- H.T. Bui and S. Tahar: Design and Synthesis of an IEEE-754 Exponential Function [Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'99), pp. 450-455, Edmonton, Alberta, Canada, May 1999.]
- M. Palanisamy and S. Tahar: RTL Design and Verification of the RCMP Egress Routing Logic [Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'99), pp. 111-115, Edmonton, Alberta, Canada, May 1999.]
- T.H Bui, T. Elshabrawy, F. Khendek, S. Tahar, and T. LeNgoc: Description and Validation of the Internet Stream Protocol (ST2+) Using SDL/MSC [Proc. IEEE Canadian Conference on Electrical & Computer Engineering (CCECE'99), pp. 238-244, Edmonton, Alberta, Canada, May 1999.]
- V.K. Pisini, S. Tahar, O. Ait-Mohamed, P. Curzon, and X. Song: An Approach to Link HOL and MDG for Hardware Verification [Proc. 1999 Micronet Annual Workshop, Ottawa, Canada, April 1999, pp. 156-157.]
- S. Balakrishnan and S. Tahar: A Hierarchical Approach to the Formal Verification of Embedded Systems Using MDGs [Proc. IEEE 9th Great Lakes Symposium on VLSI (GLS-VLSI'99), Ann Arbor, Michigan, USA, March 1999, IEEE Computer Society Press, pp. 284-287.]
- S. Balakrishnan and S. Tahar: Modeling and Formal Verification of a Commercial Microcontroller for Embedded System Applications [Proc. IEEE 10th International Conference on Microelectronics (ICM'98), Monastir, Tunisia, December 1998, pp. 107-110.]
- S. Tahar, P. Curzon and J. Lu: Three Approaches to Hardware Verification: HOL, MDG and VIS Compared Gopalakrishnan, G. and Windley, P. (Eds.), Formal Methods in Computer-Aided Design, Lecture Notes in Computer Science 1522, Springer Verlag, 1998, pp. 433-450 [Proc. International Conference on Formal Methods in Computer-Aided Design (FMCAD'98), Palo Alto, California, USA, November 1998.]
- J. Lu, S. Tahar, D. Voicu and X. Song: Model Checking of a real ATM Switch [Proc. IEEE International Conference on Computer Design (ICCD'98), Austin, Texas, USA, October 1998, IEEE Computer Society Press, pp. 195-198.]
- P. Curzon, S. Tahar, and O. Ait-Mohamed: Verification of the MDG Components Library in HOL J. Grundy and M. Newey (Eds.), Theorem Proving in Higher Order Logics: Emerging Trends, The Australian National University, 1998, pp. 31-45. Supplementary [Proc. International Conference on Theorem Proving in Higher-Order Logics (TPHOLs'98), Canberra, Australia, September 1998.]
- J. Lu and S. Tahar: Practical Approaches to the Automatic Verification of an ATM Switch Fabric using VIS [Proc. IEEE 8th Great Lakes Symposium on VLSI (GLS-VLSI'98), Lafayette, Louisiana, USA, February 1998, IEEE Computer Society Press, pp. 368-373.]
- Ying Xu, Eduard Cerny, Xiaoyu Song, Francisco Corella, Otmane Ait Mohamed: Model Checking for a First-Order Temporal Logic Using Multiway Decision Graphs (CAV 1998): 219-231
- A.E.K Dekdouk, Otmane Ait Mohamed, Sadegh Jahanpour, Eduard Cerny.What About Formal Verification of IP-based SoC Designs International Conference IWLAS’98. Grenoble,France.
- Mostefa Azizi, Otmane Ait Mohamed, Xiaoyu Song: Cache Coherence Protocol Verification of Multiprocessor System with Shared Memory Microelectronics (ICM’98). Monastir, Tunisia. Dec. 14-16, 98
- Otmane Ait Mohamed, Eduard Cerny, Xiaoyu Song: MDG-based Verification by Retiming and Combinational Transformations [Proc. of the Great Lakes Symposium on VLSI (GLS-VLSI'98): 356--361.IEEE Computer Society Press.]
- Otmane Ait Mohamed, Xiaoyu Song, Eduard Cerny: On the non-termination of MDGs-based abstract state enumeration. CHARME 1997: 218-235
- Z. Zhou, X. Song, S. Tahar, E. Cerny, F. Corella and M. Langevin: Verification of the Island Tunnel Controller using Multiway Decision Graphs Srivas, M. and Camilleri, A. (Eds.), Formal Methods in Computer-Aided Design, Lecture Notes in Computer Science 1166, Springer Verlag, 1996, pp. 233-246. Proc. International Conference on Formal Methods in Computer-Aided Design (FMCAD’96), Palo Alto, California, USA, November 1996.
- M. Langevin, S. Tahar, Z. Zhou, X. Song and E. Cerny: Behavioral Verification of an ATM Switch Fabric using Implicit Abstract State Enumeration [Proc. IEEE International Conference on Computer Design (ICCD'96) , Austin, Texas, USA, October 1996, IEEE Computer Society Press, pp. 20-26.]
- S. Tahar and P. Curzon: A Comparison of MDG and HOL for Hardware Verification Von Wright, J.; Grundy, J. and Harrison, J. (Eds.), Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science 1125, Springer Verlag, 1996, pp. 415-430 [Proc. International Conference on Theorem Proving in Higher Order Logics (TPHOLs'96), Turku, Finland, August 1996.]
- Z. Zhou, X. Song, F. Corella, M. Langevin, E. Cerny and S. Tahar: MDG Tools for the Verification of RTL Designs; In: Alur, R. and Henzinger, T. (Eds.), Computer Aided Verification, Lecture Notes in Computer Science 1102, Springer Verlag, 1996, pp. 433-436 [Proc. Conference on Computer Aided Verification (CAV'96), New Brunswick, New Jersey, USA, July/August 1996.]
- S. Tahar, Z. Zhou, X. Song, E. Cerny and M. Langevin: Formal Verification of an ATM Switch Fabric using Multiway Decision Graphs [Proc. IEEE Sixth Great Lakes Symposium on VLSI (GLS-VLSI'96), Ames, Iowa, USA, March 1996, IEEE Computer Society Press, pp. 106-111.]