Paper-Conference

Efficient Decrease-And-Conquer Linearizability Monitoring
Linearizability has become the de facto correctness specification for implementations of concurrent data structures. While formally …
Zheng Han Lee, Umang Mathur
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
Greybox Fuzzing for Concurrency Testing
Uncovering bugs in concurrent programs is a challenging problem owing to the exponentially large search space of thread interleavings. …
Dylan Wolff, Zheng Shi, Gregory J. Duck, Umang Mathur, Abhik Roychoudhury
PDF Cite DOI
Predictive Monitoring with Strong Trace Prefixes
A faster FPRAS for #NFA
Given a non-deterministic finite automaton (NFA) A with m states, and a natural number n (presented in unary), the #NFA problem asks to …
Kuldeep S. Meel, Sourav Chakraborty, Umang Mathur
PDF Cite DOI
Optimistic Prediction of Synchronization-Reversal Data Races
Dynamic data race detection has emerged as a key technique for ensuring reliability of concurrent software in practice. However, …
Zheng Shi, Umang Mathur, Andreas Pavlogiannis
PDF Cite DOI
Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separation Logic
Array-based encodings of tree structures are often preferable to linked or abstract data type-based representations for efficiency …
Qiyuan Zhao, George Pîrlea, Zhendong Ang, Umang Mathur, Ilya Sergey
PDF Cite Code DOI