Steve Hsu

Steve in front of the Royal Palace of Amsterdam
second-year PhD student at the University of Pennsylvania

Contact Information

stevehsu at seas upenn edu

Research Interests


Research Experience


Compositionally reinforcement learning December 2020–present 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: January–July 2019 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
I wrote some tests for an equivalence checker late in this project's development. The equivalence checker works on on loop-free programs written either in an assembly language or in a DSL designed to express cryptographic algorithms. The results of the project are published in the paper Automatic Equivalence Checking for Assembly Implementations of Cryptographic Algorithms.




Programming Languages


Industry Experience

internship at Amazon Connect (Amazon Web Services), summer 2018
I implemented a variation of a feature called least-cost routing, which sends an outgoing call through the cheapest available carrier.