26 citations · 106 across the 19 of their papers we have counts for
24 papers
Dynamic Race Detection With O(1) Samples
Mosaad Al Thokair, Minjian Zhang, Umang Mathur +1
Happens before-based dynamic analysis is the go-to technique for detecting data races in large scale software projects due to the absence of false positive reports. However, such a…
Efficient Timestamping for Sampling-based Race Detection
Minjian Zhang, Daniel Wee Soong Lim, Mosaad Al Thokair +2
Dynamic race detection based on the happens before (HB) partial order has now become the de facto approach to quickly identify data races in multi-threaded software. Most practical…
The Decision Problem for Regular First-Order Theories
Umang Mathur, David Mestel, Mahesh Viswanathan
The \emph{Entscheidungsproblem}, or the classical decision problem, asks whether a given formula of first-order logic is satisfiable. In this work, we consider an extension of this…
Optimistic Prediction of Synchronization-Reversal Data Races
Zheng Shi, Umang Mathur, Andreas Pavlogiannis
Dynamic data race detection has emerged as a key technique for ensuring reliability of concurrent software in practice. However, dynamic approaches can often miss data races owing…
How Hard is Weak-Memory Testing?
Soham Chakraborty, Shankaranarayanan Krishna, Umang Mathur +1
Weak-memory models are standard formal specifications of concurrency across hardware, programming languages, and distributed systems. A fundamental computational problem is consist…
Predictive Monitoring against Pattern Regular Languages
Zhendong Ang, Umang Mathur
In this paper, we focus on the problem of dynamically analysing concurrent software against high-level temporal specifications. Existing techniques for runtime monitoring against s…
Optimal Reads-From Consistency Checking for C11-Style Memory Models
Hünkar Can Tunç, Parosh Aziz Abdulla, Soham Chakraborty +3
Over the years, several memory models have been proposed to capture the subtle concurrency semantics of C/C++.One of the most fundamental problems associated with a memory model M…
Sound Dynamic Deadlock Prediction in Linear Time
Hünkar Can Tunç, Umang Mathur, Andreas Pavlogiannis +1
Deadlocks are one of the most notorious concurrency bugs, and significant research has focused on detecting them efficiently. Dynamic predictive analyses work by observing concurre…
Coarser Equivalences for Causal Concurrency
Azadeh Farzan, Umang Mathur
Trace theory is a principled framework for defining equivalence relations for concurrent program runs based on a commutativity relation over the set of atomic steps taken by indivi…
A Tree Clock Data Structure for Causal Orderings in Concurrent Executions
Umang Mathur, Andreas Pavlogiannis, Hünkar Can Tunç +1
Dynamic techniques are a scalable and effective way to analyze concurrent programs. Instead of analyzing all behaviors of a program, these techniques detect errors by focusing on a…
Dynamic Data-Race Detection through the Fine-Grained Lens
Rucha Kulkarni, Umang Mathur, Andreas Pavlogiannis
Data races are among the most common bugs in concurrency. The standard approach to data-race detection is via dynamic analyses, which work over executions of concurrent programs, i…
Optimal Prediction of Synchronization-Preserving Races
Umang Mathur, Andreas Pavlogiannis, Mahesh Viswanathan
Concurrent programs are notoriously hard to write correctly, as scheduling nondeterminism introduces subtle errors that are both hard to detect and to reproduce. The most common co…
Scalable Statistical Root Cause Analysis on App Telemetry
Vijayaraghavan Murali, Edward Yao, Umang Mathur +1
Despite engineering workflows that aim to prevent buggy code from being deployed, bugs still make their way into the Facebook app. When symptoms of these bugs, such as user submitt…
The Complexity of Dynamic Data Race Prediction
Umang Mathur, Andreas Pavlogiannis, Mahesh Viswanathan
Writing concurrent programs is notoriously hard due to scheduling non-determinism. The most common concurrency bugs are data races, which are accesses to a shared resource that can…
Atomicity Checking in Linear Time using Vector Clocks
Umang Mathur, Mahesh Viswanathan
Multi-threaded programs are challenging to write. Developers often need to reason about a prohibitively large number of thread interleavings to reason about the behavior of softwar…
What's Decidable About Program Verification Modulo Axioms?
Umang Mathur, P. Madhusudan, Mahesh Viswanathan
We consider the decidability of the verification problem of programs \emph{modulo axioms} --- that is, verifying whether programs satisfy their assertions, when the functions and r…
Decidable Synthesis of Programs with Uninterpreted Functions
Paul Krogmeier, Umang Mathur, Adithya Murali +2
We identify a decidable synthesis problem for a class of programs of unbounded size with conditionals and iteration that work over infinite data domains. The programs in our class…
Deciding Memory Safety for Single-Pass Heap-Manipulating Programs
Umang Mathur, Adithya Murali, Paul Krogmeier +2
We investigate the decidability of automatic program verification for programs that manipulate heaps, and in particular, decision procedures for proving memory safety for them. We…
Decidable Verification of Uninterpreted Programs
Umang Mathur, P. Madhusudan, Mahesh Viswanathan
We study the problem of completely automatically verifying uninterpreted programs---programs that work over arbitrary data models that provide an interpretation for the constants,…
What Happens - After the First Race? Enhancing the Predictive Power of Happens - Before Based Dynamic Race Detection
Umang Mathur, Dileep Kini, Mahesh Viswanathan
Dynamic race detection is the problem of determining if an observed program execution reveals the presence of a data race in a program. The classical approach to solving this probl…
Data Race Detection on Compressed Traces
Dileep Kini, Umang Mathur, Mahesh Viswanathan
We consider the problem of detecting data races in program traces that have been compressed using straight line programs (SLP), which are special context-free grammars that generat…
A Decidable Fragment of Second Order Logic With Applications to Synthesis
P. Madhusudan, Umang Mathur, Shambwaditya Saha +1
We propose a fragment of many-sorted second order logic called EQSMT and show that checking satisfiability of sentences in this fragment is decidable. EQSMT formulae have an $\exis…
Dynamic Race Prediction in Linear Time
Dileep Kini, Umang Mathur, Mahesh Viswanathan
Writing reliable concurrent software remains a huge challenge for today's programmers. Programmers rarely reason about their code by explicitly considering different possible inter…
Weak Singular Hybrid Automata
Shankara Narayanan Krishna, Umang Mathur, Ashutosh Trivedi
The framework of Hybrid automata, introduced by Alur, Courcourbetis, Henzinger, and Ho, provides a formal modeling and analysis environment to analyze the interaction between the d…