My current research activities are with the Trustable Programming Group, overseen by my advisor, Prof. Bill Harris.
Safety Properties in Shape Analysis
I am interested in the automated generation of proofs for safety properties about the usage of heap objects in programs. I want to answer questions about the structural organization of such objects such as, "Does this linked list ever contain a cycle during the course of execution?" or, "Is this queue always sorted correctly?" or, "Does my tree re-balancing routine break the consistency of the tree or drop any nodes?" An answer in the affirmative should consist of a counterexample that illustrates a bug. The negative answer is a proof of correctness. This work is still heating up. Stay tuned!
In the summer of 2016, I collaborated with Prof. Jim Griffioen of the University of Kentucky on the cross-domain problem of high-level approaches to software-defined networking.
Multi-author Hierarchical Network Policies
Software-define networking (SDN) is the ability for routing protocols to be programmed into a network dynamically from a controller. A central authority can define forwarding rules to implement policies, firewalls, address translation, and other network functions. Moreover, these rules can be updated dynamically in response to network events to allow for adaptive policies like stateful firewalls and load balancing.
We are interested in the advantages of delegating the authorship of the total network policy to local administrators and even tenants of the network. Such an approach requires an automated framework in which an IT department can retain ultimate control while still yielding to the contributions of individuals. Our framework uses a hierarchical allocation of both permission and responsibility to users. At every point in the hierarchy, the framework answers the questions of what can be done and what should be done. The framework enforces permissions so that even a buggy or malicious contribution by an individual cannot overstep its bounds. Our hope is that this decentralized approach can allow organizations with large networks to safely crowdsource network governance and achieve the full power of SDN.
I have had the privilege to work under the supervision of Prof. Mark Moll in the lab of Prof. Lydia E. Kavraki during my time as an undergraduate at Rice University. Here I discuss the two major research projects I have produced with them.
Randomizing Graph Searches for Robustness
Finding the shortest path through a weighted graph is a well-understood task. With a cost heuristic, A* is the way to go. But what if the graph is not reliable? A broken edge or an incorrect weight can make the apparent shortest path a poor choice. The client wants options. So how can we find paths other than the shortest one? And what criteria can we use to evaluate the set of proposed alternatives?
It is still good for alternatives to be short. We could try the second shortest path, but in a moderately dense graph, it is likely to share almost all its edges with the original. The th shortest, for large , is probably better, but systematically checking all these options is expensive. Instead, consider an algorithm that encourages random deviations from known paths: it says, “What if this area of the graph, along the shortest path, is broken? Then what would the shortest path be? Now what about that area? Or both?” and so on, iteratively building a set of increasingly diverse alternatives. Intuitively, this heuristic simulates random breaking of the graph to build an arsenal that we hope will stand up against any specific issue with the actual graph.
This is the core of the contribution in my 2015 ICRA paper, together with applications for robotic motion planning and an analysis of the efficiency and quality of this approach. Also have a look at my code repository for this research.
High-dimensional Motion Planning Algorithms
The last time you carried a tray, or plate, or something else with two hands, did you keep it from spilling? How hard did you have to think in order to hold it level? For a robot that can be a very difficult task—not to execute the motion, but to compute beforehand what the motion should be. Each arm is a kinematic linkage, or series of joints. Each joint has one or more numbers associated to it explaining what angle it is currently set to. All the numbers taken together are a point in , and there is a computation that will tell us where this puts the end effector, or hand, of each arm. Holding a tray level means both hands are at the same height. This is called a constraint, which gives us an equation explaining how the numbers should relate to one another. This is the tricky part: not all of holds the tray level; instead, the tray is level on some curved surface, a manifold, with dimension . Having trouble visualizing that? So am I.
A computer does not mind the high dimensions though. Teach it the math, and it does just fine. It is the curviness of the manifold that causes the difficulty. What kind of formula explains how to move along the manifold without leaving it (and spilling lunch!)? We often do not have such a formula. This is problematic for motion planning algorithms that try to find paths by connecting valid robot configurations without hitting any obstacles. A good solution is to look around and pretend the manifold is flat where you are (a hyperplane). Then moving around is just some easy linear algebra! As long as you stay close, you can fix any errors that creep in as the manifold curves away from the plane. But once you get too far away, you have to switch to a different plane—a different linear approximation of the manifold. Each of these planar regions is called a chart, and together the charts make up an atlas of the manifold.
This technique for manifolds has already been combined with one existing algorithm for robotic motion planning. I am currently authoring a paper which takes the idea further, by combining it with a host of existing algorithms for robotic motion planning. The goal is to produce a powerful tool chest that solves a variety of problems for constrained kinematic linkages or any high-dimensional system with equations that imply a lower-dimensional manifold.