Home
Selected Publications
2022
2021
2020
2019
2018
2017
2016
2015
2014
2013
2012
2011
2010
2009
 2008
 2007
 2006
 2005
 2004
 pre-2004
2022
    1.        1. Specification-Guided Component-Based Synthesis from Effectful Libraries
    2.                ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), December 2022
    3.                (with A. Mishra) (abstract)
    4.        2. Defending Observation Attacks in Deep Reinforcement Learning via Detection and Denoising
    5.                European Conference on Machine Learning and Principles and Practice of Knowledge Discovery in Databases (ECML/PKDD), October 2022
    6.                (with Z. Xiong, J. Eappen, H. Zhu) (abstract)
    7.        3. DistSPECTRL: Distributing Specifications in Multi-Agent Reinforcement Learning Systems
    8.                European Conference on Machine Learning and Principles and Practice of Knowledge Discovery in Databases (ECML/PKDD), October 2022
    9.                (with J. Eappen) (abstract)
    10.        4. Model-free Neural Lyapunov Control for Safe Robot Navigation
    11.                International Conference on Intelligent Robots and Systems
    12.                (with Z. Xiong, J. Eappen, A. Querishi) (abstract)
2021
    1.        1. Data-Driven Abductive Inference of Library Specifications
    2.                ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), October 2021
    3.                (with Z. Zhou, R. Dickerson, and B. Delaware) (abstract)
    4.        2. Repairing serializability bugs in distributed database programs via automated schema refactoring
    5.                ACM Conference on Programming Language Design and Implementation (PLDI), June 2021
    6.                (with K. Rahmani, K.Nagar, and B. Delaware) (abstract)
2020
    1.        1. Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
    2.                Computer-Aided Verification (CAV), July 2020
    3.                (with K.Nagar) (abstract)
    4.        2. ART : Abstraction Refinement-Guided Training for Provably Correct Neural Networks
    5.                Formal Methods in Computer-Aided Design (FMCAD), September 2020
    6.                (with H. Zhu, R. Samanta) (abstract)
2019
    1.        1. Mergeable Replicated Data Types
    2.                ACM Conference on Object-Oriented Programming, Languages, Systems, and Applications (OOPSLA), November 2019
    3.                (with G. Kaki, S. Priya, K.C. Sivaramakrishnan) (abstract)
    4.        2. CLOTHO: Directed Test Generation for Weakly-Consistent Database Systems
    5.                ACM Conference on Object-Oriented Programming, Languages, Systems, and Applications (OOPSLA), November 2019
    6.                (with K. Rahmani, B. Delaware) (abstract)
    7.        3. An Inductive Synthesis Framework for Verifiable Reinforcement Learning
    8.                ACM Conference on Programming Language Design and Implementation (PLDI), June 2019
    9.                (with H. Zhu, Z. Xiong, S. Magill) (Distinguished Paper) (abstract)
    10.        4. Automated Parameterized Verification of CRDTs
    11.                Computer-Aided Verification (CAV), July 2019
    12.                (with K. Nagar) (abstract)
2018
    1.        1. Safe Replication Through Bounded Concurrency Verification
    2.                ACM Conference on Object-Oriented Programming, Languages, Systems, and Applications (OOPSLA), November 2018
    3.                (with G. Kaki, K. Earnky, K.C. Sivaramakrishnan) (abstract)
    4.        2. Alone Together: Compositional Reasoning and Inference for Weak Isolation
    5.                ACM Symposium on Principles of Programming Languages (POPL), January 2018
    6.                (with G. Kaki, K. Nagar, M. Najafzadeh) (abstract)
      1.        3. A Data-Driven CHC Solver
      2.                ACM Conference on Programming Language Design and Implementation (PLDI), June 2018
      3.                (with H. Zhu, S. Magill) (Distinguished Paper) (abstract)
        1.        4. Automated Detection of Serializability Violations Under Weak Consistency
        2.                29th International Conference on Concurrency Theory (CONCUR), September 2018
        3.                (with K. Nagar) (abstract)
2017
    1.        1. Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology
    2.                Interactive Theorem Proving (ITP), October 2017
    3.                (with Y. Zakowski1, D. Cachera, D. Demange, G. Petri, D. Pichardie, J. Vitek) (abstract)
2016
    1.        1. Automatically Learning Shape Specifications
    2.                ACM Conference on Programming Language Design and Implementation (PLDI), June 2016
    3.                (with H. Zhu and G. Petri). (abstract)
    4.        2. Representation without Taxation: A Uniform, Low-Overhead and High-Level Interface to Eventually Consistent Key-Value Stores
    5.                IEEE Data Engineering Bulletin, 39(1)2016
    6.                (with G. Kaki and K.C. Sivaramakrishnan). (abstract)
    7.        3. Verifying Custom Synchronisation Constructs Using Higher-Order Separation Logics
    8.                ACM Transactions on Programming Languages and Systems (TOPLAS), 38(2):4, 2016
    9.                (with M. Dodds, M.J. Parkinson, K. Svendsen, L. Birkedal). (abstract)
2015
    1.        1. Learning Refinement Types
    2.                ACM International Conference on Functional Programming (ICFP), September 2015
    3.                (with H. Zhu and A. Nori). (abstract)
    4.        2. Cooking the Books: Formalizing JMM Implemetation Recipes
    5.                European Conference on Object-Oriented Programming (ECOOP), July 2015
    6.                (with G. Petri and J. Vitek. (abstract)
    7.        3. Poling: SMT-Aided Linearizability Proofs
    8.                Computer Aided Verification (CAV), July 2015
    9.                (with H. Zhu and G. Petri). (abstract)
    10.        4. Declarative Programming over Eventually Consistent Data Stores
    11.                ACM Conference on Programming Language Design and Implementation (PLDI), June 2015
    12.                (with K.C. Sivaramakrishnan and G. Kaki). (abstract)
    13.        5. Synthesizing Racy Tests
    14.                ACM Conference on Programming Language Design and Implementation (PLDI), June 2015
    15.                (with M. Samak and M. Ramanathan). (abstract)
    16.        6. Dependent Array Type Inference from Tests
    17.                International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), January 2015
    18.                (with H. Zhu and A. Nori). (abstract)
2014
    1.        1. MultiMLton: A Multicore-aware Runtime for Standard ML
    2.                Journal of Functional Programming, 24(6)
    3.                (with K.C. Sivaramakrishnan and L. Ziarek). (abstract)
    4.        2. A Relational Framework for Higher-Order Shape Analysis
    5.                ACM International Conference on Functional Programming (ICFP), September 2014
    6.                (with G. Kaki). (abstract)
    7.        3. Atomicity Refinement for Verified Compilation
    8.                ACM Transactions on Programming Languages and Systems (TOPLAS), 36(2):6
    9.                Presented at PLDI, June 2014
    10.                (with V. Laporte, G. Petri, D. Pichardie, and J. Vitek). (abstract)
    11.        4. Rx-CML: A Prescription for Safely Relaxing Synchrony
    12.                Conference on Practical Aspects of Declarative Languages (PADL), January 2014
    13.                (with K.C. Sivaramakrishnan and L. Ziarek). (abstract)
2013
    1.        1. Flexible Access Control for Javascript
    2.                ACM Conference on Object-Oriented Programming, Systems, Languagess, and Applications (OOPSLA), October 2013
    3.                (with G. Richards, C. Hammer, F. Zappa Nardelli, J. Vitek). (abstract)
    4.        2. Plan B: A Buffered Memory Model for Java
    5.                ACM Symposium on Principles of Programming Languages (POPL), January 2013
    6.                (with D. Demange, V. Laporte, L. Zhao, D. Pichardie, J. Vitek). (abstract)
    7.        3. Compositional and Lightweight Dependent Type Inference for ML,
    9.                International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), January 2013
    10.                (with H. Zhu). (abstract)
    11.        4. Proof-Directed Parallelization Synthesis by Separation Logic,
    13.                ACM Transactions on Programming Languages and Systems (TOPLAS), 35(2):8, 2013
    14.                (with M. Botincan and M. Dodds). (abstract)
2012
    1.        1. Eliminating Read Barriers through Procrastination and Cleanliness
    2.                International Symposium on Memory Management (ISMM), June 2012
    3.                (with K.C. Sivaramakrishan. L. Ziarek). (abstract)
    4.        2. Resource-Sensitive Synchronization Inference Using Abduction,
    6.                ACM Symposium on Principles of Programming Languages (POPL), January 2012
    7.                (with M. Botincan and M. Dodds). (abstract)
2011
    1.        1. Accentunating the Positive: Atomicity Inference and Enforcement Using Correct Executions
    3.                ACM Conference on Object-Oriented Programming, Systems, Languages, and Architectures (OOPSLA), October 2011
    4.                (with D. Weeratunge and X. Zhang). (abstract)
      1.        2. Isolating Determinism in Multi-threaded Programs,
      3.                Runtime Verification, September 2011
      4.                (with L. Ziarek and S. Tiwary). (abstract)
        1.        3. Composable Asynchronous Events,
        3.                ACM Conference on Programming Language Design and Implementation (PLDI), June 2011
        4.                (with L. Ziarek, K.C. Sivaramakrishnan). (abstract)
        5.        4. Relaxed Memory Concurrency and Verifying Compilation,
        7.                ACM Symposium on Principles of Programming Languages (POPL), January 2011
        8.                (with J. Sevcik, V. Vafeiadis, F. Zappa Nardelli, and P. Sewell). (abstract)
          1.        5. Modular Reasoning for Deterministic Parallelism,
          3.                ACM Symposium on Principles of Programming Languages (POPL), January 2011
          4.                (with M. Dodds and M. Parkinson). (abstract)
2010
    1.        1. Analyzing Concurrency Bugs Using Dual Slicing,
    3.                International Symposium on Software Testing and Analysis, June 2010
    4.                (with D. Weeratunge, N. Sumner and X. Zhang). (abstract)
          1.        2. Analyzing Multicore Dumps to Facilitate Concurrency Bug Reproduction,
          3.                Architectual Support for Programming Languages and Operating Systems, March 2010
          4.                (with D. Weeratunge and X. Zhang). (abstract)
          5.        3. Lightweight Checkpointing for Concurrent ML,
          7.                Journal of Functional Programming, March 2010
          8.                (with L. Ziarek). (abstract)
          9.       
2009
        1.        1. Partial Memoization of Concurrency and Communication,
        3.                ACM International Conference on Functional Programming, September 2009
        4.                (with L. Ziarek and K.C.Sivaramakrishnan).(abstract)
        5.        2. Exceptionally Safe Futures,
        7.                Coordination, June 2009
        8.                (with A. Navabi).(abstract)
        9.        3. Semantics-Aware Trace Analysis,
        10.                ACM Conference on Programming Language Design and Implementation, June 2009
        11.                (with K. Hoffman and P. Eugster). (abstract)
        12.        4. Alchemist: A Transparent Dependence Distance Profiling Infrastructure,
        13.                ACM Conference on Code Generation and Optimization, March 2009
        14.                (with A. Navabi, X. Zhang). (abstract)
        15.        5. Speculative N-Way Barriers,
        17.               ACM Workshop on Declarative Aspects of Multicore Programming, January 2009.
        18.               (with L. Ziarek, M. Fluet, U. Acar). (abstract)

    2008

    1.         1. Flattening Tuples in an SSA Intermediate Representation, Higher-Order Symbolic
    2.                 Computation, December 2008 (with L. Ziarek, S. Weeks). (abstract)
      3.         2. A Uniform Transactional Execution Environment for Java,  European Conference on
                      Object-Oriented Programming, July 2008 (With L. Ziarek, A. Welc, A. Adl-tabatabai,
                      V. Menon, and T. Shpeisman). (abstract)
    3.         3. Protocol Inference Using Static Path Profiles, Static Analysis Symposium, July 2008                  (With R. Ramanathan, K. Sen, and A. Grama). (abstract)
    4.         4. Quasi-Static Scheduling for Safe Futures, ACM Conference on Principles and Practice of                 Parallel Programming, February 2008. (With A. Navabi and X. Zhang). (abstract)
    5.        

    2007
 
  1. 1.Static Specification Inference Using Predicate Mining, ACM Conference on Programming Language Design and Implementation, June 2007. (with M.K. Ramanathan and A. Grama).  (abstract)  
  2. 2.Path-Sensitive Inference of Function Precedence Protocols, International Conference on Software Engineering, May 2007. (with M.K. Ramanathan and A. Grama). (abstract) 
  3. 3.Randomized Protocols for Duplicate Elimination in Peer-to-Peer Storage Systems, IEEE Transactions on Parallel and Distributed Systems, May 2007. (with R. Ferreria, M.K. Ramanathan, and A. Grama). (abstract)
  4. 4.Randomized Leader Election, Distributed Computing, April 2007. (with M.K. Ramanathan, R. Ferrerira, A. Grama, and W. Szpankowski). (abstract)
  5. 5.Macroprogramming Heterogeneous Sensor Networks Using COSMOS, March 2007. (with A. Awan, and A. Grama). (abstract)
 
2006
  1. 1.Improving Duplicate Elimination in Storage Systems, ACM Transactions on Storage, November 2006. (with D. Bobbarjung and C. Dubnicki).  (abstract)
  2. 2.Stabilizers: A Modular Checkpointing Abstraction for Concurrent Functional Programs, ACM International Conference on Functional Programming, September 2006. (with L. Ziarek and P. Schatz). (abstract)
  3. 3.Sieve: A Tool for Automatically Detecting Variations Across Program Versions, IEEE Automated Software Engineering Conference, September 2006. (with M. Ramanathan and A. Grama). (abstract)
  4. 4.Transparently Reconciling Transactions with Locking for Java Synchronization, European Conference on Object-Oriented Programming (ECOOP), July 2006. (with A. Welc and A. Hosking). (abstract)
  5. 5.Trace-based Memory Aliasing Across Program Versions, Fundamental Approaches to Software Engineering, March 2006. (with M. Ramanathan and A. Grama). (abstract)
  6. 6.Revocation Techniques for Java Concurrency, Concurrency: Practice and Experience, October 2006. (with A. Welc and A. Hosking). (abstract)
  7. 7.Dynamic State Restoration Using Versioning Exceptions, Higher-Order Symbolic Computation, January 2006. (with N.V. Krishna). (abstract)
  8. 8.Unstructured Peer-to-Peer Networks for Sharing Processor Cycles, Parallel Computing, January 2006. (with A. Awan, R. Ferreira, and A. Grama). (abstract)
  9. 9.Locality in Structured Peer-to-Peer Networks, Journal of Parallel and Distributed Computing, January 2006. (with R. Ferreria and A. Grama). (abstract)
2005
  1. 1.Preemptible Atomic Regions for Real-time Java, IEEE Real-time Systems Symposium, December 2005. (with J. Manson, J. Baker, A. Cunei, M. Prochazka, B. Xin, and J. Vitek).
  2. 2.Safe Futures for Java, ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), October 2005. (with A. Welc and A. Hosking).
  3. 3.Randomized Protocols for Duplicate Elimination in Peer-to-Peer Storage Systems, IEEE 5th International Conference on Peer-to-Peer Systems, September 2005. (with R. Ferreira, M. Ramanathan, and A. Grama).
  4. 4.Search with Probablistic Guarantees in Unstructured Peer-to-Peer Networks IEEE 5th International Conference on Peer-to-Peer Systems, September 2005. (with R. Ferreira, A. Awan, M. Ramanathan, and A. Grama).
  5. 5.A Transactional Object Calculus, Science of Computer Programming, August 2005. (with J. Vitek, A. Welc, and A. Hosking).
  6. 6.VI-Attached Database Storage, IEEE Transactions on Parallel and Distributed Systems, January 2005. (with Y.Zhou, A.Bilas, D. Xinidis, and K. Li).
2004
  1. 1.Plethora: An Efficient Wide-Area Storage Systems, High-Performance Computing, December 2004. (with R. Ferreria, and A. Grama).
  2. 2.Preemption-Based Avoidance of Priority Inversion for Java, International Conference on Parallel Processing, August 2004. (with A. Welc and A. Hosking).
  3. 3.A Locality-Enhancing Peer-to-Peer Network, IEEE International Conference on Parallel and Distributed Systems, July 2004, (with R. Ferreria and A. Grama).
  4. 4.Transactional Monitors for Concurrent Objects, European Conference on Object-Oriented Programming, June 2004. (with A. Welc and A. Hosking).
  5. 5.A Semantic Framework for Designer Transactions, European Symposium on Programming, March 2004. (with A. Hosking, A. Welc, and J. Vitek).
  6. 6.Optimistic Concurrency Semantics for Transactions in Coordination Langauges, Coordination: Languages and Models, February 2004. (with J. Vitek).
2002
  1. 1.Experiences with VI Communication for Database Storage, International Symposium on Computer Architecture, June 2002 (with Y. Zhou, A. Bilas, C. Dubnicki, K. Li, and J. Philbin)
 
2000
 
  1. 1.Concurrency Analysis for Java, International Static Analysis Symposium, July 2000. (with C. Ungureanu).
  2. 2.Continuation-based Transformations for Coordination Languages, Theoretical Computer Science, July 2000.
  3. 3.Flow-Directed Closure Conversion for Typed Languages. European Symposium on Programming, March 2000. (with H. Cejtin and S. Weeks).
 
1999
 
  1. 1.Transparent Communication for Distributed Objects in Java. Java Grande'99. (with M. Hicks, R. Kelsey, J. Moore, and C. Ungureanu.)
 
1998
 
  1. 1.Compiling Java to a Typed Intermediate Language: A Preliminary Report. Types in Compilation, 1998. (with A. Wright, C. Ungureanu, and A. Hertzmann).
  2. 2.Polymorphic Splitting: An Effective Polyvariant Flow Analysis. ACM Transactions on Programming Languages and Systems, March 1998. (with A. Wright).
  3. 3.Single and Loving It: Must-Alias Analysis for Higher-Order Languages. ACM Symposium on Principles of Programming Languages. January 1998. ACM Press. (with P. Thiemann, S. Weeks, and A. Wright).
 
1997
 
  1. 1.Communication-Passing Style for Coordination Languages. 2nd International Conference on Coordination Models and Languages. September 1997.
  2. 2.Type-Directed Flow Analysis for Typed Intermediate Languages. 4th International Static Analysis Symposium. September 1997. (with S. Weeks and A. Wright).
 
1996
 
  1. 1.Flow-Directed Inlining. ACM Symposium on Programming Language Design and Implementation. May 1996. (with A. Wright).
 
1995
 
  1. 1.Higher-Order Distributed Objects. ACM Transactions on Programming Languages and Systems. September 1995. (with H. Cejtin and R. Kelsey).
  2. 2.Effective Flow Analysis for Avoiding Runtime Checks. 2nd International Static Analysis Symposium. September 1995. (with A. Wright).
  3. 3.A Unified Treatment of Flow Analysis in Higher-Order Languages, ACM Symposium on Principles of Programming Languages, January 1995. ACM Press. (with S. Weeks).
 
1994
 
  1. 1.A Concurrent Abstract Interpreter. Lisp and Symbolic Computation. April 1994. (with Stephen Weeks and James Philbin).
  2. 2.Analyzing Stores and References in Parallel Symbolic Languages, ACM Symposium on Lisp and Functional Programming, June 1994. (with S. Weeks).