Adnan Rashid
Research Fellow at Concordia University with a PhD in Formal Methods, specializing in formal verification and safety analysis of safety-critical systems such as robotics, autonomous vehicles, satellites, and smart grids. Proven track record of applying rigorous mathematical verification techniques to solve real-world engineering challenges, complemented by expertise in reliability engineering and safety assessment. Enthusiastic about contributing formal methods expertise to safety-critical system development, verification engineering, and reliability analysis.
You can explore my research contributions through my , learn about my technical background, or connect with me on LinkedIn.
Research Focus
Higher-Order Logic Theorem Proving for System Verification
Development of formal verification frameworks using HOL Light, HOL4, and Isabelle/HOL for safety-critical systems. Formalized mathematical foundations, including transform methods, dynamical analysis, and reliability models, to enable machine-checked proofs of system correctness and safety properties.
System Dynamics Formal Modeling and Analysis
Mathematical modeling of system dynamics using differential equations, with applications to the analysis of robotic systems, vehicle platoons, and UAVs.
Safety Analysis of Autonomous Systems
Deep safety Assessment of Robotics and Autonomous Vehicles Complying with ISO 26262 and IEC 61508.
Selected Publications
Formal Verification of Universal Numbers using Theorem Proving
Journal of Electronic Testing: Theory and Applications (JETTA 2024)
Presents first higher-order-logic (HOL) formalization of Unum-III (posits) using the HOL Light theorem prover.
Formal verification of robotic cell injection systems up to 4-DOF using HOL Light
Formal Aspects of Computing (FAOC 2020)
Proposes a higher-order-logic (HOL) theorem proving based framework for analyzing the dynamical behavior of the robotic cell injection systems upto 4-DOF. The proposed analysis enables us to identify some discrepancies in the simulation and model checking based analysis of the same robotic cell injection system.
Formalization of Transform Methods using Higher-order-logic Theorem Proving
PhD Thesis, NUST-SEECS, 2019
Comprehensive formalization of mathematical transform methods including Laplace and Fourier transforms using HOL theorem proving, enabling formal analysis of control systems and signal processing applications.
Experience
Research Fellow
Concordia University • Hardware Verification Group (HVG)
Leading advanced research in formal verification of safety-critical systems using HOL Light and Isabelle/HOL. Performing deep safety analysis of autonomous systems. Advising graduate students on their research topics.
Assistant Professor
National University of Sciences and Technology (NUST)
Led System Analysis and Verification (SAVe) research laboratory focusing on safety-critical system verification and reliability analysis. Designed and delivered under-graduate and graduate-level courses in computation theory, compiler design, and algorithms analysis. Supervised FYPs and MS thesis projects.
Researcher
System Analysis and Verification (SAVe) Lab, NUST-SEECS
Pioneered formalization of mathematical transform methods (Laplace and Fourier) in a theorem prover, for analog circuits and control system verification, creating the first comprehensive library of verified transform methods and their associated properties. Implemented formal verification frameworks for synthetic biological circuits and UAVs controllers and robotic cell injection systems.
Contact
If you would like to discuss potential opportunities in formal verification, safety analysis, or reliability engineering, I'm always open to connecting.