Adnan Rashid

Functional Safety Engineer at ReasonX Labs, developing safety assurance strategies for autonomous systems — from requirements engineering and traceability to safety analysis. With a PhD in Formal Methods, and prior position as Research Fellow at Concordia University, developed deep expertise in formal verification of safety-critical systems such as robotics, autonomous vehicles, 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 analysis. Enthusiastic about contributing formal methods expertise to safety-critical system development, verification engineering, and reliability analysis.

Research Focus

Safety Analysis of Autonomous Systems

Deep safety analysis of Robotics and Autonomous Vehicles complying with ISO 26262 and IEC 61508.

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.

Selected Publications

Formal Verification of Universal Numbers using Theorem Proving

Adnan Rashid, Ayesha Gauhar, Osman Hasan, Sa'ed Abed, Imtiaz Ahmad

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.

Universal NumbersPositsHigher-order LogicTheorem Proving

Formal verification of robotic cell injection systems up to 4-DOF using HOL Light

Adnan Rashid, Osman Hasan

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.

Robotic cell injection systemsFormal verificationTheorem ProvingHigher-order logic

Formalization of Transform Methods using Higher-order-logic Theorem Proving

Adnan Rashid

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.

Theorem ProvingTransform MethodsControl SystemsSignal Processing

Experience

Functional Safety Engineer

ReasonX Labs

Feb 2025 — Present

Performing deep safety analysis of autonomous systems. Establishing requirements engineering and traceability frameworks for autonomous systems.

Safety AnalysisAutonomous SystemsRequirement Engineering

Research Fellow

Concordia University

Hardware Verification Group (HVG)

Jul 2023 — Jan 2025

Leading advanced research in formal verification of safety-critical systems using HOL Light and Isabelle/HOL. Advising graduate students on their research topics.

Theorem ProvingSafety-critical SystemsFormal VerificationGraduate Advising

Assistant Professor

National University of Sciences and Technology (NUST)

School of Electrical Engineering and Computer Science

Feb 2020 — Jun 2023

Led System Analysis and Verification (SAVe) research laboratory focusing on safety-critical system verification and reliability analysis. Taught graduate and undergraduate-level courses in computation theory, compiler construction, and formal methods.

Research LeadershipTeachingFormal MethodsSystem Verification