Hello! I'm Travis Hance, a researcher 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 a postdoctoral researcher at the Max Planck Institute for Software Systems working with the Principled Systems Group and the Foundations of Programming Group.
I have recently earned my Ph.D. from 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 enabling the verification of high-quality software. Towards this end, I work on software verification tooling with the aim of being scalable and usable. Modern verification theory is incredibly powerful, but much of that theory remains firmly in the realm of domain experts. I aim to extend and consolidate that theory into more friendly, approachable tools.
For example, in my PhD thesis, Verifying Concurrent Systems Code, I showed how to adapt ideas from the powerful but highly technical Iris separation logic into the scalable, semi-automated verification tool Verus. I demonstrate several applications of the work via highly-concurrent, high-performance software systems. These applications are state-of-the-art in both complexity and total verification effort.
Much of my work today revolves around the use of ownership types to enable automated verification along with techniques from separation logic. I believe that state-of-the-art type systems like Rust's borrowing system make ownership types practical for safe memory management. At MPI-SWS, I am currently working to expand our theoretical understanding of these relationships.
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.