Paper-Conference

A Tree Clock Data Structure for Causal Orderings in Concurrent Executions
Dynamic techniques are a scalable and effective way to analyze concurrent programs. Instead of analyzing all behaviors of a program, …
Umang Mathur, Andreas Pavlogiannis, Hünkar Can Tunç, Mahesh Viswanathan
Cite DOI ArXiv Video Media Coverage Publication page
Checking LTL[F,G,X] on Compressed Traces in Polynomial Time
The problem of checking if a program execution meets a formal specification arises in many software engineering tasks including runtime …
Minjian Zhang, Umang Mathur, Mahesh Viswanathan
PDF Cite DOI Publication page
Dynamic Data-Race Detection through the Fine-Grained Lens
Data races are among the most common bugs in concurrency. The standard approach to data-race detection is via dynamic analyses, which …
Rucha Kulkarni, Umang Mathur, Andreas Pavlogiannis
Cite DOI ArXiv Publication page
Optimal Prediction of Synchronization-Preserving Races
Concurrent programs are notoriously hard to write correctly, as scheduling nondeterminism introduces subtle errors that are both hard …
Umang Mathur, Andreas Pavlogiannis, Mahesh Viswanathan
Cite DOI ArXiv Video Publication page
Scalable Statistical Root Cause Analysis on App Telemetry
Despite engineering workflows that aim to prevent buggy code from being deployed, bugs still make their way into the Facebook app. When …
Vijayaraghavan Murali, Edward Yao, Umang Mathur, Satish Chandra
Cite DOI ArXiv Blog Video Publication page
Atomicity Checking in Linear Time using Vector Clocks
Multi-threaded programs are challenging to write. Developers often need to reason about a prohibitively large number of thread …
Umang Mathur, Mahesh Viswanathan
Cite DOI ArXiv Video Tool Publication page
Decidable Synthesis of Programs with Uninterpreted Functions
We identify a decidable synthesis problem for a class of programs of unbounded size with conditionals and iteration that work over …
Paul Krogmeier, Umang Mathur, Adithya Murali, P. Madhusudan, Mahesh Viswanathan
Cite DOI ArXiv Video Publication page
Deciding Memory Safety for Single-Pass Heap-Manipulating Programs
We investigate the decidability of automatic program verification for programs that manipulate heaps, and in particular, decision …
Umang Mathur, Adithya Murali, Paul Krogmeier, P. Madhusudan, Mahesh Viswanathan
Cite DOI ArXiv Video Tool Publication page
The Complexity of Data Race Prediction
Writing concurrent programs is notoriously hard due to scheduling non-determinism. The most common concurrency bugs are data races, …
Umang Mathur, Andreas Pavlogiannis, Mahesh Viswanathan
Cite DOI ArXiv Video Publication page
What's Decidable About Program Verification Modulo Axioms?
We consider the decidability of the verification problem of programs mph{modulo axioms} — that is, verifying whether programs …
Umang Mathur, P. Madhusudan, Mahesh Viswanathan
Cite DOI ArXiv Publication page