Paper-Conference

Fixed Parameter Tractable Linearizability Monitoring
We study the linearizability monitoring problem, which asks whether a given history of a concurrent implementation of a data structure …
Cite DOI Video ArXiv Media Coverage Publication page
State Space Estimation for DPOR-based Model Checkers
We study the estimation problem for concurrent programs: given a bounded program P, estimate the number of Mazurkiewicz …
A. R. Balasubramanian, Mohammad Hossein Khoshechin Jorshari, Rupak Majumdar, Umang Mathur, Minjian Zhang
Cite DOI Video ArXiv Publication page
Anvil: A General-Purpose Timing-Safe Hardware Description Language
Expressing hardware designs using hardware description languages (HDLs) routinely involves using stateless signals whose values change …
Jason Zhijingcheng Yu, Aditya Ranjan Jha, Umang Mathur, Trevor E. Carlson, Prateek Saxena
PDF Cite DOI Publication page
Counting and Sampling Traces in Regular Languages
In this work, we study the fundamental problems of counting and sampling traces that a regular language touches. Formally, one fixes …
Alexis De Colnet, Kuldeep S. Meel, Umang Mathur, Random Author Order
Cite DOI ArXiv Video Publication page
The Complexity of Testing Message-Passing Concurrency
A key computational question underpinning the automated testing and verification of concurrent programs is the consistency question — …
Zheng Shi, Lasse Møldrup, Umang Mathur, Andreas Pavlogiannis
Cite DOI ArXiv Video Publication page
Efficient Decrease-And-Conquer Linearizability Monitoring
Linearizability has become the de facto correctness specification for implementations of concurrent data structures. While formally …
PDF
Efficient Timestamping for Sampling-Based Race Detection
Dynamic race detection based on the happens before (HB) partial order has now become the de facto approach to quickly identify data …
Minjian Zhang, Daniel Lim, Mosaad Al Thokair, Umang Mathur, Mahesh Viswanathan
PDF
Program Skeletons for Automated Program Translation
Translating software between programming languages is a challenging task, for which automated techniques have been elusive and hard to …
Bo Wang, Tianyu Li, Ruishi Li, Umang Mathur, Prateek Saxena
PDF
Selectively Uniform Concurrency Testing
Buggy behaviors in concurrent programs are notoriously elusive, as they may manifest only in few of exponentially many possible thread …
Huan Zhao, Dylan Wolff, Umang Mathur, Abhik Roychoudhury
PDF
The Decision Problem for Regular First-Order Theories
The Entscheidungsproblem, or the classical decision problem, asks whether a given formula of first-order logic is satisfiable. In this …
Umang Mathur, David Mestel, Mahesh Viswanathan
PDF Cite DOI