About Me

Hi! I am a final year Ph.D. student in the Paul G. Allen School of Computer Science & Engineering at the University of Washington. I am a part of the programming languages and databases research groups, where I work on machine-aided programming. I am interested in harnessing advances in program synthesis and machine learning to develop tools that enable programmers to write high-level programs that function as well or better than manually crafted low-level programs created by experts. I am advised by Alvin Cheung.

My current research focuses on Verified Lifting; a program synthesis and verification based technique for discovering code-transformations across different programming abstractions. In 2019, I interned at Intel's software pathfinding team, where I developed a proof-of-concept compiler for Intentional Programming in C++. In Summer 2017, I interned at Adobe, where I built Dexter, a compiler for lifting legacy image processing code C++ from Photoshop to Halide. In Summer 2015, I interned at Tableau, where I worked on improving the incremental extract refresh process in the Tableau Data Engine.

In June 2014 I received my B.S. in Computer Science at the National University of Computer & Emerging Sciences and was awarded the University Silver Medal for highest standing in the graduating class.


Rake active

Rake is a new tool that uses program-synthesis to transform lower-level DSL IRs to complex high-level instruction sets found in modern hardware, such as the Hexagon HVX ISA.

Kriek active

Kriek is a new DSL for high-performance tensor computation. Our vision for this IR is to use scheduling primitives coupled with learned cost-models to decompose algorithms hierarchically into smaller sub-problems, which are then implemented dynamically using program synthesis.This project is a collaborative effort with Rastislav Bodik, Sam Kaufman and Krzysztof Drewniak.

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

Dexter complete

Dexter is a new tool to automatically translate image processing functions from a low-level language to a high-level domain-specific language (DSL), allowing such functions to leverage the cross-platform optimizations enabled by DSLs. This project is an outcome of my internship at Adobe and is done in collaboration with Shoaib Kamil and Jonathan Ragan-Kelley.

Project Website · Slides · GitHub · Demo (Coming Soon)

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 · Talk · Slides · 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 · Talk


Automatically Translating Image Processing Libraries to Halide
Maaz Bin Safeer Ahmad, Jonathan Ragan-Kelley, Alvin Cheung and Shoaib Kamil
SIGGRAPH ASIA 2019 · BibTex · DOI · Slides

Optimizing Data-Intensive Applications Automatically By Leveraging Parallel Data Processing Frameworks
Maaz Bin Safeer Ahmad and Alvin Cheung
SIGMOD 2017 Demo · BibTex · DOI · Honorable Mention for Best Demo Award

Gradual Synthesis for Static Parallelization of Single-Pass Array-Processing Programs
Grigory Fedyukovich, Maaz Bin Safeer Ahmad and Rastislav Bodik
PLDI 2017 · BibTex · DOI · Talk

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

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 · BibTex · DOI