Home
Selected Publications
See also:    DBLP   Google Scholar

  1.        Morpheus: Automated Safety Verification of Data-Dependent Parser Combinator Programs
                   European Conference on Object-Oriented Programming (ECOOP), September 2023
                   (with A. Mishra) (abstract)

  2.        Covering All the Bases: Type-Based Verification of Test Input Generators
                   ACM Conference on Programming Language Design and Implementation (PLDI), June 2023
                   (with Z. Zhou, A. Mishra, and B. Delaware) (Distinguished Paper) (abstract)

  3.        Specification-Guided Component-Based Synthesis from Effectful Libraries
                   ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), December 2022
                   (with A. Mishra) (abstract)

  4.        Defending Observation Attacks in Deep Reinforcement Learning via Detection and Denoising
                   European Conference on Machine Learning and Principles and Practice of Knowledge Discovery in Databases (ECML/PKDD), October 2022
                   (with Z. Xiong, J. Eappen, H. Zhu) (abstract)

  5.        DistSPECTRL: Distributing Specifications in Multi-Agent Reinforcement Learning Systems
                   European Conference on Machine Learning and Principles and Practice of Knowledge Discovery in Databases (ECML/PKDD), October 2022
                   (with J. Eappen) (abstract)

  6.        Model-free Neural Lyapunov Control for Safe Robot Navigation
                   International Conference on Intelligent Robots and Systems
                   (with Z. Xiong, J. Eappen, A. Querishi) (abstract)

  7.        Data-Driven Abductive Inference of Library Specifications
                   ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA), October 2021
                   (with Z. Zhou, R. Dickerson, and B. Delaware) (Distinguished Artifact) (abstract)

  8.        Repairing serializability bugs in distributed database programs via automated schema refactoring
                   ACM Conference on Programming Language Design and Implementation (PLDI), June 2021
                   (with K. Rahmani, K.Nagar, and B. Delaware) (abstract)

  9.        Semantics, Specification, and Bounded Verification of Concurrent Libraries in Replicated Systems
                   Computer-Aided Verification (CAV), July 2020
                   (with K.Nagar) (abstract)

  10.        ART : Abstraction Refinement-Guided Training for Provably Correct Neural Networks
                   Formal Methods in Computer-Aided Design (FMCAD), September 2020
                   (with H. Zhu, R. Samanta) (abstract)

  11.        Mergeable Replicated Data Types
                   ACM Conference on Object-Oriented Programming, Languages, Systems, and Applications (OOPSLA), November 2019
                   (with G. Kaki, S. Priya, K.C. Sivaramakrishnan) (abstract)

  12.        CLOTHO: Directed Test Generation for Weakly-Consistent Database Systems
                   ACM Conference on Object-Oriented Programming, Languages, Systems, and Applications (OOPSLA), November 2019
                   (with K. Rahmani, B. Delaware) (abstract)

  13.        An Inductive Synthesis Framework for Verifiable Reinforcement Learning
                   ACM Conference on Programming Language Design and Implementation (PLDI), June 2019
                   (with H. Zhu, Z. Xiong, S. Magill) (Distinguished Paper) (abstract)

  14.        Automated Parameterized Verification of CRDTs
                   Computer-Aided Verification (CAV), July 2019
                   (with K. Nagar) (abstract)

  15.        Safe Replication Through Bounded Concurrency Verification
                   ACM Conference on Object-Oriented Programming, Languages, Systems, and Applications (OOPSLA), November 2018
                   (with G. Kaki, K. Earnky, K.C. Sivaramakrishnan) (abstract)

  16.        Alone Together: Compositional Reasoning and Inference for Weak Isolation
                   ACM Symposium on Principles of Programming Languages (POPL), January 2018
                   (with G. Kaki, K. Nagar, M. Najafzadeh) (abstract)

  17.        A Data-Driven CHC Solver
                   ACM Conference on Programming Language Design and Implementation (PLDI), June 2018
                   (with H. Zhu, S. Magill) (Distinguished Paper) (abstract)

  18.        Automated Detection of Serializability Violations Under Weak Consistency
                   29th International Conference on Concurrency Theory (CONCUR), September 2018
                   (with K. Nagar) (abstract)

  19.        Verifying a Concurrent Garbage Collector using a Rely-Guarantee Methodology
                   Interactive Theorem Proving (ITP), October 2017
                   (with Y. Zakowski1, D. Cachera, D. Demange, G. Petri, D. Pichardie, J. Vitek) (abstract)

  20.        Automatically Learning Shape Specifications
                   ACM Conference on Programming Language Design and Implementation (PLDI), June 2016
                   (with H. Zhu and G. Petri). (abstract)

  21.        Representation without Taxation: A Uniform, Low-Overhead and High-Level Interface to Eventually Consistent Key-Value Stores
                   IEEE Data Engineering Bulletin, 39(1)2016
                   (with G. Kaki and K.C. Sivaramakrishnan). (abstract)

  22.        Verifying Custom Synchronisation Constructs Using Higher-Order Separation Logics
                   ACM Transactions on Programming Languages and Systems (TOPLAS), 38(2):4, 2016
                   (with M. Dodds, M.J. Parkinson, K. Svendsen, L. Birkedal). (abstract)

  23.        Learning Refinement Types
                   ACM International Conference on Functional Programming (ICFP), September 2015
                   (with H. Zhu and A. Nori). (abstract)

  24.        Cooking the Books: Formalizing JMM Implemetation Recipes
                   European Conference on Object-Oriented Programming (ECOOP), July 2015
                   (with G. Petri and J. Vitek. (abstract)

  25.        Poling: SMT-Aided Linearizability Proofs
                   Computer Aided Verification (CAV), July 2015
                   (with H. Zhu and G. Petri). (abstract)

  26.        Declarative Programming over Eventually Consistent Data Stores
                   ACM Conference on Programming Language Design and Implementation (PLDI), June 2015
                   (with K.C. Sivaramakrishnan and G. Kaki). (abstract)

  27.        Synthesizing Racy Tests
                   ACM Conference on Programming Language Design and Implementation (PLDI), June 2015
                   (with M. Samak and M. Ramanathan). (abstract)

  28.        Dependent Array Type Inference from Tests
                   International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), January 2015
                   (with H. Zhu and A. Nori). (abstract)

  29.        MultiMLton: A Multicore-aware Runtime for Standard ML
                   Journal of Functional Programming, 24(6)
                   (with K.C. Sivaramakrishnan and L. Ziarek). (abstract)

  30.        A Relational Framework for Higher-Order Shape Analysis
                   ACM International Conference on Functional Programming (ICFP), September 2014
                   (with G. Kaki). (abstract)

  31.        Atomicity Refinement for Verified Compilation
                   ACM Transactions on Programming Languages and Systems (TOPLAS), 36(2):6
                   Presented at PLDI, June 2014
                   (with V. Laporte, G. Petri, D. Pichardie, and J. Vitek). (abstract)

  32.        Rx-CML: A Prescription for Safely Relaxing Synchrony
                   Conference on Practical Aspects of Declarative Languages (PADL), January 2014
                   (with K.C. Sivaramakrishnan and L. Ziarek). (abstract)

  33.        Flexible Access Control for Javascript
                   ACM Conference on Object-Oriented Programming, Systems, Languagess, and Applications (OOPSLA), October 2013
                   (with G. Richards, C. Hammer, F. Zappa Nardelli, J. Vitek). (abstract)

  34.        Plan B: A Buffered Memory Model for Java
                   ACM Symposium on Principles of Programming Languages (POPL), January 2013
                   (with D. Demange, V. Laporte, L. Zhao, D. Pichardie, J. Vitek). (abstract)

  35.        Compositional and Lightweight Dependent Type Inference for ML,
                   International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI), January 2013
                   (with H. Zhu). (abstract)

  36.        Proof-Directed Parallelization Synthesis by Separation Logic,
                   ACM Transactions on Programming Languages and Systems (TOPLAS), 35(2):8, 2013
                   (with M. Botincan and M. Dodds). (abstract)

  37.        Eliminating Read Barriers through Procrastination and Cleanliness
                   International Symposium on Memory Management (ISMM), June 2012
                   (with K.C. Sivaramakrishan. L. Ziarek). (abstract)

  38.        Resource-Sensitive Synchronization Inference Using Abduction,
                   ACM Symposium on Principles of Programming Languages (POPL), January 2012
                   (with M. Botincan and M. Dodds). (abstract)

  39.        Accentunating the Positive: Atomicity Inference and Enforcement Using Correct Executions
                   ACM Conference on Object-Oriented Programming, Systems, Languages, and Architectures (OOPSLA), October 2011
                   (with D. Weeratunge and X. Zhang). (abstract)

  40.        Isolating Determinism in Multi-threaded Programs,
                   Runtime Verification, September 2011
                   (with L. Ziarek and S. Tiwary). (abstract)

  41.        Composable Asynchronous Events,
                   ACM Conference on Programming Language Design and Implementation (PLDI), June 2011
                   (with L. Ziarek, K.C. Sivaramakrishnan). (abstract)

  42.        Relaxed Memory Concurrency and Verifying Compilation,
                   ACM Symposium on Principles of Programming Languages (POPL), January 2011
                   (with J. Sevcik, V. Vafeiadis, F. Zappa Nardelli, and P. Sewell). (abstract)


  43.        Modular Reasoning for Deterministic Parallelism,
                   ACM Symposium on Principles of Programming Languages (POPL), January 2011
                   (with M. Dodds and M. Parkinson). (abstract)


  44.        Analyzing Concurrency Bugs Using Dual Slicing
                   International Symposium on Software Testinng and Analysis (ISSTA), June 2010
                   (with D. Weeratunge, N. Sumner and X. Zhang). (abstract)


  45.        Analyzing Multicore Dumps to Facilitate Concurrency Bug Reproduction,
                   Architectual Support for Programming Languages and Operating Systems (ASPLOS), March 2010
                   (with D. Weeratunge and X. Zhang). (abstract)


  46.        Lightweight Checkpointing for Concurrent ML,
                   Journal of Functional Programming, March 2010
                   (with L. Ziarek). (abstract)


  47.        Partial Memoization of Concurrency and Communication,
                   ACM International Conference on Functional Programming (ICFP), September 2009
                   (with L. Ziarek and K.C.Sivaramakrishnan).(abstract)


  48.        Exceptionally Safe Futures,
                   Coordination, June 2009
                   (with A. Navabi).(abstract)


  49.        Semantics-Aware Trace Analysis,
                   ACM Conference on Programming Language Design and Implementation (PLDI), June 2009
                   (with K. Hoffman and P. Eugster). (abstract)


  50.        Alchemist: A Transparent Dependence Distance Profiling Infrastructure,
                   ACM Conference on Code Generation and Optimization (CGO), March 2009
                   (with A. Navabi, X. Zhang). (abstract)


  51.         Flattening Tuples in an SSA Intermediate Representation,
                    Higher-Order Symbolic Computation
                    December 2008 (with L. Ziarek, S. Weeks). (abstract)


  52.         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)    <\li>

  53.         Protocol Inference Using Static Path Profiles,
                     Static Analysis Symposium (SAS), July 2008
                     (With R. Ramanathan, K. Sen, and A. Grama). (abstract)


  54.         Quasi-Static Scheduling for Safe Futures,
                    ACM Conference on Principles and Practice of Parallel Programming (PPoPP), February 2008.
                    (With A. Navabi and X. Zhang) (abstract)