University of Pennsylvania:
PhD student in computer science,
BS in computer science and mathematics (summa cum laude),
Compositionally reinforcement learning
with Rajeev Alur, Osbert Bastani, and Kishor Jothimurugan
We want to design a compositional reinforcement learning algorithm
that breaks up a complex task into subtasks, solves each subtask,
and combines the solutions into a procedure for the whole task.
We will require the user to give a
STRIPS-style specification of the problem,
and we'll need to specify how the STRIPS predicates correspond
to states in the reinforcement learning environment,
but we hope to automate the rest of the process.
Compositionally training and verifying a controller for an F1/10 car
September 2019–November 2020
with Rajeev Alur, Osbert Bastani, Shaan Vaidya, Kishor Jothimurugan, and Radoslav Ivanov
We trained a car to drive in a class of configurations of hallways
and we proved that it doesn't crash (at least in a simulator).
Our training was compositional in the sense that
we represented hallways as a sequnece of segments
(straight, 90° left, 90° right, 120° left, and 120° right),
trained a controller that can drive the car on each segment type,
and trained a mode predictor that decides which controller to use at any given moment.
Our verification was also compositional and proceeded by induction
on the number of segments in the hallway.
(For the base case, we needed to assume that
the car stared in a reasonable position.)
We submitted this work to PLDI in November 2020.
Verifying eBPF Programs:
with Santosh Nagarakatte and Srinivas Narayana
I wrote a translator
that takes in eBPF programs written in an assembly-like syntax
and outputs a Z3 query specifying the relationship
between its inputs and outputs.
This project studies the Linux kernel's eBPF verifier with the goal
of proving its soundness (or finding a counterexample).
Professors Nagarakatte and Narayana are continuing the project
with a Facebook Networking Systems Research Award.
Verifying Assembly Implementations of Cryptographic Algorithms:
September 2017–May 2018
with Jay Lim, Santosh Nagarakatte, and Mihai Andrei