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
|