Welcome to my homepage !

Introduction

I am a software engineer at Google Inc. This site contains my academic work before I joined Google.

Before Google, I was a post-doctoral researcher 
supervised by Dr. Koushik Sen, in the Parallel Computing Laboratory (ParLab) at UC Berkeley
. In my research, 
I worked on developing methods and tools for debugging and verification of concurrent software. 

I am an alumnus of the Koc University Research Center for Multicore Software Engineering. I received my Ph.D. in Computer Engineering at Koc University in August 2010. My advisors were Dr. Serdar Tasiran (Koc University) and Dr. Shaz Qadeer (Microsoft Research). This web site contains material describing the work I produced during my graduate study; also see myresearch statement.

Outline
In this page, I briefly overview my recent research work. You can learn more about my work by reading my papers, looking at my talk slides, or visiting our lab's web site. My teaching experience can be found here. This site also provides my short biography and contact information. I try to provide links to recent and upcoming events related to my research field. 

Research interests
My research interests are formal methods, algorithms, and tools for the debugging, analysis, and verification of concurrent software. I focus on concurrent implementations of data structures and services that form the backbone of many widely-used systems such as databases, Internet servers, and file systems. 

Concurrency-related bugs are difficult to detect, reproduce, and diagnose using code review and testing-based techniques originally developed for sequential programs. This difficulty creates demand for new program analyses that are capable of examining the software with high coverage of its executions and catching subtle bugs. My research goal is to develop methods and software tools to respond to this demand, selecting between runtime and static techniques that best fit the objectives of the work.

Research projects

Recent projects:
  • NDSEQ (NonDeterministic SEQuential Specifications) is a novel lightweight specification method to specify the correctness of parallelism in a program. In particular, NDSEQ specification of a program specifies the correctness of a program's parallelism using a sequential version of the program with controlled nondeterminism. Such a nondeterministic sequential specification allows (1) the correctness of parallel interference to be verified independently of the program's functional correctness, and (2) the functional correctness of a program to be understood and verified on a sequential version of the program, one with controlled nondeterminism but no interleaving of parallel threads. For details, please see our PLDI 2010 paper here.
  • concurrit is a new testing framework I am working on for testing multithreaded programs. The goal is to combine and integrate the advanced techniques for concurrent programs and provide them in a flexible, usable, and effective testing framework for programmers to use continuously during the software development process.
  • KUDA is a framework for performing runtime monitoring using GPUs as accelerators. The idea is to separate the runtime burden of a runtime analysis such as data-race checking from the application threads and use GPU threads to perform the actual checking of the execution in a highly parallel manner. See our technical report titled "Rethinking Runtime Verification on Hundreds of Cores: Challenges and Opportunities" for more information about out vision and approach. The KUDA tool is open source and available for download at http://kuda.codeplex.com.
During my graduate study at Koc University, I led both the technical and practical development of three projects. More information about them and my earlier projects can be found here.
  • QED is a static proof system to verify concurrent programs for prevalent correctness criteria including assertions and linearizability, combining strengthful techniques like reduction, abstraction and auxiliary variables. QED was awarded “Best project representing an innovative use of Microsoft technology” in the ACM Student Research Competition (SRC) hosted in ICSE 2010. The QED tool is open source and available for download at http://qed.codeplex.com.
  • Goldilocks is a Java runtime that can precisely monitor programs for data-races, and throw DataRaceException to the attention of the programmer. This work was published in the November 2010 Communications of the ACM Research Highlights (Nominated in January 2009).
  • VYRD  is an extensible and lightweight runtime verification framework for I/O and view refinement, which are novel correctness criteria for concurrent data structures, and provides significantly more thorough checking than testing.
Conclusion
This web site mostly contains information about my professional life in Computer Science research. If you are also interested in my non-professional life, please visit here.