Hello! I'm Travis Hance, a PhD student studying formal methods and software verification. I have an interest in writing software that is machine-checked to be correct and secure, and in establishing practical methods to do so. I'm especially interested in storage systems, asynchronous systems, and concurrent systems.
I am currently studying at Carnegie Mellon University under Bryan Parno.
You can contact me by e-mail me at,
My CV can be found here.
I'm primarily interested in verifying high-performance, asynchronous systems, including storage systems or multi-node distributed systems. I believe that doing so effectively involves formal reasoning at a variety of different levels, including at the low level of careful memory management, and the high level of abstract protocols. I'm interested in exploring proof architectures that can bring the right tools for each level of the proof stack.
Some of the tools I am interested in include separation logic, linear types, ownership types, SMT-based theorem proving, state transition systems, state machine refinement, and inductive invariant inference.
Right now, I am especially interested in how ownership types can enable automated verification along with techniques from separation logic. I also think that state-of-the-art type systems like Rust's borrowing system make ownership types practical for safe memory management. Therefore, I am exploring the intersection of these subjects.
I have been involved with the following projects:
(2021 – Present)
With Andrea Lattuada, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, Chris Hawblitzel, and others
Our tool for verified Rust code in the style of verification languages like Dafny. We take advantage of Rust's ownership type system to enable efficient verification conditions. I have been working on support for concurrent code and other advanced situations, including some of Rust's “unsafe” features.
(2020 – 2023)
With Reto Achermann, Alex Conway, Chris Hawblitzel, Jon Howell, Andrea Lattuada, Bryan Parno, Ryan Stutsman, Yi Zhou, and Gerd Zellweger
We originally built Linear Dafny for use in VeriBεtrFS to enable practical automation with imperative, heap-based data structures.
I added support for shared-memory concurrency, integreated the Leaf formalism, and worked with a host of other researchers to verify performant systems with low-level optimizations in this framework. Our paper is now available.
(2021 – 2023)
With Jon Howell, Bryan Parno, and Oded Padon.
I have been developing a formalism within separation logic for reasoning about state-sharing patterns that involve temporarily shared state, especially intended for verifying reader-writer locks and other algorithms that are used to manage shared state.
See our paper for more information.
(2019 – 2020)
With Chris Hawblitzel, Jon Howell, Rob Johson, Andrea Lattuada, Jialin Li, Bryan Parno, and Yi Zhou.
Our aim is to develop a verified, crash-safe, highly-performant file system. Currently, the state of the project is that we have produced a key-value store, which we call VeriBεtrKV, written in Dafny. We intend to use the key-value store as a building block for the file system. Developing tools to verify components of VeriBεtrFS has driven much of my research interest.(2018 – 2020)
With Bryan Parno, Ruben Martins, and Marijn Heule.
SWISS is an invariant inference tool to infer inductive invariants of distributed protocols, expressed as state transition systems. Our publication is available.