Uğur Y. Yavuz
Uğur /uˈɣur/ Y. Yağmur: /jɑːˈmur/ Yavuz /jaˈvuz/
uyyavuz (at) bu (dot) edu
CV

about me

I am a Ph.D. student in the Department of Computer Science at Boston University, advised by Marco Gaboardi and Alley Stoughton. I am a member of the Principles of Programming and Verification (POPV) group at BU.

My research focuses on the specification and formal verification of concurrent algorithms and systems. I am particularly interested in proof development using tools such as TLA+/TLAPS.

publications

talks

news

Refereed publications
Formal Machine-Verification of MemSnap: an Efficient, Far-Future Linearizable Snapshot Algorithm
Siddhartha Jayanti, Ugur Y. Yavuz
37th ACM Symposium on Parallelism in Algorithms and Architectures [SPAA '25]
Distinguished Paper Award
PDF Code
Meta-Configuration Tracking for Machine-Certified Correctness of Concurrent Data Structures (Abstract)
Prasad Jayanti, Siddhartha Jayanti, Ugur Yavuz, Lizzie Hernandez
ACM Workshop on Highlights of Parallel Computing [HOPC @ SPAA '24]
PDF
A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
Prasad Jayanti, Siddhartha Jayanti, Ugur Y. Yavuz, Lizzie Hernandez
51st ACM Symposium on Principles of Programming Languages [POPL '24]
PDF Talk Code
Preprints
Mechanized Metatheory of Forward Reasoning for End-to-End Linearizability Proofs
Zachary Kent, Ugur Y. Yavuz, Siddhartha Jayanti, Stephanie Balzer, Guy Blelloch
arXiv preprint, September 2025
arXiv
Theses
A Machine-Verified Proof of Linearizability for a Queue Algorithm
Ugur Y. Yavuz
Dartmouth College, Master's thesis, 2022
PDF Talk
Producing Easy-to-Verify Proofs of Linearizability
Ugur Y. Yavuz
Dartmouth College, Honors thesis, 2021
Awarded High Honors
PDF
Verifying Differential Privacy in TLA+ via Self-Products
TLA+ Community Event at ETAPS 2026, Turin, Italy. April 12, 2026.
Slides Code
Formal Machine-Verification of MemSnap
SPAA 2025, Portland, OR, USA. July 31, 2025.
PDF
A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability
POPL 2024, London, UK. January 17, 2024.
NJ Programming Languages and Systems Seminar (NJPLS), Princeton, NJ, USA. November 10, 2023.
Talk PDF
04/2026
My submission on soundness bugs in TLAPS was accepted to UNSOUND 2026 at ECOOP in Brussels!
04/2026
Presented at the TLA+ Community Event at ETAPS 2026 on verifying differential privacy.
Turin, IT 🇮🇹
03/2026
Serving on the Artifact Evaluation Committee for PLDI 2026.
02/2026
Serving as an external reviewer for LICS 2026.
10/2025
Gave an informal TLA tutorial for the POPV group.
Boston, MA 🇺🇸
08/2025
Awarded the Distinguished Paper Award for our SPAA 2025 paper! 🏅🎉
Portland, OR 🇺🇸
07/2025
Presenting our SPAA 2025 paper on the verification of an adaptive snapshot algorithm.
Portland, OR 🇺🇸
06/2025
Attending OPLSS 2025 (and helping with AV) at the University of Oregon!
Eugene, OR 🇺🇸
03/2025
Serving on the Artifact Evaluation Committee for PLDI 2025.
08/2024
Completed a Student Researcher engagement at Google.
Cambridge, MA 🇺🇸
06/2024
Helping organize and attending OPLSS 2024 at BU! 🎓
Boston, MA 🇺🇸
01/2024
Presented our POPL 2024 paper on meta-configuration tracking.
London, UK 🇬🇧
11/2023
Gave a talk at NJPLS 2023 on a preliminary version of our POPL work.
Princeton, NJ 🇺🇸
10/2023
Spoke at BU's POPV seminar series on our upcoming POPL 2024 paper.
Boston, MA 🇺🇸
09/2022
Joined the POPV group at Boston University as a Ph.D. student!
Boston, MA 🇺🇸
08/2022
Finished a remote internship at Microsoft, working on bug-patch metadata generation via InferSharp.
05/2022
Defended my master's thesis at Dartmouth College! 🌲🎉
Hanover, NH 🇺🇸