Kinan Dak Albab
LinkedIn | Github | Resume

Boston University
Department of Computer Science
111 Cummington St
Boston, MA, 02215


I am a PhD student in the Department of Computer Science at Boston University. I was advised by Prof. Andrei Lapets. I work closely with Professors Prof. Assaf Kfoury, Mayank Varia and Prof. Azer Bestavros . I joined the PhD programing in September 2016. I am currently interning at Google working with Dr. Konstantin Weitz and Dr. Stefan Heule on formal verification and testing of network switches.

My research lies in building and reasoning about computer systems and programs. I have been working on desiging cryptographic protocols for distributed systems at scale to ensure security and privacy. I am interested in utilizing formal program analysis techniques (proof assistants) and novel programming models and frameworks to reason about the correctness and security of whole system at large.

I recieved a B.S. in Computer Science in 2015 from the American University of Beirut with a Minor in Mathematics. I mainly worked with Prof. Paul Attie and Prof Mohamad Jaber.

You can find my Resume here.


I work on a variety of research projects, spanning areas from systems design, applied cryptography, and formal verification.

I am part of the MPC research group at the Hariri Institute for Computing and the Software and Innovation Application Lab (SAIL), where we are working on a variety of frameworks and protocols for desiging and implementing MPC applications at scale. This includes JIFF, a customizable general-purpose javascript framework for Web-based MPC. Effecient and Scalable protocols for iterative graph algorithms including network distance and route recommendation. We deployed many of our techniques and framework in several real-world deployments with the Boston Women's Workforce Council and the Pacesetters initiative. This work is supported by NSF and the Honda Research Institute.

I am working on verifying concrete implementations of the snapping mechansim in the Coq theorem prover. The verification combines probabilistic coupling based relational reasoning with reasoning about floating point arithmetic and errors. Joint work with Jiawen Liu and Marco Gaboardi.

I am running an informal reading group on verifying operating systems kernels and hypervisors, with a particular focus on security and temporal isolation. I am also co-organizing the programming language reading group for Fall 2019 at Boston University with Will Blair.

I was a visting student at MIT CSAIL with Prof. Dina Katabi in the Networks @ MIT research group on the Emrald project. I worked on desiging, implementing, and deploying various systems running on IoT devices and on the cloud, for sensing, streaming, collecting, and analysing data at scale.

I worked with
Prof. Paul Attie on Subtractive Model Repair. Given a model (a Kripke Structure) of a sequential or concurrent program and specifications (CTL Formula), we attempt to repair the structure by removing states and transitions. We use the model and specifications to construct a SAT formula that is satisfiable if and only if the model is repairable, we use the resulting satisfying assignemnt to deduce which states and transitions are removed from the structure. We use a pair-wise representation of the model to avoid state explosion as the number of processes grow. We developed a tool Eshmun that can be used for repairing Kripke Structures, as well as a variety of other features (Model Checking, Abstractions, ...).

Industry Work

Google: I am interning at Google during the summer of 2020. I am working with the core infrastructure team on formal verification and testing of network switches, by analyzing SDN programs and generating test packets that cover path combinations in the data and control plane, using SMT solving.

Software Application & Innovation Lab: I was a software engineering fellow at the Software & Application Innovation Lab (SAIL), a professional research software engineering lab within Boston University. I worked on developing a back-end platform that supports performing MPC on-the-fly between clients using different devices including mobile and web applications. I have led and produced several open source frameworks for secure computation, and worked with and mentored several interns at SAIL from high-schoolers to graduate students.

Interactive Life: I worked as a senior software developer for Interactive Life from August 2015 to August 2016. Interactive Life is a startup based in Seattle, WA. It provides apps and services for businesses and organizations to help them engage and reach to a wide range of users. The company provided solutions for a wide range of sectors including health-care (clinics), interactive TV, churches, and media agencies. Some of my responsibilites included:
Fetch: During my undergraduate studies, I worked as an intern for Fetch in the summer of 2014. I worked on a web application that is used by companies and service providers to analyse their clients comments on social media. The web application would gather data from social media, and use sentiment analysis to produce reports that include the overall satisfaction and amount of engagment of clients. I have worked as a freelancer in 2014-2015 on different projects, mostly small and medium sized websites and web applications, as well as one desktop application (java-based).


Boston University:

American University of Beirut:





Teaching Excellence Award: Boston University, Department of Computer Science, 2020. Vivli and Microsoft datatheon on Privacy and Utility of Rare Diseases Datasets: Award for Outstanding Graduate Submission, June 2019.

Hariri Institute for Computing (HIC @ BU) Gradute Student Fellow 2017-2020.

Mark Sawaya Excellence Award , Best Graduating Student in Computer Science (AUB), 2015.

AUB Dean's Honor List: Fall 2013, Spring 2014.

1st Place in ACM - Lebanese Collegiate Programming Contest (Team Khawarizmi), 2015.

1st Place in AUB's Supernacci Math Programming Competition (Team 0xdeadbeef), 2015.