Selected Papers:

• Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
  With Jialu Bao and Emanuele D’Osualdo
  in POPL 2025
  Paper

• Coarser Equivalences for Causal Concurrency
  With Umang Mathur
  in POPL 2024
  Paper Extended Version

• Commutativity Simplifies Proofs of Parametrized Programs
  With Dominik Klumpp and Andreas Podelski:
  in POPL 2024
  Paper

• Commutativity in Automated Verification
  in LICS 2023
  Paper

• Commutativity For Concurrent Program Termination Proofs
  With Danya Lette
  in CAV 2023
  Paper Extended Version

• Stratified Commutativity in Verification Algorithms for Concurrent Programs
  With Dominik Klumpp and Andreas Podelski:
  in POPL 2023
  Paper

• Proving Hypersafety Compositionally
  With Emanuele D’Osualdo, and Derek Dreyer:
  in OOPSLA 2022
  Paper Extended Version

• Sound Sequentialization for Concurrent Program Verification
  With Dominik Klumpp and Andreas Podelski:
  to appear in PLDI 2022
  Paper Appendix

• Recursion Synthesis with Unrealizability Witnesses
  With Victor Nicolet and Danya Lette:
  to appear in PLDI 2022
  Paper Extended Version

• Counterexample-Guided Partial Bounding for Recursive Function Synthesis
  With Victor Nicolet:
  in CAV 2021
  Paper Extended Version

• Phased Synthesis of Divide and Conquer Programs
  With Victor Nicolet:
  in PLDI 2021
  Full Paper

• TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs
  With Emanuele D’Osualdo, Julian Sutherland, and Philippa Gardner:
  in TOPLAS 2021
  Paper

• Root Causing Linearizability Violations
  With Berk Cirisci, Constantin Enea, Suha Orhun Mutluergi
  in CAV 2020
  Paper

• Reductions for Safety Verification
  With Anthony Vandikas:
  in POPL 2020
  Paper Extended Version

• Automated Hypersafety Verification
  With Anthony Vandikas:
  in CAV 2019
  Paper Extended Version

• Modular Divide and Conquer Parallelism for Nested Loops
  With Victor Nicolet:
  in PLDI 2019
  Paper Extended Version

• Strategy Synthesis for Linear Arithmetic Games
  With Zachary Kincaid:
  in POPL 2018
  Paper

• Automated Synthesis of Divide and Conquer Parallelism for Loops
  With Victor Nicolet:
  in PLDI 2017
  Paper Extended Version

• Proving Liveness of Parameterized Programs
  With Zachary Kincaid, Andreas Podelski:
  in LICS 2016
  Paper

• Linear Arithmetic Satisfiability Via Strategy Improvement
  With Zachary Kincaid:
  in IJCAI 2016
  Paper

• On Atomicity in Presence of Non-atomic Writes
  With Constantin Enea:
  in TACAS 2016
  Paper Extended Version

• Compositional Recurrence Analysis
  With Zachary Kincaid:
  in FMCAD 2015
  Paper

• Proof Spaces for unbounded Parallelism
  With Zachary Kincaid, Andreas Podelski:
  in POPL 2015
  Paper More on Predicate Automata

• Consistency Analysis of Decision Making Programs
  With Swarat Chaudhuri, Zachary Kincaid:
  in POPL 2014
  Paper

• Proofs That Count
  With Zachary Kincaid, Andreas Podelski:
  in POPL 2014
  Paper

• Predicting Atomicity Violations in Concurrent Programs via Planning
  With Niloofar Razavi, Sheila McIlraith:
  in STTT 2014
  Paper

• Duet: Static Analysis for Unbounded Parallelism
  With Zachary Kincaid:
  in CAV 2013
  Paper

• Con2colic Testing
  With Andreas Holzer, Niloofar Razavi, Helmut Veith:
  in FSE 2013
  Paper

• Inductive Data Flow Graphs
  With Zachary Kincaid, Andreas Podelski:
  in POPL 2013
  Paper

• Predicting Null-Pointer Dereferences in Concurrent Programs
  With P. Madhusudan, Niloofar Razavi, Francesco Sorrentino:
  in FSE 2012
  Paper

• Verification of Parameterized Concurrent Programs By Modular Reasoning about Data and Control
  With Zachary Kincaid:
  in POPL 2012
  Paper

• Bounded-Interference Sequentialization for Testing Concurrent Programs
  With Andreas Holzer, Niloofar Razavi:
  in ISOLA 2012 (invited paper)
  Paper

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

• Weaving Threads To Expose Atomicity Violations
  With P. Madhusudan, Francesco Sorrentino: PENELOPE:
  in FSE 2010
  Paper

• Compositional Bitvector Analysis for Concurrent Programs With Nested Locks
  With Zachary Kincaid:
  in SAS 2010
  Paper

• Automated Assume-Guarantee Reasoning Through Implicit Learning
  With Y. Chen, E. M. Clarke, M. Tsai, Y. Tsan, B. Wang:
  in CAV 2010
  Paper

• Comparing Learning Algorithms in Automated Assume-Guarantee Reasoning
  With Y. Chen, E. M. Clarke, M. Tsai, Y. Tsan, B. Wang, Lei Zhu
  in ISOLA 2010 (invited paper)
  Paper

• Meta Analysis of Concurrent Program Runs With Nested Locking For Atomicity Violations
  With P. Madhusudan, Francesco Sorrentino:
  in CAV 2009
  Paper

• The Complexity of Predicting Atomicity Violations
  With P. Madhusudan:
  in TACAS 2009
  Paper

• Learning Minimal Separating DFAs for Compositional Verification
  With Y. Chen, E. M. Clarke, Y. Tsan, B. Wang
  in TACAS 2009
  Paper

• Monitoring Atomicity in Concurrent Programs
  With P. Madhusudan:
  in CAV 2008
  Paper

• Extending Automated Compositional Verification to the Full Class of Omega-Regular Languages
  With Y. Chen, E. M. Clarke, Y. Tsan, B. Wang:
  in TACAS 2008
  Paper

• Partial Order Reduction for the Semantics of Programming Languages
  With José Meseguer:
  in Electronic Notes in Theoretical Computer Science (ENTCS) 2007
  Paper

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

• State Space Reduction of Rewrite Theories Using Invisible Transitions
  With José Meseguer:
  in AMAST 2006
  Paper

• Causal Atomicity
  With P. Madhusudan:
  in CAV 2006
  Paper

• Making Partial Order Reduction Language Independent
  With José Meseguer:
  in WRLA 2006
  Paper

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

• Formal Analysis of Java Programs in JavaFAN
  With Feng Chen, José Meseguer, Grigore Rosu:
  in CAV 2004
  Paper

• Formal JVM Code Analysis in JavaFAN
  With José Meseguer, Grigore Rosu:
  in AMAST 2004
  Paper