O. Barhoumi, M. Zaki and S. Tahar: Formal Analysis of Vehicular Crash Severity using KeYmaera X; In: S.M. Watt and T. Ida (Eds.), Symbolic Computation in Software Science, Lecture Notes in Computer Science 14991, Springer Verlag, 2024, pp. 1-19. [Proc. Symposium on Symbolic Computation in Software (SCSS’2024), Tokyo, Japan, August 2024].
E. Deniz., A. Rashid, O. Hasan and S. Tahar: Formal Verification of ABCD Parameters Based Models for Transmission Lines; In: S.M. Watt and T. Ida (Eds.), Symbolic Computation in Software Science, Lecture Notes in Computer Science 14991, Springer Verlag, 2024, pp. 20-37. [Proc. Symposium on Symbolic Computation in Software (SCSS’2024), Tokyo, Japan, August 2024].
M. Abdelghany, A. Rashid and S. Tahar: A Framework for Formal Probabilistic Risk Assessment using HOL Theorem Proving; In: A. Kohlhase and L. Kovács (Eds.): Intelligent Computer Mathematics, Lecture Notes in Computer Science 14960, Springer Verlag, 2024, pp. 298–314. [Proc. Conference on Intelligent Computer Mathematics (CICM’24), Montreal, Canada, August 2024].
N. Dekhil, A. Rashid and S. Tahar: HOL4PRS: Proof Recommendation System for HOL4 Theorem Prover; In: A. Kohlhase and L. Kovács (Eds.): Intelligent Computer Mathematics, Lecture Notes in Computer Science 14960, Springer Verlag, 2024, pp. 352-359. [Proc. Conference on Intelligent Computer Mathematics (CICM’24), Montreal, Canada, August 2024].
M. Abdelghany and S. Tahar: Formalization of Functional Block Diagrams using HOL Theorem Proving; In L. Lima and V. Molnár (Eds.), Formal Methods: Foundations and Applications, Lecture Notes in Computer Science 13768, Springer Verlag, 2022, pp. 22-35. [Proc. Brazilian Symposium on Formal Methods (SBMF’22), Brazil, December, 2022]
M. Abdelghany and S. Tahar. Tahar: Formal Probabilistic Risk Assessment of a Nuclear Power Plant; Proc. ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS’22), Auckland, New Zealand, December 2022, pp. 80-87.
A. Aoun, M. Masadeh and S. Tahar: On the Design of Approximate Sobel Filter; Proc. IEEE International Conference on Microelectronics (ICM’22), Casablanca, Morocco, December 2022, pp. 1-5.[BEST PAPER]
E. Deniz, A. Rashid, O. Hasan and S. Tahar: On the Formalization of the Heat Conduction Problem in HOL; In: K. Buzzard and T. Kutsia (Eds.): Intelligent Computer Mathematics, Lecture Notes in Computer Science 13467, Springer Verlag, 2022, pp. 21-37. [Proc. Conference on Intelligent Computer Mathematics (CICM’22), Tbilisi, Georgia, September 2022].
M. Soualhia, F. Komh, and S. Tahar: Failure Analysis of Hadoop Schedulers using an Integration of Model Checking and Simulation; In: T. Kutsia (Ed.), Symbolic Computation in Software Science, Electronic Proceedings in Theoretical Computer Science 342, 2021, pp. 114-128. [Proc. International Symposium on Symbolic Computation in Software Science (SCSS’21), Linz, Austria, September 2021].
M. Abdelghany and S. Tahar: Formalization of RBD-based Cause Consequence Analysis in HOL; In: F. Kamareddine and C. Sacerdoti Coen (Eds.): Intelligent Computer Mathematics, Lecture Notes in Computer Science 12833, Springer, 2021, pp. 47-64. [Proc. Conference on Intelligent Computer Mathematics (CICM’21), Timisoara, Romania, July 2021].
Y. Elderhalli, O. Hasan, and S. Tahar: A Framework for Formal Dynamic Dependability Analysis using HOL Theorem Proving; In: C. Benzmuller and B. Miller (Eds.): Intelligent Computer Mathematics, Lecture Notes in Computer Science 12236, Springer, 2020, pp. 105-122. [Proc. Conference on Intelligent Computer Mathematics (CICM’20), Bertinoro, Italy, July 2020].
A. Rashid, U. Siddique, and S. Tahar: Formal Verification of Cyber-Physical Systems Using Theorem Proving; In: O. Hasan and F. Mallet (Eds.), Formal Techniques for Safety-Critical Systems, Communications in Computer and Information Science 1165, Springer, 2020, pp. 3-18. [Proc. International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS’19), Shenzhen, China, November 9, 2019].
Y. Elderhalli, O. Hasan and S. Tahar: A Formally Verified Algebraic Approach for Dynamic Reliability Block Diagrams; In: Y. Ameur and S. Qin (Eds.), Formal Methods and Software Engineering, Lecture Notes in Computer Science 11852, Springer, 2019, pp. 253-269. [Proc. International Conference on Formal Engineering Methods (ICFEM’19), Shenzhen, China, November, 2019].
Y. Elderhalli, M. Volk, O. Hasan, J.-P. Katoen and S. Tahar: Formal Verification of Rewriting Rules for Dynamic Fault Tree; In: P.C. Ölveczky and G. Salaün, Software Engineering and Formal Methods, Lecture Notes in Computer Science 11724, Springer, 2019, pp. 513-531. [Proc. International Conference on Software Engineering and Formal Methods (SEFM’19), Oslo, Norway, September, 2019].
H. El-Derhalli, S. LeBeux and S. Tahar: Stochastic Computing with Integrated Optics; Proc. IEEE/ACM Design Automation and Test in Europe (DATE’19), Florence, Italy, March 2019, pp. 1342-1347.
M. Masadeh, O. Hasan and S. Tahar: Approximation-Conscious IC Testing; Proc. IEEE 30th International Conference on Microelectronics (ICM’18), Sousse, Tunisia, December 2018, pp. 56-59.
M. Masadeh, O. Hasan and S. Tahar: Comparative Study of Approximate Multipliers; Proc. ACM 28th Great Lakes Symposium on VLSI (GLS-VLSI’18), Chicago, Illinois, USA, May 2018, ACM Publications, pp. 415-418.
Y. Elderhalli, O. Hasan, W. Ahmad, and S. Tahar: Formal Dynamic Fault Trees Analysis Using an Integration of Theorem Proving and Model Checking; In: A. Dutle, C. Muñoz, and A. NarkawiczK (Eds.), NASA Formal Methods Symposium, Lecture Notes in Computer Science 10811, Springer Verlag, 2018, pp. 139-156. [Proc. NASA Frormal Methods Symposium (NFM’18), Newport News, VA, USA, April 2018]
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]
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]
S.M. Beillahi, U. Siddique and S. Tahar: Formal Analysis of Engineering Systems Based on Signal-Flow-Graph Theory;In: S. Bogomolov, M. Martel, and P. Prabhakar (Eds.), Numerical Software Verification, Lecture Notes in Computer Science 10152, Springer Verlag, 2017, pp. 31-46. [Proc. International Workshop on Numerical Software Verification (NSV’16), Toronto, Canada, July 2016]
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]
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]
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]
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]
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]
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]
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]
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.]
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. 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]
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]
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]
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: 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.]
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]
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.]
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.]
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.]
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.]
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.]
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.]
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.]
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.]
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.]
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.
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.]
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.]
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]
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.]
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.
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.]
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.]
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.]
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]
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. 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.]
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
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]
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.]
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 .]
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: 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.]
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.]
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. 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.]
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.]
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.]
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. 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]
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.]
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.]
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.]
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.]
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.
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.
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.]