Pranav Garg

Applied Scientist
Amazon Web Services (AWS) AI
New York City

Email: prangarg [AT] amazon.com



Research Interests: Machine learning, Programming Languages, Formal methods, Security.

Research:
  • Current (at Amazon)
    • Malware detection in Amazon EC2 by learning malware-related network activity
    • Estimating causal effects of customer purchase actions on downstream revenue

  • Past (at UIUC)
    • Machine learning based inductive program invariant synthesis
    • Natural proof tactics to aid verification of (1) data-structure programs and (2) asynchronous event-driven systems
    • Deductive verification of concurrent programs


Prior to joining Amazon, I finished my PhD in 2015 from the department of Computer Science at the University of Illinois at Urbana-Champaign (UIUC), where my PhD advisor was Prof. Madhusudan Parthasarathy. At different points in time, I spent my summers as a graduate student at NEC labs (with Franjo Ivancic and Gogul Balakrishnan ), Microsoft Research India (with Akash Lal) and EPFL Switzerland (with George Candea). Prior to joining graduate school, I completed my under-graduate studies from the Indian Institute of Technology Kanpur, India.


[ Publications | CV ]

Publications

Articles Under Submission

  • Certified Program Models for Eventual Consistency. PDF
    • Edgar Pek, Pranav Garg, Muntasir Raihan Rahman, Indranil Gupta, and P. Madhusudan

Invited Tutorials

  • Machine Learning based methods for Invariant Synthesis
    • Pranav Garg and P. Madhusudan
    27th Int'l Conf. on Computer Aided Verification (CAV), 2015.

Thesis

  • Learning-based Inductive Invariant Synthesis.
    • Pranav Garg
    Ph.D. Dissertation. University of Illinois at Urbana-Champaign (UIUC). July 2015

Refereed Journal Articles

  • Syntax-Guided Synthesis. PDF
    • Rajeev Alur, Rastislav Bodik, Eric Dallal, Dana Fisman, Pranav Garg, Garvit Juniwal, Hadas Kress-Gazit, P. Madhusudan, Milo Martin, Mukund Raghothaman, Shamwaditya Saha, Sanjit Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, Abhishek Udupa
    In Proceedings of the Marktoberdorf Summer School. NATO Science Series. Invited Article

  • Quantified Data Automata for Linear Data Structures. A Register Automaton Model with Applications to Learning Invariants of Programs Manipulating Arrays and Lists. PDF
    • Pranav Garg, Christof Loding, P. Madhusudan and Daniel Neider
    Formal Methods in System Design (FMSD). A Special Issue on Computer Aided Verification. Invited Article

Refereed Conference Publications

  • Horn-ICE Learning for Synthesizing Invariants and Contracts PDF
    • P. Ezudheen, D. Neider, D. D'Souza, P. Garg and P. Madhusudan
    Conference on Object-Oriented Programming Systems, Languages, and Applications (OOPSLA), 2018.

  • Invariant Synthesis for Incomplete Verification Engines PDF
    • Daniel Neider, Pranav Garg, P. Madhusudan, Shambwaditya Saha and Daejun Park
    24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2018.

  • Efficient Incrementalized Runtime Checking of Linear Measures on Lists
    • Alex Gyori, Pranav Garg, Edgar Pek and P. Madhusudan
    10th IEEE International Conference on Software Testing, Verification and Validation (ICST), 2017.

  • Learning Invariants Using Decision Trees and Implication Counterexamples. Tool
    • Pranav Garg, P. Madhusudan, Daniel Neider and Dan Roth
    43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), 2016.

  • Alchemist: Learning Guarded Affine Functions.
    • Shambwaditya Saha, Pranav Garg, and P. Madhusudan
    27th Int'l Conf. on Computer Aided Verification (CAV), 2015.

  • Natural Proofs for Asynchronous Programs using Almost-Synchronous Reductions. PDF
    • Ankush Desai, Pranav Garg and P. Madhusudan
    28th Intl. Conf. on Object-oriented Programming, Systems, Languages, and Applications (OOPSLA), 2014.

  • ICE: A Robust Framework for Learning Invariants. PDF, Project Page
    • Pranav Garg, Christof Loding, P. Madhusudan and Daniel Neider
    26th Int'l Conf. on Computer Aided Verification (CAV), 2014.
    *Invited for submisison to Journal of the ACM (JACM)*

  • Learning Universally Quantified Invariants of Linear Data Structures. PDF, Project Page, arXiv
    • Pranav Garg, Christof Loding, P. Madhusudan and Daniel Neider
    25th Int'l Conf. on Computer Aided Verification (CAV), 2013.
    *Invited for submisison to Formal Methods in System Design (FMSD)*

  • Quantified Data Automata on Skinny Trees: an Abstract Domain for Lists. PDF, Project Page
    • Pranav Garg, P. Madhusudan and Gennaro Parlato
    20th Static Analysis Symposium (SAS), 2013.

  • Natural Proofs for Structure, Data, and Separation. PDF, Supplementary Appendix, Project Page
    • Xiaokang Qiu, Pranav Garg, Andrei Stefanescu and P. Madhusudan
    ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI), 2013.

  • Feedback-Directed Unit Test Generation for C/C++ using Concolic Execution. PDF
    • Pranav Garg, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda and Aarti Gupta
    35th Int'l Conf. on Software Engineering (ICSE), 2013.

  • Compositionality Entails Sequentializability. PDF
    • Pranav Garg and P. Madhusudan
    17th Int'l Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), 2011.

  • Rebound: Scalable Checkpointing for Coherent Shared Memory. PDF
    • Rishi Agarwal, Pranav Garg and Josep Torrellas
    38th Int'l Symposium on Computer Architecture (ISCA), 2011.

Industry Publications (Internally peer-reviewed)

  • Malware Detection in Amazon EC2
    • Pranav Garg and Vineet Chaoji
    5th Amazon Machine Learning Conference (AMLC), 2017.

Refereed Workshop Publications

  • A New Reduction for Event-Driven Distributed Programs. PDF
    • Ankush Desai, Pranav Garg and P. Madhusudan
    7th International Workshop on Exploiting Concurrency Executionciently and Correctly (EC2), 2014.

Patents

  • Jointly Estimating *Valid* Causal Effects of Multiple R-related Events
    • Pranav Garg, Vineet Chaoji, Karthik Gurumoorthy
    Approved for filing with the US Patent Office.

  • Artificial Intelligence System for Network Traffic Flow-based Detection of Service Usage Policy Violations
    • Vineet Chaoji, Pranav Garg
    Approved for filing with the US Patent Office.

  • Automatically Identifying Dynamic Applications
    • Saurabh Sohoney, Vineet Chaoji, Pranav Garg
    Approved for filing with the US Patent Office.

  • Feedback-Directed Random Class Unit Test Generation Using Symbolic Execution. US Patent Number 20130091495
    • Pranav Garg, Franjo Ivancic, Gogul Balakrishnan, Naoto Maeda and Aarti Gupta

top

Last Updated: July, 2017.