Symbolic Execution
Designing targeted control-flow transformations that reduce path explosion and improve bug discovery in dynamic symbolic execution.
Muhammad Hassan
PhD Student in Computer Science, Virginia Tech
I study compiler and program-analysis techniques for improving software reliability, security, and test effectiveness, with current work in symbolic execution and constant-time transformations.
mhassan01@vt.edu · Google Scholar · GitHub · LinkedIn · CV
About
I work on program analysis and compiler techniques for dependable software.
I am a PhD student in Computer Science at Virginia Tech, advised by Dr. Kirshanthan Sundararajah. My research interests are in compilers, programming languages, software testing, and security, with an emphasis on techniques that make program behavior easier to analyze and validate.
Before Virginia Tech, I completed my B.S. in Computer Science at Lahore University of Management Sciences, where I worked on software debloating and security evaluation. I am especially interested in research that combines principled compiler ideas with empirical systems evaluation.
News
- 2026 Our work on targeted control-flow transformations for dynamic symbolic execution appears in PACMPL/OOPSLA.
- 2025 Started the PhD program in Computer Science at Virginia Tech and joined the Language and Compiler Design Lab.
- 2023 Presented work on evaluating container debloaters at IEEE SecDev.
Research
Research themes.
Secure Compilation
Developing compiler transformations that reduce timing side-channel leakage and preserve constant-time behavior across optimized code.
Security Evaluation
Evaluating software and container debloating techniques across correctness, CVE mitigation, attack-surface reduction, and usability.
Publications
Publications.
PACMPL 10(OOPSLA1), 2026
Taming the Hydra: Targeted Control-Flow Transformations for Dynamic Symbolic Execution
Charitha Saumya, Muhammad Hassan, Rohan Gangaraju, Milind Kulkarni, Kirshanthan Sundararajah.
IEEE Secure Development Conference 2023
Evaluating Container Debloaters
Muhammad Hassan, T. Tahir, M. Farrukh, A. Naveed, A. Naeem, F. Shaon, F. Zaffar, A. Gehani, S. Rahaman.
Research Experience & Artifacts
Academic work, systems, and evaluation artifacts.
Graduate Research Assistant
Investigating compiler transformations for constant-time code and control-flow merging, with experimental evaluation in LLVM and KLEE.
Software Engineer
Developed interactive 2D/3D annotation systems for digital-twin models, including rendering optimizations and synchronized spatial transformations.
Research Assistant
Studied Docker image debloating through benchmarking, correctness testing, CVE analysis, and security-focused evaluation.
Research Code & Artifacts
-
Control Flow Transformations for Symbolic Execution
Targeted compiler transformations for mitigating path explosion in dynamic symbolic execution. Code and experiment scripts are available with the OOPSLA artifact.
-
Debloat Bench
Benchmarking framework for evaluating debloating correctness, size reduction, security, and time.
Skills
Research and engineering toolkit.
Research Tools
LLVM/Clang, KLEE, SMT solvers, program analysis, Docker, Vagrant
Languages
Python, C/C++, Assembly, JavaScript, Solidity, Haskell
ML & Web Frameworks
Angular, React, Node, Django, TensorFlow, PyTorch, OpenCV
Systems & Design
Linux, shell scripting, PostgreSQL, Three.js, Konva.js, Figma
Contact
Open to research conversations and collaborations.
The easiest way to reach me is by email. You can also find my work and professional profile through the links below.