Hello!
Right now, I am a postdoctoral researcher at the Aarhus University Center for Basic Research in Program Verification (CPV), working with Lars Birkedal, Jean Pichon-Pharabod, and Zongyuan Liu on program logics for Arm, and at the Center for Research and Development on Secure Computer Systems (CRADSEC), Research Organization of Information and Systems (ROIS) in Tokyo, working with Taro Sekiyama on trusted execution environments. Before that, I was a visiting researcher at the National Institute of Informatics (NII). 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
October 2026: Started as postdoctoral researcher at CRADSEC, ROIS in Tokyo, working with Taro Sekiyama, alongside my postdoctoral work at Aarhus CPV.
Summer 2026: Co-advised (with Taro Sekiyama) Keisuke Nishimura, a research intern at NII, on a program logic for inline assembly in Iris.
April 2026: Started as visiting researcher at NII Tokyo, hosted by Taro Sekiyama.
February 2026: Started as postdoctoral researcher at Aarhus University CPV.
November 2025: Talk at the Research Organization of Information and Systems (ROIS), Tokyo. Slides
August 2025: "Modal Verification Patterns for Systems Software" accepted at PLOS 2025, co-located with SOSP 2025.
August 2025: "Modal Abstractions for Virtualizing Memory Addresses" accepted at OOPSLA 2025.
July 2025: Started as postdoctoral researcher at Drexel CCI.
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. (2025, October). Modal Abstractions for Virtualizing Memory Addresses. Proceedings of the ACM on Programming Languages, 9(OOPSLA2), 2338–2366 (OOPSLA 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, October). Modal Verification Patterns for Systems Software. Proceedings of the 13th Workshop on Programming Languages and Operating Systems (PLOS 2025), co-located with SOSP 2025, pp. 25–33. [DOI] [Video]
Manuscripts Under Submission
- Liu, Z., Crawford, F. M., Kuru, I., Pichon-Pharabod, J., & Birkedal, L. Modular and Tractable Verification of a Realistic Ticket Lock on Mixed-Size Arm in Separation Logic. Under submission.
- Kuru, I., & Gordon, C. S. Resource Morphisms for Protocol Indistinguishability. Under submission.
- Kuru, I., & Gordon, C. S. ModFs: Modal Abstractions for Snapshotting Copy-On-Write Filesystems. Under submission.
- Kuru, I., & Gordon, C. S. Deferred Reclamation Is One Discipline: A Scheme-Agnostic Type System for Memory Safety, Mechanized. Under submission.
Manuscripts In Preparation
- Kuru, I., & Gordon, C. S. specNL: Protocols, Resources, Contexts and Specification from Natural Language. In preparation.
- Nishimura, K., Kuru, I., & Sekiyama, T. A Program Logic for Inline Assembly. In preparation.
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
- Research Advisor — Keisuke Nishimura (research intern, National Institute of Informatics), program logic for inline assembly in Iris; co-advised with Taro Sekiyama. Summer 2026.
- 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 (2021–)
- 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