Barış Bayazıt

• Verified Stack Switching in CompCert In progress
  [poster]
  Effect handlers and stack switching across every CompCert IR, mechanized in Rocq. With Ningning Xie and Oghenevwogaga Ebresafe.
• VerifyThisBench: Joint Evaluation of Code, Specifications, and Proof NeurIPS'26
  [arXiv|code]
  Xun Deng, Barış Bayazıt, Si Cheng Zhong, Andreas Veneris, Fan Long, Xujie Si
• A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants LMPL 2025
  [paper|doi]
  Barış Bayazıt, Yao Li, Xujie Si
• RESpecBench: How Reliable Is LLM-as-a-Judge? Rigorous Evaluation of Specification Generation with Automated Verification Preprint
  Barış Bayazıt, Xujie Si
• Linear Stages In progress
  A staged, linearly typed calculus with mutable references, mechanized in Rocq. With Ningning Xie and Maite Kramarz.

Talks

• A Case Study on the Effectiveness of LLMs in Verification with Proof Assistants — LMPL, Singapore Oct 2025
• RESpecBench — POPL Student Research Competition, Rennes Jan 2026
• RESpecBench — ARIA, Toronto Nov 2025

Awards

• CRA Outstanding Undergraduate Researcher Award, Honourable Mention 2026
• 2nd place, POPL Student Research Competition 2026
• 1st place, CS Undergraduate Research Showcase, University of Toronto Twice: 2025, 2026
• Department of Computer Science Research Award, University of Toronto 2025, 2026
• ACM SIGPLAN PAC 2025

Service

• Student volunteer, POPL 2026
• Orientation leader, Victoria College, University of Toronto 2026
• Web engineering lead, Computer Science Student Union, University of Toronto 2024–2025