Generalizing and Derandomizing Gurvits's Approximation Algorithm for the Permanent. - Scott Aaronson; Travis Hance (Electron. Colloquium Comput. Complex., 2012)

End-To-End Policy-Agnostic Security for Database-Backed Applications. - Jean Yang 001; Travis Hance; Thomas H. Austin; Armando Solar-Lezama; Cormac Flanagan; Stephen Chong (CoRR, 2015)

Precise, dynamic information flow for database-backed applications. - Jean Yang 001; Travis Hance; Thomas H. Austin; Armando Solar-Lezama; Cormac Flanagan; Stephen Chong (PLDI, 2016)

Storage Systems are Distributed Systems (So Verify Them That Way!). - Travis Hance; Andrea Lattuada 001; Chris Hawblitzel; Jon Howell; Rob Johnson 001; Bryan Parno (OSDI, 2020)

Liquid information flow control. - Nadia Polikarpova; Deian Stefan; Jean Yang 001; Shachar Itzhaky; Travis Hance; Armando Solar-Lezama (Proc. ACM Program. Lang., 2020)

Finding Invariants of Distributed Systems: It's a Small (Enough) World After All. - Travis Hance; Marijn Heule; Ruben Martins; Bryan Parno (NSDI, 2021)

Sharding the State Machine: Automated Modular Reasoning for Complex Concurrent Systems. - Travis Hance; Yi Zhou 025; Andrea Lattuada 001; Reto Achermann; Alex Conway 001; Ryan Stutsman; Gerd Zellweger; Chris Hawblitzel; Jon Howell; Bryan Parno (OSDI, 2023)

Verus: Verifying Rust Programs using Linear Ghost Types (extended version). - Andrea Lattuada 001; Travis Hance; Chanhee Cho; Matthias Brun 002; Isitha Subasinghe; Yi Zhou 025; Jon Howell; Bryan Parno; Chris Hawblitzel (CoRR, 2023)

Leaf: Modularity for Temporary Sharing in Separation Logic (Extended Version). - Travis Hance; Jon Howell; Oded Padon; Bryan Parno (CoRR, 2023)

Verus: Verifying Rust Programs using Linear Ghost Types. - Andrea Lattuada 001; Travis Hance; Chanhee Cho; Matthias Brun 002; Isitha Subasinghe; Yi Zhou 025; Jon Howell; Bryan Parno; Chris Hawblitzel (Proc. ACM Program. Lang., 2023)

Leaf: Modularity for Temporary Sharing in Separation Logic. - Travis Hance; Jon Howell; Oded Padon; Bryan Parno (Proc. ACM Program. Lang., 2023)

Inductive Invariants That Spark Joy: Using Invariant Taxonomies to Streamline Distributed Protocol Proofs. - Tony Nuda Zhang; Travis Hance; Manos Kapritsos; Tej Chajed; Bryan Parno (OSDI, 2024)

Verus: A Practical Foundation for Systems Verification. - Andrea Lattuada 001; Travis Hance; Jay Bosamiya; Matthias Brun 002; Chanhee Cho; Hayley LeBlanc; Pranav Srinivasan; Reto Achermann; Tej Chajed; Chris Hawblitzel; Jon Howell; Jacob R. Lorch; et al. (SOSP, 2024)