U of A at Birmingham

Office: 4155 UH (map)

Email: gilrauab.edu

Twitter: @tomgilray

Thomas Gilray

My research focuses on declarative programming systems for high-performance automated reasoning and the design and implementation of tunable correct-by-design analyses of complex systems and especially software: mainly of higher-order, functional and logical languages. I also work on compiling, parallelizing, and incrementalizing such analyses, and on their applications—software verification, optimization, and auditing. More broadly, my interests include semantics, language design, compilers and their implementation, safety and verification, parallelism and high-performance logic solvers. Contact me if you have an idea which intersects with my research or broader interests and want to discuss it. I am looking for students!

News

• The HARP lab, with key collaborators at WSU, OSU, and UT, has won a PPoSS (Principles and Practice of Scalable Systems) Large award from the NSF, to develop Slog and related techniques into a full-stack approach to modern declarative programming. This ~$5M award will provide reliable support to roughly ten PhD students and seven faculty for its five year duration. Read more ↠
• The HARP lab has won a PPoSS (Principles and Practice of Scalable Systems) planning-grant award from the NSF, to develop a Large proposal on scaling Datalog-based compute platforms like Slog. See our preprint on the Slog language for more details.
• The HARP lab has won an award, through subcontract with Galois, inc., to work on the DARPA V-SPELLS program: Verified Security and Performance Enhancement of Large Legacy Software. We will be exploring the use of AI-based programming languages for reasoning about code at scale—in the cloud and on supercomputers. Read more ↠

Selected Publications

• Distributed Relational Algebra at Scale with Sidharth Kumar. IEEE International Conference on High Performance Computing, Data, and Analytics (HiPC). 2019. (pdf)
• Size-Change Termination as a Contract with Phúc C. Nguyễn, Sam Tobin-Hochstadt, and David Van Horn. SIGPLAN, Programming Language Design and Implementation (PLDI). 2019. (pdf)
• Soft Contract Verification for Higher-order Stateful Programs with Phúc C. Nguyễn, Sam Tobin-Hochstadt, and David Van Horn. SIGPLAN, Principles of Programming Languages (POPL). 2018. (pdf)
• Pushdown Control-Flow Analysis for Free. with Steven Lyde, Michael Adams, Matthew Might, and David Van Horn. SIGPLAN, Principles of Programming Languages (POPL). 2016. (pdf)
• Allocation Characterizes Polyvariance. with Michael Adams, Matthew Might. SIGPLAN, International Conference on Functional Programming (ICFP). 2016. (pdf) (invited JFP version)
• Dynamic Sparse-Matrix Allocation on GPUs. with James King, Robert M. Kirby, and Matthew Might. International Supercomputing Conference (ISC). 2016. (Winner of the PRACE ISC award.) (pdf)

All Publications

1. Distributed Relational Algebra at Scale with Sidharth Kumar. IEEE International Conference on High Performance Computing, Data, and Analytics (HiPC). 2019. (pdf)
2. Size-Change Termination as a Contract with Phúc C. Nguyễn, Sam Tobin-Hochstadt, and David Van Horn. SIGPLAN, Programming Language Design and Implementation (PLDI). 2019. (pdf)
3. Symbolic Path Tracing to Find Android Permission-Use Triggers with Kristopher Micinski, Daniel Votipka, Jeffrey S. Foster, and Michelle L. Mazurek. NDSS workshop on Binary Analysis Research (BAR). 2019. (pdf)
4. Racets: Faceted Execution in Racket with Zhanpeng Wang and Kristopher Micinski. SIGPLAN, Scheme Workshop (SC). 2018. (pdf)
5. Abstract Allocation as a Unified Approach to Polyvariance in Control-flow Analyses with Michael D. Adams, Matthew Might. Journal of Functional Programming (JFP). 2018. (Invited) (pdf) (ICFP version)
6. User Comfort with Android Background Resource Accesses in Different Contexts with Daniel Votipka, Seth M. Rabin, Kristopher Micinski, Michelle L. Mazurek, Jeffrey S. Foster. Symposium on Usable Privacy and Security (SOUPS). 2018. (pdf)
7. Soft Contract Verification for Higher-order Stateful Programs with Phúc C. Nguyễn, Sam Tobin-Hochstadt, and David Van Horn. SIGPLAN, Principles of Programming Languages (POPL). 2018. (pdf)
8. Toward Parallel CFA with Datalog, MPI, and CUDA with Sidharth Kumar. The Scheme Workshop (SW). 2017. (pdf)
9. Introspective Polyvariance for Control-Flow Analyses. Ph.D. Dissertation. University of Utah. 2016. (pdf)
10. Allocation Characterizes Polyvariance. with Michael Adams, Matthew Might. SIGPLAN, International Conference on Functional Programming (ICFP). 2016. (pdf)
11. Dynamic Sparse-Matrix Allocation on GPUs. with James King, Robert M. Kirby, and Matthew Might. International Supercomputing Conference (ISC). 2016. (Winner of the PRACE ISC award.) (pdf) (extended pdf)
12. Pushdown Control-Flow Analysis for Free. with Steven Lyde, Michael Adams, Matthew Might, and David Van Horn. SIGPLAN, Principles of Programming Languages (POPL). 2016. (pdf)
13. A Linear Encoding of Pushdown Control-Flow Analysis. with Steven Lyde and Matthew Might. The Scheme Workshop (SW). 2014.
14. Concrete and Abstract Interpretation: Better Together. with Maria Jenkins, Leif Andersen, and Matthew Might. The Scheme Workshop (SW). 2014.
15. Partitioning 0-CFA for the GPU. with James King and Matthew Might. International Workshop on Functional and Constraint Logic Programming (WFLP). 2014. (pdf)
16. A Unified Approach to Polyvariance in Abstract Interpretations. with Matthew Might. The Scheme Workshop (SW). 2013.
17. Sound and Precise Malware Analysis for Android via Pushdown Reachability and Entry-Point Saturation. with Shuying Liang, Andrew W. Keep, Matthew Might, David Van Horn, Steven Lyde, and Petey Aldous. Workshop in Security and Privacy for Smartphones (SPSM). 2013.
18. A Survey of Polyvariance in Abstract Interpretations. with Matthew Might. Symposium on Trends in Functional Programming (TFP). 2013. (Winner of the best student paper award.) (pdf)