About Me

Hi! I am a Ph.D. student in the School of Computer Science & Engineering at the University of Washington . I am a part of the databases and programming languages research groups, where I focus on developing tools for verified lifting; a novel synthesis and verification based technique for source-to-source translation of programs. I am advised by Alvin Cheung.

Research Interests

I am interested in building programming systems using synthesis, especially for high-performance computing and big-data management.


MetaLift active

MetaLift is a framework for building compilers that target domain-specific languages (DSLs). Unlike traditional syntax-driven compilers, which consists of rules that recognize patterns in the input code and translate them into the target language, MetaLift uses verified lifting to search for possible candidate programs in the target language that the given input can be translated to. This frees the developer from the need to devise, check, and maintain those pesky syntax-driven rules!

Project Website

HALO active

HALO is a compiler that uses Verified Lifting (a combination of synthesis and verification) to automatically retarget legacy image processing stencils to Halide. I am working on this project as part of my internship at Adobe under Shoaib Kamil.

Casper complete

Casper is a compiler that uses Verified Lifting (a combination of synthesis and verification) to automatically retarget sequential Java code to MapReduce frameworks such as Apache Spark.

Project Website · Demo · GitHub

GraSSP complete

A novel approach for automatic parallelization of single-pass array-processing programs with possible data-dependencies. This project is lead by Grigory Fedyukovich.

Project Website


[1]  Automatically Leveraging MapReduce Frameworks for Data-Intensive Applications
      Maaz Bin Safeer Ahmad and Alvin Cheung
      SIGMOD 2018

[2]  Optimizing Data-Intensive Applications Automatically By Leveraging Parallel Data
Processing Frameworks

      Maaz Bin Safeer Ahmad and Alvin Cheung
      SIGMOD 2017 Demo · Honorable Mention for Best Demo Award

[3]  Gradual Synthesis for Static Parallelization of Single-Pass Array-Processing Programs
      Grigory Fedyukovich, Maaz Bin Safeer Ahmad and Rastislav Bodik
      PLDI 2017

[4]  Leveraging Parallel Data Processing Frameworks with Verified Lifting
      Maaz Bin Safeer Ahmad and Alvin Cheung
      SYNT 2016 · Best Student Paper

[5]  Characterizing dengue spread and severity using internet media sources
      Talal Ahmad, Nabeel Abdur Rehman, Fahad Pervaiz, Shankar Kalyanaraman, Maaz       Bin Safeer Ahmad, Sunandan Chakraborty, Umar Saif and Lakshminarayanan       Subramanian
      ACM DEV 2013