Kinan Dak Albabbabman@bu.edu
LinkedIn | Github | CV
Department of Computer Science
111 Cummington St
Boston, MA, 02215
BiographyI am a PhD student in the Department of Computer Science at Boston University. My advisor is Prof. Assaf Kfoury. My research interests lie in Program Verification. I am interested in developing automated tools and techniques that help ensure the correctness of software. I joined the PhD program in September 2016.
I recieved a B.S. in Computer Science in 2015 from the American University of Beirut with a Minor in Mathematics. I worked mainly with Prof. Paul Attie and Prof Mohamad Jaber.
You can find my CV here.
ResearchI am interested in using Formal Methods and Programming Languages techniques to come up with general purpose or domain specific tools for ensuring a programs correctness. I worked with Prof. Paul Attie on Subtractive Model Repair. Given a model (a Kripke Structure) 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. I am developing (and maintaining) a tool Eshmun that can be used for repairing Kripke Structures, as well as a variety of other features (Model Checking, Abstractions, ...). We also support repair of concurrent Kripke Structures that model Concurrent Programs. We use pairwise repair to avoid state-explosion. We are working on extending the theory and tool to infinite state machines.
I am currently working on performing iterative graph algorithms efficiently in Secure Multiparty Computation (MPC). Where multiple parties can collaborate to perform aggregates and analysis on their private networks without revealing it. This is a joint work with another PhD student Rawane Issa, as well as the MPC group at the Hariri Institue for Computing. We have developed a technique for partitioning the graph and only performing MPC on a small part of the graph. We use symbolic execution to unroll loops into expressions (parse-trees), optimize these expressions and simplify them, then evaluate them using MPC. We exploit algebraic properties of the operators in the code to reduce the number of expensive operators. We are currently working on a workshop paper detailing this work. We hope to extend this in the feature to a variety of other graph algorithms and problems.
I am interested in combining theorem proving and popular imperative languages (in particular Java), to achieve high levels of confidence in the correctness of code. I am exploring different ideas in this direction and I hope to begin work in this soon.
Industry WorkI worked as a senior software developer for a startup 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:
- Android Mobile Development: I participated in developing an Android SDK that provides a large API for common functionalities between the different apps, I worked extensively on the design of the SDK and its interactions with the apps. I also worked on some of the apps implementations and UI.
- Backend Development: I was responsible for developing and maintaining a specialized backend server that delievers and trigger data to the mobile apps through RESTful APIs. The backend provided authentication and profile management for the end-users as well.
- Architecture: I also worked on the overall architecture of the platform, including designing the different backend servers and their roles, the SDK and libraries for both Android and iOS, and choosing technologies for different components.
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).
- CMPS 272: Operating Systems (Fall 2015): Teaching assistant (American University of Beirut).
- CMPS 211: Discrete Structures (Spring 2016): Teaching assistant (American University of Beirut).
- CMPS 257: Theory of Computation (Fall 2014 and 2015): Peer tutoring (American University of Beirut).
- CS 332: Theory of Computation (Spring 2017): Teaching Fellow (Boston University).
Model and Program Repair via SAT Solving
Paul C. Attie, Kinan Dak Al Bab, and Mohamad Sakr
To appear in ACM Transactions on Embedded Computing Systems (TECS)
Model and Program Repair via SAT Solving
Paul C. Attie, Ali Cherri, Kinan Dak Al Bab, Mohamad Sakr, and Jad Saklawi
13th ACM-IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE'15)
September 2015, Austin, Texas, USA.
A High-level Modeling Language for the Efficient Design, Implementation, and Testing of Android Applications.
Mohamad Jaber, Ylies Falcone, Kinan Dak-Al-Bab, John Abou-Jaoudeh and Mostafa El-Katerji.
International Journal on Software Tools for Technology Transfer (STTT)
AwardsMark 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.