1 citations · 1 across the 6 of their papers we have counts for
8 papers
Scenario Proofs for Verification of Distributed Protocols
Zhendong Ang, George Pîrlea, Umang Mathur
Formal verification of distributed protocols is still dominated by inductive-invariant proofs, whose central challenge is discovering strengthening assertions that rule out unreach…
SafePar: Monitoring Asynchrony in Microservices
Karuna Grewal, P. Brighten Godfrey, Justin Hsu +1
Modern cloud applications are built from loosely-coupled microservices that coordinate through well-defined APIs to service user requests. A single API request often triggers multi…
Instrumentation Optimization for Practical Dynamic Race Detection
Alexey Paznikov, Andrey Kogutenko, Yaroslav Osipov +2
Dynamic data race detectors are successful at flagging concurrency bugs, but their high runtime overhead limits adoption. This overhead stems primarily from pervasive instrumentati…
Fixed Parameter Tractable Linearizability Monitoring
Lee Zheng Han, Umang Mathur
We study the linearizability monitoring problem, which asks whether a given concurrent history of a data structure is equivalent to some sequential execution of the same data struc…
The Complexity of Testing Message-Passing Concurrency
Zheng Shi, Lasse Møldrup, Umang Mathur +1
A key computational question underpinning the automated testing and verification of concurrent programs is the consistency question - given a partial execution history, can it be c…
Enhanced Data Race Prediction Through Modular Reasoning
Zhendong Ang, Azadeh Farzan, Umang Mathur
There are two orthogonal methodologies for efficient prediction of data races from concurrent program runs: commutativity and prefix reasoning. There are several instances of each…
Efficient Decrease-and-Conquer Linearizability Monitoring
Lee Zheng Han, Umang Mathur
Linearizability has become the de facto correctness specification for implementations of concurrent data structures. While formally verifying such implementations remains challengi…
Predictive Monitoring with Strong Trace Prefixes
Zhendong Ang, Umang Mathur
Runtime predictive analyses enhance coverage of traditional dynamic analyses based bug detection techniques by identifying a space of feasible reorderings of the observed execution…