Paper-Conference

Decidable Verification of Uninterpreted Programs
We study the problem of completely automatically verifying uninterpreted programs—programs that work over arbitrary data models …
Umang Mathur, P. Madhusudan, Mahesh Viswanathan
Cite DOI ArXiv Conference Talk Talk at OWLS seminar Slides Publication page
Controller Synthesis Made Real: Reach-avoid Specifications and Linear Dynamics
We address the problem of synthesizing provably correct controllers for linear systems with reach-avoid specifications. Our solution …
Chuchu Fan, Umang Mathur, Sayan Mitra, Mahesh Viswanathan
PDF Cite DOI Tool Publication page
Data Race Detection on Compressed Traces
We consider the problem of detecting data races in program traces that have been compressed using straight line programs (SLP), which …
Dileep Kini, Umang Mathur, Mahesh Viswanathan
Cite DOI ArXiv Tool Publication page
Decidable Fragment of Second Order Logic With Applications to Program Synthesis
We propose a fragment of many-sorted second order logic called EQSMT and show that checking satisfiability of sentences in this …
P. Madhusudan, Umang Mathur, Shambwaditya Saha, Mahesh Viswanathan
PDF Cite DOI ArXiv Publication page
What Happens-After the First Race? Enhancing the Predictive Power of Happens-Before Based Dynamic Race Detection
Dynamic race detection is the problem of determining if an observed program execution reveals the presence of a data race in a program. …
Umang Mathur, Dileep Kini, Mahesh Viswanathan
Cite DOI ArXiv Tool Video Publication page
Dynamic Race Prediction in Linear Time
Writing reliable concurrent software remains a huge challenge for today’s programmers. Programmers rarely reason about their code …
Dileep Kini, Umang Mathur, Mahesh Viswanathan
Cite DOI ArXiv Tool Video Publication page
Exact Quantitative Probabilistic Model Checking Through Rational Search
Model checking of systems formalized using probabilistic models such as discrete time Markov chains (DTMCs) and Markov decision …
Matthew S. Bauer, Umang Mathur, Rohit Chadha, A. Prasad Sistla, Mahesh Viswanathan
PDF Cite DOI Publication page
Look for the Proof to Find the Program: Decorated-Component-Based Program Synthesis
We introduce a technique for component-based program synthesis that relies on searching for a target program and its proof of …
Adria Gascon, Ashish Tiwari, Brent Carmer, Umang Mathur
PDF Cite DOI Tool Video Publication page
Computing Information Flow Using Symbolic Model-Checking
Several measures have been proposed in literature for quantifying the information leaked by the public outputs of a program with secret …
Rohit Chadha, Umang Mathur, Stefan Schwoon
Cite DOI Tool Publication page
Weak Singular Hybrid Automata
The framework of Hybrid automata—introduced by Alur, Courcourbetis, Henzinger, and Ho—provides a formal modeling and …
Shankaranarayanan Krishna, Umang Mathur, Ashutosh Trivedi
Cite DOI ArXiv Publication page