Dr. Osman Hasan
Assistant Professor
Department of Electrical Engineering

School of Electrical Engineering and Computer Science (SEECS)
National University of Sciences and Technology (NUST)
NUST Campus H-12, Islamabad
Tel: 051-90852137
Email: osman.hasan at seecs.nust.edu.pk
Web: http://ohasan.seecs.nust.edu.pk/

Specialization:
Formal Methods and VLSI/ASIC/FPGA Design.

Education:
Postdoctoral – Formal Verification – Concordia University, Canada (2009)

Education

Ph.D.      Electrical Engineering Concordia University, Montreal, Canada (2008)

M.Eng.    Electrical Engineering Concordia University, Montreal, Canada (2001)

B.Sc.       Electrical Engineering N-W.F.P University of Engineering and Technology Peshawar, Pakistan (1997)

Interests

Digital and VLSI Design, Computer Architectures, Formal Verification, Theorem Proving, Higher-Order-Logic.

Email: osman.hasan AT seecs DOT edu DOT pk

Research Interest

These days hardware and software systems are increasingly being used in safety-critical domains, such as electronic military and medicine equipment and automated transportation systems. This fact makes the accuracy of their analysis very important as an uncaught system bug may endanger human life or lead to a significant financial loss. Traditionally, the verification of these systems has predominantly been accomplished by computer simulation. However, it does not ascertain 100% correctness and thus has primarily been responsible for many unfortunate incidents that happened due to an erroneous hardware or software system deployed in a safety-critical domain.

The focus of our research is on using formal methods, which are based on mathematical techniques and thus unlike simulation ensure 100% precise results, for the analysis and verification of hardware, software, and embedded systems. In particular, we aim at using theorem proving, which is one of the widely used formal methods, to develop methodologies, algorithms and  tools for the accurate analysis of systems that are continuous in nature or interact with continuous physical environments.

 More details can be found at my research lab website.

Current Research Projects

Research Projects

Automated Tele-Micromanipulator Cell Injection System, Funded by National ICTR&D Fund, Pakistan

Formal Verification of Distributed Thermal and Resource Management Schemes for on-chip Many-core Systems, Funded by Der Deutsche Akademische Austauschdienst (DAAD), Germany

Formalization of Information Theories and Application in Safety-critical Engineering Systems, Funded by Qatar National Research Fund (QNRF), Qatar

Formal System Analysis and Verification, Funded by NRPU, Higher Education Commission (HEC), Pakistan

Tele-Surgical Robot and Simulator, Funded by National ICTR&D fund, Pakistan

Research Experience

Postdoctoral Fellow, Concordia University
June 2008 – August 2009 (1 year 2 months )

Journal Papers

F. K. Lodhi, S. R. Hasan, O. Hasan, and F. Awwad, "Analyzing Vulnerability of Asynchronous Pipeline to Soft Errors: Leveraging Formal Verification", Journal of Electronic Testing: Theory and Applications, Vol. 32, No. 5, pp. 569-586, Sep, 2016.

W. Ahmed, O. Hasan and S. Tahar,, "Formalization of Reliability Block Diagrams in Higher-order Logic", Journal of Applied Logic, Vol. 18, No. 1, pp. 19-41, Aug, 2016.

S.R. Hasan, W.Gul and O. Hasan, , "Clock Domain Crossing (CDC) in 3D-SICs: Semi QDI Asynchronous vs Loosely Synchronous", Integration, the VLSI Journal, Vol. 52, pp. 367-380, Jan, 2016.

U. Pervez, A. Mehmood, O. Hasan, K. Latif, and A. Gawanmeh, "Improvement Strategies For Device Interoperability Middleware Using Formal Reliability Analysis", Scalable Computing: Practice and Experience, Vol. 17, No. 3, pp. 155-170, 2016.

S.A.A. Bukhari, F. K. Lodhi, O. Hasan, M.Shafique and J.Henkel, "FAMe-TM: Formal Analysis Methodology for Task Migration Algorithms in Many-Core Systems", Science of Computer Programming, Vol. 133, No. 2, pp. 154-174, 2016.

M. U. Sardar, O. Hasan, M. Shafique and J. Henkel, "Theorem Proving Based Formal Verification of Distributed Dynamic Thermal Management Schemes", Journal of Parallel and Distributed Computing, Vol. 100, pp. 157-171, 2016.

W. Ahmed, O. Hasan, U. Pervez, and J. Qadir, "Reliability Modeling and Analysis of Communication Networks", Journal of Network and Computer Applications , Vol. 78, pp. 191-215, 2016.

U. Mushtaq, O. Hasan, F. Awwad, "NoC based Implementation of Free Form Deformations in Medical Imaging Registration", Journal of Circuits, Systems, and Computers, Vol. 26, No. 4, pp. 1750078, 2016.

J. Qadir and O. Hasan, "Applying Formal Methods to Networking: Theory, Techniques and Applications", Communications Surveys and Tutorials, Vol. 17, No. 1, pp. 256-291, Mar, 2015.

S. Ahmad, , O. Hasan, U. Siddique, "On the Formalization of Zsyntax with Applications in Molecular Biology", Scalable Computing: Practice and Experience, Vol. 16, No. 1, pp. 37-51, Feb, 2015.

A.H. Qureshi, S. Mumtaz, Y. Ayaz and O. Hasan, "Triangular Geometrised Sampling Heuristic for Fast Optimal Motion Planning", International Journal of Advanced Robotic Systems, Vol. 12, No. 10, pp. 10.5772/59763, Feb, 2015.

M. Elleuch, O. Hasan, S. Tahar and M. Abid, "Formal Probabilistic Analysis of Detection Properties in Wireless Sensor Networks", Formal Aspects of Computing, Vol. 27, No. 1, pp. 79-102, 2015.

M. Elleuch, O. Hasan, S. Tahar, M. Abid, "Formal Probabilistic Analysis of Detection Properties in Wireless Sensor Networks", Formal Aspects of Computing, Vol. 28, No. 1, pp. 1-24, Jul, 2014.

T. Hassan, A. Hameed, S. Nasir, N. Kamal, O. Hasan, "Al-Zahrawi: A Telesurgical Robotic System for Minimal Invasive Surgery", Systems Journal, Vol. 9, No. 1, pp. 1-11, Jul, 2014.

U. Siddiqui, O. Hasan, "On the Formalization of Gamma Function in HOL", Journal of Automated Reasoning, Vol. 54, No. 4, pp. 407-429, Jul, 2014.

S.K. Afshar, U. Siddique, M.Y. Mahmoud, V. Aravantinos, O. Seddiki, O.Hasan, S. Tahar, "Formal Analysis of Optical Systems", Mathematics in Computer Science, Vol. 8, No. 1, pp. 39-70, May, 2014.

O. Hasan, S.A. Khayam, "Towards Formal Linear Cryptanalysis using HOL4", Journal of Universal Computer Science,, Vol. 20, No. 2, pp. 193-212 , Mar, 2014.

O. Hasan, , F. Lodhi, N. Sharif, N. Ramzan, S.R. Hasan, "Variation Aware Dynamic Digital Phase Detector for Low Latency Clock Domain Crossing", Circuits, Devices & Systems,, Vol. 8, No. 1, pp. 58-64, Jan, 2014.

L. Liu, O. Hasan, S. Tahar, "Formal Reasoning about Finite-state Discrete-Time Markov Chains in HOL", Journal of Computer Science and Technology, Vol. 28, No. 2, pp. 217-231, Jun, 2013.

N. Abbasi, O.hasan, S. Tahar, "An Approach for Lifetime Reliability Analysis using Theorem Proving", Journal of Computer and System Sciences, Vol. 80, No. 2014, pp. 323-345, Mar, 2013.

T.Mhamdi, O. Hasan, S.Tahar, "Formalization of Measure Theory and Lebesgue Integration for Probabilistic Analysis in HOL", Transactions on Embedded Computing Systems, Vol. 12, No. 1, pp. 13:1-23, Jan, 2013.

J. Nasir F. Islam, U. Malik, Y. Ayaz, , M. Khan and M. S. Muhammad , O. Hasan, "RRT*-SMART: A rapid convergence implementation of RRT*", Journal of Advanced Robotic Systems: Robot Motion,, Vol. 10, No. 299, pp. 1-10, 2013.

Osman Hasan , S. Tahar, "Reasoning about Conditional Probabilities using a Higher-order-Logic Theorem Prover", Journal of Applied Logic, Vol. 9, No. 1, pp. 23-40, Mar, 2011.

Osman Hasan, J. Patel and S. Tahar, "Formal Reliability Analysis of Combinational Circuits using Theorem Proving", Journal of Applied Logic, Vol. 9, No. 1, pp. 41-60, Mar, 2011.

Osman Hasan, S. Tahar, "Formally Analyzing Expected Time Complexity of Algorithms using Theorem Proving", Journal of Computer Science and Technology, Vol. 25, No. 6, pp. 1305-1320, Nov, 2010.

O. Hasan, S. Tahar and N. Abbasi, "Formal Reliability Analysis using Theorem Proving", IEEE Transactions on Computers, Vol. 59, No. 5, pp. 579-592, Oct, 2010.

O. Hasan, S. Tahar, "Probabilistic Analysis of Wireless Systems using Theorem Proving", Electronic Notes in Theoretical Computer Science, Vol. 242, No. 2, pp. 43-58, Jul, 2009.

O. Hasan, S. Tahar, "Formal Verification of Tail Distribution Bounds in the HOL Theorem Prover", Mathematical Methods in the Applied Sciences, Vol. 32, No. 4, pp. 480-504, Mar, 2009.

O. Hasan, S. Tahar, "Performance Analysis and Functional Verification of the Stop-and-Wait Protocol in HOL", Journal of Automated Reasoning, Vol. 42, No. 1, pp. 1-33, Jan, 2009.

O. Hasan, S. Tahar, "Using Theorem Proving to Verify Expectation and Variance for Discrete Random Variables", Journal of Automated Reasoning, Vol. 41, No. 3-4, pp. 295-323, Dec, 2008.

O. Hasan, S. Tahar, "Formalization of the Standard Uniform Random Variable", Theoretical Computer Science, Vol. 382, No. 1, pp. 71-83, May, 2007.

Conference Papers

M. U. Sardar and O. Hasan, "Towards Probabilistic Formal Modeling of Robotic Cell Injection Systems", Proceedings of the Workshop on Models for Formal Analysis of Real Systems (MARS), 2017, Sweden.

W. Ahmed, O. Hasan, "Towards Availability Analysis using Theorem Proving", Proceedings of the Formal Engineering Methods , Nov, 2016, Tokyo Japan.

W. Ahmed, O. Hasan, "Formalization of Fault Trees in Higher-order Logic: A Deep Embedding Approach", Proceedings of the Dependable Software Engineering Theories, Tools and Applications, Nov, 2016, China.

W. Ahmed, O. Hasan and S. Tahar, "Formal Dependability Modeling and Analysis: A Survey", Proceedings of the Conferences on Intelligent Computer Mathematics (CICM-2016), , Jul, 2016, Poland.

J. A. Khan,, U. Pervaiz, H. A. Akbar and O. Hasan, "A Wearable Wireless Sensor for Cardiac Monitoring", Proceedings of the Body Sensor Networks (BSN-2016), , Jul, 2016, San Francisco, United States.

S. Mazahir,, O. Hasan, R. Hafiz, M. Shafique, J. Henkel, "An Area-Efficient Consolidated Configurable Error Correction for Approximate Hardware Accelerators", Proceedings of the Design Automation Conference (DAC-2016), , Jun, 2016, Austin United States.

M. U. Sardar, N. Afaq, K. A. Hoque, O. Hasan, T. Johnson, "Probabilistic Formal Verification of SATS Concept of Operation", Proceedings of the NASA Formal Methods (NFM-2016), , Jun, 2016, Minneapolis United States.

S. Hameed, O. Hasan, "Towards Autonomous Collision Avoidance in Surgical Robots using Image Segmentation and Genetic Algorithms", Proceedings of the IEEE Region 10 Symposium (TENSYMP-2016), , May, 2016, Bali Indonesia.

A. Mahmood, , H. Gillani, Y. Ssaleem, O. Hasan and S. Hasan, "Formal Reliability Analysis of Protective Systems in Smart Grids", Proceedings of the IEEE Region 10 Symposium (TENSYMP-2016), , May, 2016, Bali Indonesia.

W. Gul, S. R. Hasan, O. Hasan, F. Khalid and F. Awwad, "Synchronously Triggered GALS Design Templates", Proceedings of the Int'l Symposium on Circuits and Systems (ISCAS-2016), May, 2016, Montreal Canada.

S. Iqtedar, O. Hasan, M. Shafique, J. Henkel, "Formal Probabilistic Analysis of Distributed Resource Management Schemes in On-Chip Systems", Proceedings of the Design, Automation and Test in Europe, 2016, Germany.

F. K. Lodhi, I. Abbasi, F. Khalid, O. Hasan, F. Awwad and S. R. Hasan, "A Self-learning Framework to Detect the Intruded Integrated Circuits", Proceedings of the Int'l Symposium on Circuits and Systems, 2016, Canada.

F. Arshad, H. Mehmood, F. Raza and O. Hasan, "g-HOL - A Graphical User Interface for the HOL Proof Assistant", Proceedings of the Formal Techniques for Safety-Critical Systems, pp. 1–5, 2016, France.

M. Nouman, U. Pervez, O. Hasan and K. Saghar, "Software Testing: A Survey and Tutorial on White and Black-box Testing of C/C++ Programs", Proceedings of the IEEE Region 10 Symposium (TENSYMP-2016), , 2016, Bali Indonesia.

A. Rashid, O. Hasan, "On the Formalization of Fourier Transforms in Higher-order Logic", Proceedings of the Interactive Theorem Proving (ITP-16), , 2016, Nancy France.

[34] A. Athar, A. M. Zafar, R. Asif, A. A. Khan, F. Islam, Y. Ayaz, O. Hasan, "Whole-Body Motion Planning for Humanoid Robots with Heuristic Search", Proceedings of the Intelligent Robots and Systems (IROS-2016), 2016, Daejeon South Korea.

W. Ahmed, O. Hasan and S. Tahar, "Formal Reliability Analysis of Wireless Sensor Network Data Transport Protocols using HOL ", Proceedings of the Wireless and Mobile Computing, Networking and Communications (WiMOB-15), pp. 225-232, Oct, 2015, Abu Dhabi United Arab Emirates.

O. Hasan, U. Sanwal, "Formally Analyzing Continuous Aspects of Cyber-Physical Systems modeled by Homogeneous Linear Differential Equations", Proceedings of the Design, Modeling and Evaluation of Cyber Physical Systems (CyPhy-15), pp. 132-146, Oct, 2015, Netherlands.

M. Ahmad and O. Hasan, "Formal Analysis of Steady State Errors in Feedback Control Systems using HOL-Light", Proceedings of the International Workshop on. Formal Methods for Industrial Critical Systems , Sep, 2015, Florence Italy.

W. Ahmed, O. Hasan, "Towards Formal Fault Tree Analysis using Theorem Proving", Proceedings of the IEEE International Conference on EnaConferences on Intelligent Computer Mathematics (CICM-2015), Aug, 2015, United States.

U. Siddique, O. Hasan, and S. Tahar, "Towards the Formalization of Fractional Calculus in Higher-order Logic", Proceedings of the Conferences on Intelligent Computer Mathematics (CICM-2015), Jul, 2015, United States.

S. Iqtedar, O. Hasan, M. Shafique, J. Henkel, "Probabilistic Formal Verification Methodology for Decentralized Thermal Management in On-Chip Systems", Proceedings of the IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises (WETICE-2015), Jun, 2015, Cyprus.

U. Siddique, O. Hasan, and S. Tahar, "Formal Modeling and Verification of Integrated Photonic Systems", Proceedings of the International Systems Conference (SysCON-2015), Apr, 2015, Canada.

W. Ahmed, O. Hasan and S. Tahar, "Towards Formal Reliability Analysis of Logistics Service Supply Chains using Theorem Proving", Proceedings of the Implementation of Logics (IWIL 2015), 2015, Fiji.

A. Rashid, O. Hasan and K. Saghar, "Formal Analysis of a ZigBee-based Routing Protocol for Smart Grids using UPPAAL", Proceedings of the High-Capacity Optical Networks and Enabling/Emerging Technologies, 2015, Pakistan.

U. Pervez, O. Hasan, K. Latif, S. Tahar, A. Gawanmeh and M. Hamdi, "Formal Reliability Analysis of a Typical FHIR Standard based E-Health System using PRISM", Proceedings of the International Conference on e-Health Networking, Applications and Services, pp. 43-48, 2015, Brazil.

S. Ahmad, O. Hasan, U. Siddique and S. Tahar, "Formalization of Z-Syntax to reason about Molecular Pathways in HOL4", Proceedings of the Brazilian Symposium on Formal Methods (SBMF-2014), pp. 32-47, 2015, Brazil.

M. S. Khan, A. A. Awan, F. Islam, Y. Ayaz and O. Hasan, "Safe Radius based Motion Planning of Hexapod using RRT-Connect", Proceedings of the Information and Automation , pp. 415-418, 2015, China.

U. Pervez, A. Mehmood, O. Hasan, K. Latif, and A. Gawanmeh, "Formal Reliability Analysis of Device Interoperability Middleware (DIM) based E-Health System using PRISM", Proceedings of the IEEE International Conference on e-Health Networking, Applications and Services, 2015, United States.

F.K. Lodhi, S.H. Rafay, O.Hasan and F. Awwad, "Formal Analysis of Macro Synchronous Micro Asychronous Pipeline for Hardware Trojan Detection", Proceedings of the NORCHIP 2015, 2015, Norway.

S.A.A. Bukhari, F. K. Lodhi, O. Hasan, M.Shafique and J.Henkel, "Formal Verification of Distributed Task Migration for Thermal Management in On-chip Multi-core Systems using nuXmv", Proceedings of the International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014), Nov, 2014, Luxembourg.

A. Zaman and O. Hasan, "Formal Verification of Circuit-Switched Network on Chip (NoC)", Proceedings of the International Symposium on System-on-Chip (ISSoC-2014), Oct, 2014, Pakistan.

[33] O. Hasan, W. Ahmed, S. Tahar and M. S. Hamdi, "Reliability Block Diagrams based Analysis: A Survey", Proceedings of the International Conference of Numerical Analysis and Applied Maths (ICNAAM-14),, pp. 850129, Sep, 2014, Rhodes Greece.

W. Gul, S.R. Hasan and O. Hasan, "Yield Aware Inter-logic-layer Communication in 3-D ICs: Some Early Design Stage Recommendations", Proceedings of the International Midwest Symposium on Circuits and Systems (MWSCAS), pp. 222 – 225, Aug, 2014, United States.

F. K. Lodhi, O. Hasan, S. R. Hasan and F. Awwad, "Low Power Soft Error Tolerant Macro Synchronous Micro Asynchronous (MSMA) Pipeline", Proceedings of the IEEE Computer Society Annual Symposium on VLSI (ISVLSI 2014), pp. 601 – 606, Jul, 2014, United States.

W. Ahmed, O. Hasan, S. Tahar, M. S. Hamdi, "Towards the Formal Reliability Analysis of Oil and Gas Pipelines", Proceedings of the Conferences on Intelligent Computer Mathematics, pp. 30–44, Jun, 2014, Portugal.

S. Ahmad, O. Hasan and U. Siddique, "Towards Formal Reasoning about Molecular Pathways in HOL", Proceedings of the IEEE International Conference on Enabling Technologies: Infrastructures for Collaborative Enterprises (WETICE), pp. 378 – 383, Jun, 2014, Parma Italy.

W. Gul, S.R. Hasan and O. Hasan, "Clock Domain Crossing (CDC) for Inter-logic-layer Communication in 3-D ICs", Proceedings of the IEEE International Northeastern Workshop on Circuits and Systems (NEWCAS), Jun, 2014, Trois-Rivicres Canada.

S. Iqtedar, O. Hasan, M. Shafique, J. Henkel, " Formal Probabilistic Analysis of Distributed Dynamic Thermal Management", Proceedings of the Design, Automation & Test in Europe Conference (DATE-2015), Mar, 2014, Grenoble France.

F. K. Lodhi, O. Hasan, S. R. Hasan and F. Awwad, "Hardware Trojan detection in soft error tolerant macro synchronous micro asynchronous (MSMA) pipeline,", Proceedings of the IEEE International Midwest Symposium on Circuits and Systems (MWSCAS 2014), pp. 659 – 662, 2014, United States.

A.H. Qureshi, S. Mumtaz, K. F.Iqbal, Y. Ayaz, F. Ahmad, M.S. Muhammad, O. Hasan, W.Y. Kim, M. Ra, "Triangular Geometry based Optimal Motion Planning using RRT*-Motion Planne", Proceedings of the Advanced Motion Control (AMC)-2014, pp. 380-385, 2014, Japan.

H. Taqdees, O. Hasan, "Formalization of Laplace Transform Using the Multivariate Calculus Theory of HOL-Light", Proceedings of the Logic for Programing Artificial Intelligence and Reasoning (LPAR 2013), pp. 744-758, Dec, 2013, Stellenbosch South Africa.

O. Hasan, A.H. Qureshi, S. Mumtaz, K. F.Iqbal, A. Badar, Y. Ayaz, F. Ahmad, M.S. Muhammad, W.Y. Kim and M. Ra, "Adaptive Potential guided directional-RRT*", Proceedings of the Robotics and Biomimetics (ROBIO-2013), pp. 1887-1892, Dec, 2013, China.

M. Binyameen, O. Hasan, S. Iqbal, "Formal Kinematic Analysis of the Two-Link Planar Manipulator", Proceedings of the International Conference on Formal Engineering Methods (ICFEM-2013), pp. 348–363, Oct, 2013, New Zealand.

O. Hasan, M. Ahmad, "Formal Analysis of Steady State Errors in Feedback Control Systems using HOL-Light", Proceedings of the Design, Automation and Test in Europe (DATE-2013), pp. 1423-1426, Mar, 2013, Grenoble France.

U. Mushtaq, o. Hasan, F. Awwad, "PNOC: Implementation on Verilog for FPGA", Proceedings of the International Conference on Innovations in Information Technology (IIT-2013), pp. 148-151, 2013, Al-Ain United Arab Emirates.

M. Usman, o. Hasan, "Formal Verification of Cyber-Physical Systems: Coping with Continuous Elements", Proceedings of the Computational Science and Its Applications (ICCSA-13), pp. 358–371, 2013, Vietnam.

A. MAshkoor, O. hasan, B. Wolfgang, "Using Probabilistic Analysis for the Certification of Machine Control Systems", Proceedings of the Security and Cognitive Informatics in Homeland Defense (SeCIHD 2013), pp. 305-320, 2013, Germany.

A. Khurram, H. Ali, A. Tariq, O. Hasan, "Formal Reliability Analysis of Protective Relays in Power Distribution Systems", Proceedings of the Formal Methods for Industrial Critical Systems (FMICS-2013), pp. 169–183, 2013, Spain.

M. Ismail, O. Hasan, T. Ebi, M. Shafique,J. henkel, "Formal Verification of Distributed Dynamic Thermal Management", Proceedings of the International Conference on Computer-Aided Design (ICCAD-2013), 2013, United States.

S.H. Taqdees, O. Hasan, "Formal Verification of Continuous Models of Analog Circuits", Proceedings of the Frontiers in Analog CAD (FAC-2013), 2013, Berkeley United States.

N. Saeed A. Inam, A. Khan , "V-HOLT Verifier: An Automatic Formal Verification Tool for Combinational Circuits", Proceedings of the International Mutitopic Conference (INMIC-12), Dec, 2012, Islamabad Pakistan.

G. Helali S. Tahar , O.Hasan, "Formal Verification of the Heavy Hitter Problem", Proceedings of the Canadian Conference on Electrical and Computer Engineering (CCECE12), 2012, Montreal Canada.

O. Hasan, A. Mashkoor , "Formal Probabilistic Analysis of Cyber-Physical Transportation Systems", Proceedings of the International Conference on Computational Science and Its Applications (ICCSA 2012), pp. 419-434, 2012, Brazil.

O. Hasan, F. Islam J. Nasir, U. Malik, Y. Ayaz, "RRT*-Smart: Rapid Convergence Implementation of RRT* Towards Optimal Solution", Proceedings of the International Conference on Mechatronics and Robotics (ICMA 2012), pp. 1651-1656, 2012, China.

O. Hasan, F. K. Lodhi S. R. HasanF. Awwad, "Modified Null Convention Logic Pipeline to Detect Soft Errors in Both Null and Data Phase", Proceedings of the International Midwest Symposium on Circuits and Systems (MWCAS 2012), pp. 402-405, 2012, United States.

O. Hasan, U. Siddiqui, "Analysis Techniques for Fractional Order Systems: A Survey", Proceedings of the International Conference of Numerical Analysis and Applied Maths (ICNAAM-12), pp. 2106-2109, 2012, Greece.

O. Hasan, T. Mhamdi, S. Tahar, "Quantitative Analysis of Information Flow using Theorem Proving", Proceedings of the International Conference on Formal Engineering Methods (ICFEM-12), pp. 119-134, 2012, Japan.

t. mhamdi, o. hasan, s. tahar, "Formalization of Entropy Measures in HOL", Proceedings of the Interactive Theorem Proving (ITP), pp. 233-248, Aug, 2011, Berg en Dal Netherlands.

Osman Hasan, N. Abbasi, S. Tahar, "Formal Lifetime Reliability Analysis Using Continuous Random Variables", Proceedings of the Logic, Language, Information and Computation (WOLLIC-10), No. Lecture Notes in Com, pp. 84-97, Jul, 2010, Brasília Brazil.

Osman Hasan, T. Mhamdi, S. Tahar, "On the Formalization of the Lebesgue Integration Theory in HOL", Proceedings of the Interactive Theorem Proving (ITP-10), No. Lecture Notes in Com, pp. 387-402, Jul, 2010, Edinburgh United Kingdom.

Osman Hasan, F. Lodhi, N. Ramzan, "Towards Precise, Scalable and Automatic Analysis of Analog and Mixed Signal Circuits", Proceedings of the Int'l Conference on Information and Emerging Technologies (ICIET-10), pp. 1-6, Jun, 2010, Karachi Pakistan.

Osman Hasan, F. Hijaz, N. Afzal, T. Ahmad, "Survey of Fall Detection and Daily Activity Monitoring Techniques", Proceedings of the Int'l. Conference on Information and Emerging Technologies (ICIET-10), pp. 1-6, Jun, 2010, Karachi Pakistan.

Osman Hasan, J. Patel, and S. Tahar, "On the Accurate Reliability Analysis of Combinational Circuits Using Theorem Proving", Proceedings of the International NortheasternInt'l. Workshop on Circuits and Systems (NEWCAS-10), pp. 273 - 276, Jun, 2010, Montreal, Quebec Canada.

Osman Hasan, J.B. Hassan, T. Sadani and S. Tahar, "Performance Analysis of Real-Time Rewriting Models", Proceedings of the Computer Systems and Applications (AICCSA-10), pp. 1 - 8 , May, 2010, Hammamet Tunisia.

Osman Hasan, S. Tahar, "Formal Probabilistic Analysis: A Higher-OrderLogic Based Approach", Proceedings of the ASM, Alloy, B and Z (ABZ-2010), No. Lecture Notes in Com, pp. 2-19, Feb, 2010, Orford, Québec, Canada.

Osman Hasan, N. Abbasi, B. Akbarpour, S. Tahar, and R. Akbarpour:, "Formal Reasoning about Expectation Properties for Continuous Random Variables", Proceedings of the Formal Methods (FM'09), No. Lecture Notes in Com, pp. 435-450, Nov, 2009, Eindhoven Netherlands.

Osman Hasan, S.K. Afshar, S. Tahar, "Formal Analysis of Optical Waveguides in HOL", Proceedings of the Theorem Proving in Higher-Order Logics (TPHOLs'09), No. Lecture Notes in Com, pp. 228-243, Aug, 2009, Munich Germany.

Osman Hasan, N. Abbasi and S. Tahar, "Formal Probabilistic Analysis of Stuck-at Faults in Reconfigurable Memory Arrays", Proceedings of the Integrated Formal Methods (IFM-09), No. Lecture Notes in Com, pp. 277-291, Feb, 2009, Düsseldorf Germany.

Osman Hasan, S. Tahar, "Performance Analysis of Wireless Systems using Theorem Proving", Proceedings of the Formal Methods for Wireless Systems (FMWS-08), pp. 3-18, Aug, 2008, Toronto, Ontario Canada.

Osman Hasan, S. Tahar, "Performance Analysis of ARQ Protocols using a Theorem Prover", Proceedings of the Int'l Symposium on Performance Analysis of Systems and Software (ISPASS'08), pp. 85-94, Apr, 2008, Austin, Texas United States.

Osman Hasan, S. Tahar, "Verification of Tail Distribution Bounds in a Theorem Prover", Proceedings of the Numerical Analysis and Applied Mathematics (ICNAAM-07), No. 936, pp. 259-262, Sep, 2007, Corfu Greece.

Osman Hasan, S. Tahar, "Verification of Expectation Properties for Discrete Random Variables in HOL", Proceedings of the Theorem Proving in Higher-Order Logics (TPHOLs-07), No. Lecture Notes in Com, pp. 119-134, Sep, 2007, Kaiserslautern Germany.

Osman Hasan, S. Kort, "Automated Formal Synthesis of Wallace Tree Multipliers", Proceedings of the Int'l Midwest Symposium on Circuits & Systems (MWSCAS-07), pp. 293 – 296, Aug, 2007, Montreal Canada.

Osman Hasan, S. Tahar, "Verification of Probabilistic Properties in the HOL Theorem Prover", Proceedings of the Integrated Formal Methods (IFM-07), No. 4591, pp. 333-352, Jun, 2007, Oxford, UK United Kingdom.

Osman Hasan, S. Tahar, "Formalization of Continuous Probability Distributions", Proceedings of the Automated Deduction (CADE-21), No. Lecture Notes in Com, pp. 2-18, Jun, 2007, Bremen Germany.

Books/Chapters Published

[Book]O. Hasan, S. Tahar, "Formalized Probability Theory and Applications using Theorem Proving. ", IGI Global Pub., ISBN 9781466683150, Mar, 2015.

[Chapter]M. Zaki, O. Hasan, S. Tahar and G. Al-Sammane, "Framework for Formally Verifying Analog and Mixed Signal Designs,Computational Intelligence in Analog?and Mixed-Signal (AMS) and Radio-Frequency (RF) Circuit Design", Springer, ISBN 978-3-319-19871-2, 2015.

[Chapter]O. Hasan and S. Tahar, "Formal Verification Methods", IGI Global, ISBN 9781466658882, Aug, 2014.

[Chapter]S. Nisar and O. Hasan, "Telesurgical Robotics", IGI Global, ISBN 9781466658882, Aug, 2014.

[Chapter]N. Abbasi, O. Hasan, S. Tahar, "Formal Reliability Analysis of Engineering Systems", IGI Global Pub., ISBN 9781466647893, Nov, 2013.

[Chapter]O. Hasan, S. Tahar, "Formal Reliability Analysis of Embedded Computing SystemsO. ", IGI Global Pub., ISBN 978-1466639225, Jun, 2013.

[Chapter]Osman Hasan, S. Tahar, "Reconfigurable Embedded Control Systems: Applications for Flexibility and Agility/Formal Analysis of Real-Time Systems", IGI Global, Vol. 1, Ed. 1, ISBN 9781609600860, Mar, 2011.

Patents

Slip Ring Device with Hollow inner Core, S. Nisar, O.Hasan, IPO Pakistan, Patent 829/2012, issued Dec 06, 2012 Mechanical Interface for Virtual Laparoscopic Surgical Simulator, S.T. Hasan, S. Nisar and O.Hasan , IPO, Patent 773/2012, issued Nov 06, 2012 Human Activity Monitoring and Fall Detection Device, [55] O. Hasan and N. Afzal, IPO Pakistan, Patent 192/2011, issued Jul 14, 2011

Assistant Professor , NUST SEECS
September 2009 – Present (7 years 6 months )

Courses at SEECS

  • Embedded System Design - Undergraduate 
  • ICT Fundamentals - Undergraduate 
  • Formal Methods - Undergraduate 
  • ASIC Design Methodology - Graduate 
  • System Validation - Graduate 

 

ASIC Design Engineer, LSI Logic
June 2001 – May 2003 (1 year 11 months )

R&D Engineer, Intelligent System Design
May 1999 – August 1999 (3 months )

Design Engineer, Pakistan Revenue Automation (Pvt.) Ltd. (PRAL)
September 2008 – April 2009 (7 months )

1998 - 2003

  • ASIC Customer Engineer (June 2001 - May 2003) LSI Logic Corporation, Ottawa, Canada
  • R&D Engineer (May 1999 - September 1999) Intelligent System Design, Islamabad, Pakistan
  • Design Engineer (September 1998 - April 1999) Pakistan Revenue Automation (Pvt.) Ltd., Islamabad, Pakistan