Steve Hsu

Steve in his office
third-year PhD student at the University of Pennsylvania

Contact Information

stevehsu at seas dot upenn dot edu

Research Interests



Compositional Learning and Verification of Neural Network Controllers: September 2019–November 2020 with Kishor Jothimurugan, Radoslav Ivanov, Shaan Vaidya, Rajeev Alur, and Osbert Bastani (PDF)
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.) This work was published at EMSOFT 2021.

Research Experience


Compositional reinforcement learning: December 2020–present with Kishor Jothimurugan, Rajeev Alur, and Osbert Bastani
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. The user specifies a set of modes (subtasks) and a set of transitions between modes, and we assume that the controller has access to the label of the current mode. If the user-provided modes have good starting regions, then simply training a controller for each mode and putting them together will produce a good composed controller. Our method corrects for bad starting regions in the user-provide modes by adjusting the starting regions during training.


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.


Machine learning libraries


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.