About me
Hello! I’m Aaryan (Pronouns: He/Him), a computer science Ph.D. student at the School of Computer, Information, and Data Sciences at The University of Wisconsin-Madison in the madPL group advised by Tej Chajed. Before coming to Madison, I did my bachelor’s at Penn State University in Computer science with honors in computer science, adviced by Danfeng Zhang.
Research
I am boradly interested in formal verification, i.e. proving that a piece of code is doing what we expect it to do. My current research focuses on formalizing the compatibility of software updates, particularly within the context of complex system software. Updating extensive stacks of system software, whether for performance enhancements or feature additions, presents significant challenges and can lead to errors if certain functionalities are altered. I am working on formalizing the criteria for a software update to be compatible and using refinement for constructing machine-checked proofs by systematically reasoning through the layered implementation of the software stack. I intend to extend this work to verify the compatibility of software updates across various components of the software stack, including file system APIs and database schema migrations.
I have also worked on verifying differential privacy for deep learning algorithms. Differential privacy is gold standard for privacy-presesrving data analytics, but it is not easy to design differentially privacy algorithm. If we can formally verify a program’s differential privacy property, we can use it for designing differentially private algorithms. My work aims to verify the widely popular variant of DP - approximate differential privacy using the powerful proof technique of randomess alignment. I designed a general recipie for extending randomness alignment for approximate-DP and used it to verify differentially private gradient descent, and it’s variants.
I have used several off-the-shelf tools for my work on verification, like Dafny, Coq, Iris (Coq library for separation logic), lean, and CPAChecker.
During Fall 23, I did an independent study with Prof. Loris D’Antoni studying the capabilities of large language models in generating code and specifications. I explored grammar-constrained decoding, a technique to generate output constrained by context-free grammar.
Personal
Outside of work, I like weightlifting, running, swimming, and reading books. I am also getting into tennis lately, so if you know how to play let’s hit the court.
News
April 2024: I will be attending Oregon Programming Languages Summer School!
January 2024: Started a research assistantship supervised by Tej Chajed!
September 2023: Started Ph.D. at UW Madison Computer Sciences
June 2023: I attended my first academic conference - Programming language Design and Implementation and Selected as a finalist at the student research competition