Research Interests:

Software Verification, Programming Languages, Formal Methods, and Security (all with an emphasis on concurrency-related issues)

Selected Papers:

with Berk Cirisci, Constantin Enea, Suha Orhun Mutluergi: Root Causing Linearizability Violations. in CAV 2020 [PDF].

with
Anthony Vandikas: Reductions for Safety Verification. in POP 2020 [PDF, EXT].

with Anthony Vandikas: Automated Hypersafety Verification. in CAV 2019 [PDF, EXT].

with Victor Nicolet: Modular Divide and Conquer Parallelism for Nested Loops. in PLDI 2019 [PDF, EXT].

with Zachary Kincaid, Strategy Synthesis for Linear Arithmetic Games. in POPL 2018 [PDF].

with
Victor Nicolet: Automated Synthesis of Divide and Conquer Parallelism for Loops. in PLDI 2017 [PDF].

with
Zachary Kincaid, Andreas Podelski: Proving Liveness of Parameterized Programs. in LICS 2016 [PDF].

with Zachary Kincaid, Linear Arithmetic Satisfiability Via Strategy Improvement. in IJCAI 2016 [PDF].

with
Constantin Enea, On Atomicity in Presence of Non-atomic Writes. in TACAS 2016 [PDF][EXT].

with
Zachary Kincaid, Compositional Recurrence Analysis. in FMCAD 2015 [PDF].

with Zachary Kincaid, Andreas Podelski: Proof Spaces for unbounded Parallelism. in POPL 2015 [PDF].

with
Swarat Chaudhuri, Zachary Kincaid : Consistency Analysis of Decision Making Programs. in POPL 2014 [PDF].

with
Zachary Kincaid, Andreas Podelski: Proofs That Count. in POPL 2014 [PDF].

with
Niloofar Razavi, Sheila McIlraith: Predicting Atomicity Violations in Concurrent Programs via Planning. in STTT 2014 [PDF] .

with
Zachary Kincaid: Duet: Static Analysis for Unbounded Parallelism. in CAV 2013 [PDF].

with Andreas Holzer,
Niloofar Razavi, Helmut Veith: Con2colic Testing. in FSE 2013 [PDF].

with
Zachary Kincaid, Andreas Podelski: Inductive Data Flow Graphs. in POPL 2013 [PDF].

with P. Madhusudan, Niloofar Razavi, Francesco Sorrentino: Predicting Null-Pointer Dereferences in Concurrent Programs. in FSE 2012 [PDF].

with Zachary Kincaid: Verification of Parameterized Concurrent Programs By Modular Reasoning about Data and Control. in POPL 2012 [PDF].

with Andreas Holzer, Niloofar Razavi: Bounded-Interference Sequentialization for Testing Concurrent Programs. in ISOLA 2012 (invited paper) [PDF].

with
Sheila McIlraith, Niloofar Razavi: Predicting Atomicity Violations in Concurrent Programs via Planning. in VVPS 2011.

with P. Madhusudan, Francesco Sorrentino: PENELOPE: Weaving Threads To Expose Atomicity Violations. in FSE 2010 [PDF].

with Zachary Kincaid: Compositional Bitvector Analysis for Concurrent Programs With Nested Locks. in SAS 2010 [PDF].

with Y. Chen, , E. M. Clarke, M. Tsai, Y. Tsan, B. Wang: Automated Assume-Guarantee Reasoning Through Implicit Learning. in CAV 2010 [PDF] .

with Y. Chen, E. M. Clarke, M. Tsai, Y. Tsan, B. Wang, Lei Zhu: Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning. in ISOLA 2010 (invited paper) [PDF] .

with P. Madhusudan, Francesco Sorrentino: Meta Analysis of Concurrent Program Runs With Nested Locking For Atomicity Violations. in CAV 2009 [PDF] .

with P. Madhusudan: The Complexity of Predicting Atomicity Violations. in TACAS 2009 [PDF] .

with Y. Chen, E. M. Clarke, Y. Tsan, B. Wang: Learning Minimal Separating DFAs for Compositional Verification. in TACAS 2009 [PDF] .

with
P. Madhusudan: Monitoring Atomicity in Concurrent Programs. in CAV 2008 [PDF] .

with Y. Chen,
E. M. Clarke, Y. Tsan, B. Wang: Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages. in TACAS 2008 [PDF] .

with José Meseguer: Partial Order Reduction for the Semantics of Programming Languages. in Electronic Notes in Theoretical Computer Science (ENTCS) 2007 [PDF] .

with
P. Madhusudan: Causal Dataflow Analysis for Concurrent Programs. in TACAS 2007 [PDF] Extended version as technical Report UIUCDCS-R-2007-2806, Computer Science Department, University of Illinois at Urbana-Champaign, 2007 [PDF] .

with
José Meseguer: State Space Reduction of Rewrite Theories Using Invisible Transitions. in AMAST 2006 [PDF] .

with P. Madhusudan: Causal Atomicity. in CAV 2006 [PDF] .

with José Meseguer: Making Partial Order Reduction Language Independent. in WRLA 2006 [PDF] .

with Feng Chen, José Meseguer, Grigore Rosu: JavaFAN: A Rewriting Logic Approach to Formal Analysis of Multithreaded Java Programs. Technical Report UIUCDCS-R-2005-1523, Computer Science Department, University of Illinois at Urbana-Champaign, 2005. [PDF]

with Feng Chen, José Meseguer, Grigore Rosu: Formal Analysis of Java Programs in JavaFAN. in CAV 2004 [PDF] .

with José Meseguer, Grigore Rosu: Formal JVM Code Analysis in JavaFAN. in AMAST 2004 [PDF] .