Muhammad Hassan

Muhammad Hassan

PhD student in computer science at Virginia Tech

I study compiler transformations for program analysis and security, with a focus on symbolic execution, parallel SMT solving, and constant-time code.

mhassan01@vt.edu Google Scholar GitHub LinkedIn CV

About

I am a PhD student in computer science at Virginia Tech and a Pratt Fellow. I am advised by Dr. Kirshanthan Sundararajah in the Language and Compiler Design Lab.

I earned a BS in computer science from Lahore University of Management Sciences, where I worked on software debloating and security evaluation. I later worked as a software engineer at Aerodyne Group, developing 3D tools.

Publications

  1. Taming the Hydra: Targeted Control-Flow Transformations for Dynamic Symbolic Execution

    Charitha Saumya*, Muhammad Hassan*, Rohan Gangaraju, Milind Kulkarni, Kirshanthan Sundararajah.

    PACMPL 10(OOPSLA1), 2026

    * These authors contributed equally.

    The artifact received the Functional, Reusable, and Results Reproduced badges.

    Paper Artifact Visualization

  2. ThunderFork: Splitting SMT Queries with Targeted Control-Flow Transformations

    Muhammad Hassan.

    SPLASH/ISSTA Student Research Competition, 2026 (Extended abstract)

    Extended abstract

  3. Evaluating Container Debloaters

    Muhammad Hassan*, Talha Tahir*, Muhammad Farrukh, Abdullah Naveed, Anas Naeem, Fareed Zaffar, Fahad Shaon, Ashish Gehani, Sazzadur Rahaman.

    IEEE Secure Development Conference 2023

    * These authors contributed equally.

    Paper Code

Research Projects

  • Control-Flow Transformations for Symbolic Execution

    LLVM transformations reduce path explosion in KLEE. Selected kernels completed symbolic execution in seconds, while unmodified KLEE timed out after one hour. On libosip 4.0.0, KLEE found a bug in approximately 18.5–20.2 hours after transformation, while the original programs reached the 24-hour timeout.

    Paper Artifact

  • ThunderFork for Parallel SMT Solving

    ThunderFork uses cost-guided control-flow transformations to split SMT queries for parallel solving. Across 44 benchmarks, it was faster than Z3 on 25, tied on 18, and slower on one. Compared with cvc5, it was faster on 17 benchmarks and tied on nine. Both ThunderFork and cvc5 timed out on the remaining 18.

    Extended abstract

  • Constant-Time Code

    I am developing compiler transformations for constant-time code.

  • Debloat Bench (BloatProfiler)

    A framework for evaluating functional correctness, vulnerability mitigation, and image size reduction in container debloating.

    Code Paper

  • LLM-Based Debloating

    This pipeline combines language models, retrieval-augmented generation, and LLVM coverage analysis for software debloating.

Research Interests

Symbolic Execution

I develop LLVM transformations that reduce path explosion in KLEE.

OOPSLA 2026

SMT Solving

I develop cost-guided control-flow transformations that split SMT queries for parallel solving.

ThunderFork

Secure Compilation

I investigate compiler transformations for constant-time code and protection against timing side channels.

Software Debloating

My work examines container debloating tools and approaches using language models and coverage analysis.

SecDev 2023

News

  • Oct 2026 I presented Taming the Hydra at OOPSLA 2026 and ThunderFork at the SPLASH/ISSTA Student Research Competition.
  • May 2026 I received the Pratt Fellowship.
  • Mar 2026 The artifact for Taming the Hydra received three artifact evaluation badges.
  • Mar 2026 I passed my PhD qualifying exam.

Teaching

CS 5244 Web Application Development

Virginia Tech · Fall 2025, Fall 2026

Graduate Teaching Assistant

CS 4804 Introduction to Artificial Intelligence

Virginia Tech · Spring 2026

Graduate Teaching Assistant

Experience

Graduate Research Assistant

Virginia Tech · Jan 2025 - Present

I develop LLVM transformations for symbolic execution and parallel SMT solving. I also investigate compiler transformations for constant-time code.

Software Engineer

Aerodyne Group · Jul 2023 - Dec 2024

I developed interactive 2D and 3D annotation tools for digital twins. I improved rendering performance from 15 to 240 frames per second.

Research Assistant

Lahore University of Management Sciences · Jan 2023 - Oct 2024

I developed and evaluated BloatProfiler, a framework for benchmarking Docker image debloating.

Honors and Presentations

Honors

  • May 2026 Pratt Fellowship, Virginia Tech

Talks

  • Oct 2026 Taming the Hydra: Targeted Control-Flow Transformations for Dynamic Symbolic Execution. Talk, OOPSLA 2026
  • Oct 2026 ThunderFork: Splitting SMT Queries with Targeted Control-Flow Transformations. Poster and talk, SPLASH/ISSTA Student Research Competition

Technical Skills

Compilers and Program Analysis

LLVM, Clang, KLEE, static analysis, symbolic execution

SMT Solvers and Tools

Z3, cvc5, STP, SMT-LIB

Languages

C, C++, Python, assembly, JavaScript, TypeScript, Solidity, Haskell

Systems and Tools

Linux, Git, Docker, Vagrant, CMake, Bash, PostgreSQL

Web and ML Tools

Angular, React, Node.js, Django, TensorFlow, PyTorch, OpenCV

Contact

For research inquiries or collaborations, email me at mhassan01@vt.edu.

mhassan01@vt.edu CV