Bill Hallahan is a PhD student at Yale University, where he works with Ruzica Piskac. His current work is on automated firewall repair and symbolic execution of Haskell programs.
The goal of the firewall work is to repair a problem in a firewall script based on examples. Each example is a description of a packet or sequence of packets, along with whether each example should be accepted or dropped by the firewall. The work involves converting the firewalls to SMT formulas, which allows both finding values that satisfy desirable properties, and checking that desired properties are satisfied.
Bill is also currently working on symbolic execution of Haskell programs. Given unannotated Haskell source code, we aim to determine either inputs that lead down all possible paths in the program, or input that will produce output satisfying a given predicate. This requires generation of constraints, expressed in first order logic, on the Haskell program's output, which can be solved by an SMT solver.