Omkar Tuppe

Home News Research Publications Education Activities Contact

📰 News

Apr 2025: Our paper got accepted at CAV 2025.
Mar 2025: Gave a talk at RISC 2025, CSE IITB
Feb 2025: Presented a poster at ACM ARCS 2025, Coimbatore.
Oct 2024: Presented our paper at ATVA 2024, Kyoto.
Aug 2024: Gave an invited talk at TCS Research Expo 2024-Pune.
July 2024: Our paper got accepted at ATVA 2024.
Dec 2023: Gave research talk at Workshop on Research Highlights in Programming Languages (RHPL 2023) - Hyderabad.
Oct 2023: Our paper got accepted at POPL 2024.
April 2023: Started Summer Internship at Uppsala University.
April 2023: Presented our paper at TACAS 2023, Paris.
Mar 2023: Gave talk at IITB CSE Research Symposium 2023 - Mumbai.
Dec 2022: Our paper got accepted at TACAS 2023.
May 2022: Started a summer internship at Uppsala University.
April 2021:Completed my coursework and have started research work under the supervision of Prof. Krishna S and Prof. Ashutosh Gupta.
July 2019: Started PhD @ CSE, IIT Bombay.

🔬 Research & Development

🧠 Overview

My research focuses on building efficient verification algorithms and analysis tools for concurrent and weakly-consistent systems. I design scalable algorithms grounded in formal semantics and implement them as LLVM-based tools targeting real-world software. These tools have demonstrated significant performance improvements over existing solutions and are validated on various benchmarks.

🚀 🧑‍💻 📑 Projects & Tools

GPUMC: Stateless Model Checker for GPU Memory Models

Problem: Existing GPU verification tools miss concurrency bugs under relaxed models.
Approach: Developed an LLVM-based verifier targeting NVPTX-style GPU programs under the SCR11 memory model.
Impact: Detected real bugs missed by state-of-the-art tools; achieved 100× speedup, 10× lower memory usage.
Extra: Integrated heterogeneous race detection and automatic repair of GPU kernels.
Tool Link

TranSER: DPOR for Serializable Transactional Programs

Problem: Transactional program verification is slow under interleaving explosion.
Approach: Designed a Dynamic Partial Order Reduction (DPOR) algorithm tailored for transactional programs.
Impact: Validated on OLTP benchmarks, outperforming Transactional-JPF by 100× in bug-finding throughput.
Tool Link

DynamicDyckReachability: On-the-Fly Static Analysis

Problem: Standard Dyck-reachability methods don’t scale for large codebases or dynamic contexts.
Approach: Engineered a dynamic Dyck-reachability algorithm for alias and data-dependence analysis.
Impact: Achieved 1000× speedup on DeCapo and SPECjvm2008 benchmarks for data-dependence and alias analysis.
Tool Link

ConsChecker: Model Checking for Causal Consistency

Problem: Ensuring causal consistency in concurrent code is underexplored in tooling.
Approach: Built an LLVM-based stateless model checker to detect causal consistency violations.
Impact: Evaluated on SV-COMP benchmarks with strong performance and correctness results.
Tool Link

TranChecker: Verifying Weakly Isolated Transactional Systems

Problem: Transactional systems often operate under weak isolation (e.g., Read Committed, Read Atomic, Causal Convergence). There is a need for a tool that can handle all these memory models.
Approach: Designed verification algorithms for weak isolation; implemented LLVM-IR interpreter in C++ to explore interleavings.
Impact: Systematically verified transactional programs under weak consistency.

SimpleDPOR: Simple DPOR based model checker for Sequential Consistency (SC)

Problem:Existing DPOR model checkers for SC are non-intuitive and complex. There is a need for a simple and intuitive model checker for SC.
Approach: Built a sleep-set-based stateless model checker for SC.
Impact: Evaluated on 9000+ litmus tests and SV-COMP benchmarks.

ARMv8-A BMC: Concurrency Verification for ARM Assembly

Problem: Detecting concurrency bugs at the ISA level—ARMv8.
Approach: Bounded model checker using symbolic execution and context bounding for ARMv8 assembly.
Impact: Systematically verified ARMv8-A programs.

📚 Publications

GPUMC: A Stateless Model Checker for GPU Weak Memory Concurrency

with Soham Chakraborty, S Krishna, Andreas Pavlogiannis

CAV 2025

Dynamic Partial Order Reduction for Transactional Programs on Serializable Platforms

with Parosh Aziz Abdulla, Ashutosh Gupta, Shankara Narayanan Krishna

ATVA 2024

On-The-Fly Static Analysis via Dynamic Bidirected Dyck Reachability

with Krishna S , Aniket Lal, Andreas Pavlogiannis

POPL 2024

Optimal Stateless Model Checking for Causal Consistency

with Parosh Abdulla, Mohamed Faouzi Atig, Krishna S, Ashutosh Gupta

TACAS 2023

🎓 Education

2019– PhD, Computer Science & Engineering IIT Bombay

Advisors: Prof. Krishna S, Prof. Ashutosh Gupta

2014–18 B.E., WIT Solapur Solapur University

Research Internships

April–June 2023 Uppsala University, Sweden

Supervisors: Prof. Parosh Abdulla, Prof. Mohamed Faouzi Atig
Topic: Stateless Model Checking for SC

May–July 2022 Uppsala University, Sweden

Supervisors: Prof. Parosh Abdulla, Prof. Mohamed Faouzi Atig
Topic: Algorithmic Program Verification

🎯 Activities

Teaching Assistantships

Data Structures (Autumn 2023)
Logics for CS (Spring 2020, Autumn 2020)
Automata Theory M (Autumn 2021)
Analysis of Concurrent Programs (Spring 2021, 2022, 2023)
Automated Reasoning (Autumn 2022)

Volunteering

CAV AEC 2023, 2025
Student Volunteer, ETAPS 2023
Web-Nominee, IRSCP 2020-21
Department Coordinator, IRSCP 2020-21
Student Member, CSE Task Force for Enabling Online Learning (during Covid-Pandemic)

Presented Research

ARCS 2025
TCS Research Expo 2024
ATVA 2024
RHPL 2023
TACAS 2023

Contact Me

Email: omkarvtuppe@cse.iitb.ac.in

LinkedIn: My LinkedIn Profile

Formal Verification | Program Analysis | Relaxed Memory Models