Publications

---

Automatic Verification of Parameterized Data Structures
J. V. Deshmukh, E. A. Emerson, P.Gupta. TACAS 2006.
Reduces verification of parameterized data structures to the emptiness of
tree automata. Can verify properties like acyclicity for a reasonable set
of methods operating on lists, trees, and general graphs.
pdf slides bib

---

Automatic Generation of Local Repairs for Boolean Programs
R.Samanta, J. V. Deshmukh, E. A. Emerson. FMCAD 2008.
For Boolean Programs specified by pre/post-condition semantics, uses local
annotations generated by pre/post-condition propagation to generate repairs.
Improves on existing complexity results by an intelligent repair extraction.
Slides due to R. Samanta
pdf slides bib

---

Symbolic Deadlock Analysis in Concurrent Libraries and their Clients
J. V. Deshmukh, E. A. Emerson, S. Sankaranarayanan. ASE 2009.
Recipient of the ACM Distinguished Paper Award
Derives interface contracts over concurrent invocations of library methods to
ensure deadlock-freedom. Symbolcally explores the exponential number of alias
patterns across method arguments, using a SMT solver to derive contracts in
terms of these patterns.
pdf slides bib

---

Verification of Recursive Methods on Tree-like Data Structures
J. V. Deshmukh, E. A. Emerson, FMCAD 2009.
Identifies syntactic fragment and associated sufficient conditions such that
recursive methods therein can be algorithmically verified. Methods and pre/post-
conditions encoded as tree automata; correctness reduced to language emptiness.
pdf slides bib

---

Logical Concurrency Control From Sequential Proofs
J. V. Deshmukh, G. Ramalingam, V. P. Ranganath, and K. Vaswani.
Microsoft Research Tech Report link
Derives concurrency control for a sequential library to make it thread-safe, given
proof of sequential correctness of the library. Thread safety defined as: a) absence
of assertion failures in concurrent context, or b) linearizability of library.
pdf (Submitted)

---