Ismail Kuru

Hello!

I will soon (March 2026) be hosted as a postdoctoral researcher at the Aarhus University Center for Basic Research in Program Verification (CPV), working with Lars Birkedal. Right at this point, I am a computer scientist at Drexel University, where I also did my Ph.D. 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

^ Future

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. (Unfortunately not attended)
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