Hello!
I am a postdoctoral researcher at the Aarhus University Center for Basic Research in Program Verification (CPV), working with Lars Birkedal. I am also holding a visiting researcher position at Center for Research and Development on Secure Computer Systems (CRADSEC) / National Institute of Informatics (NII) in Research Organization of Information and Systems (ROIS) collaborating with Taro Sekiyama. I got my Ph.D. at Drexel University in the field of programming languages, logic, and verification with Colin S. Gordon.
Before Drexel, I was a Senior Software Engineer at Crytek. Before Crytek, I graduated with an M.S. degree from Koc University in 2015. Thanks to Microsoft Research for supporting me through a Microsoft Research scholarship during my M.S. degree studies.
My work focuses on understanding software systems, primarily the low-level ones, through mathematical proof. On this mission, I am interested in building program logics, the ergonomics of specifications within these logics, and, most recently, articulating (drawing them!) proofs and specifications for programs. The complete set of projects constituting my work can be found in Contingent Systems Project which includes systems (OS kernel, filesystem, machine models, etc.) and Rocq (mostly Iris) proofs for them.
My Ph.D. thesis was funded by the NSF Career grant.
Talks & News
March 2026: Started as postdoctoral researcher at Aarhus University CPV and visiting researcher at NII Tokyo.
November 2025: I gave a talk to the ROIS Group at NII Japan. Slides
August 2025: "On Verification Patterns for Low-Level Systems via Modal Abstractions" accepted at PLOS 2025, co-located with SOSP 2025.
August 2025: "Modal Abstractions for Virtualizing Memory Addresses" accepted at OOPSLA 2024–2025.
July 2025: Continuing research at Drexel as a researcher.
March 2025: Defended my thesis! Slides
September 2024: Hosted as a research fellow at Drexel CCI.
May 2024: Talk at UPenn PL Club.
May 2024: Talk at Princeton PL Group.
May 2024: Talk at NJPLS 2024 at NYU.
April 2024: Talk at Languages, Systems and Data Seminar 2024 at UC Santa Cruz.
March 2024: Defended my thesis proposal.
May 2023: Talk at NJPLS 2023 at UPenn.
Representative Papers
Conference Papers
- Kuru, I., & Gordon, C. S. (To be submitted January 2026). Modal Understanding of Modularity of State Transition Systems.
- Kuru, I., & Gordon, C. S. (2025, August). Modal Abstractions for Virtualizing Memory Addresses. OOPSLA 2024–2025. [DOI] [Video]
- Kuru, I., & Gordon, C. S. (2019, April). A Type System for Read-Copy-Update Concurrency. European Symposium on Programming (ESOP 2019). [DOI]
Workshop Papers
- Kuru, I., & Gordon, C. S. (2025, August). On Verification Patterns for Low-Level Systems via Modal Abstractions. PLOS 2025, co-located with SOSP 2025. [DOI] [Video]
Tech Reports
- Kuru, I., & Gordon, C. S. (2025). Modal Verification Patterns for Systems. CoRR, abs/2506.01719.
- Kuru, I., & Gordon, C. S. (2024). Modal Abstractions for Virtualizing Memory Addresses. CoRR, abs/2307.14471.
- Kuru, I., & Gordon, C. S. (2019). Safe Deferred Memory Reclamation with Types. CoRR, abs/1811.11853.
Ph.D. Thesis
- Kuru, I. (2025). Modal Abstractions for Operating System Kernels. Graduate School of the College of Computing and Informatics, Drexel University.
Other Papers (Before Ph.D.)
Conference Papers
- Kuru, I., Matar, H. S., Cristal, A., Kestor, G., & Unsal, O. (2013). PaRV: Parallelizing Runtime Detection and Prevention of Concurrency Errors. In S. Qadeer & S. Tasiran (Eds.), Runtime Verification (pp. 42–47). Springer Berlin Heidelberg.
Book Chapters
- Cristal, A., Ozkan, B. K., Cohen, E., Kestor, G., Kuru, I., Unsal, O., Tasiran, S., Mutluergil, S. O., & Elmas, T. (2015). Verification Tools for Transactional Programs. In R. Guerraoui & P. Romano (Eds.), Transactional Memory: Foundations, Algorithms, Tools, and Applications (pp. 283–306). Springer. [DOI]
Workshop Papers
- Kuru, I., Kulahcioglu Ozkan, B., Mutluergil, S. O., Tasiran, S., Elmas, T., & Cohen, E. (2014). Verifying Programs under Snapshot Isolation and Similar Relaxed Consistency Models.
- Matar, H. S., Kuru, I., Tasiran, S., & Dementiev, R. (2014). Accelerating Precise Race Detection Using Commercially-Available Hardware Transactional Memory Support.
M.S. Thesis
- Kuru, I. (2015). Static Methods for Checking Correctness of Programs on Relaxed Memory Systems. Graduate School of Engineering, Koc University.
Awards & Grants
- Scholarship for School on Univalent Mathematics Workshop, University of Minnesota Twin Cities, 2024.
- Scholarship for DeepSpec Summer School, Princeton University, 2018.
- Scholarship for PLMW at ICFP, UK, 2017.
- Travel Grant. Microsoft Research Visitor Grants (Multiple), hosted by Dr. Matthew Parkinson, UK, 2014.
- Graduate School Scholarship. One of 18 Microsoft Research Europe PhD Scholarship recipients, 2011–2014.
- Travel Grant. Koc University, for the VCLA Winter School in Vienna, 2012.
- Travel Grant. Inria-Paris Visitor Grants (Multiple), hosted by Dr. Albert Cohen, France, 2011.
Teaching
- Teaching Assistant — CS 360: Programming Languages, taught by Krzysztof Nowak. Drexel University, Summer 2019.
- Teaching Assistant — SE 311: Software Engineering, taught by Yuanfang Cai. Drexel University, Winter 2019.
- Teaching Assistant — Software Engineering, taught by Serdar Tasiran. Koc University, Spring 2012.
Service
- SIGPLAN-M Long-Term Mentor
- OOPSLA'24 Subreviewer
- POPL'20 Artifact Evaluation Committee
- OOPSLA'19 Artifact Evaluation Subreviewer
- PLDI'18 Student Volunteer
- SEFM'13 Subreviewer
- SAS'13 Subreviewer
- RV'12 Subreviewer