Zoom: https://illinois.zoom.us/j/86025687514?pwd=UDhTK2pLeDFSQXMwOTNvOFgyOEtOQT09
Abstract:
The field of formal methods often promises to deliver bug-free software with mathematical guarantees of correctness. Unfortunately, despite large advances in the theory of program verification, we remain far from seeing it deployed widely in practice due to the amount of effort and technical expertise that is required. Furthermore, low-level systems software (e.g., memory allocators, file systems, and operating systems) often pose unique challenges that make formal methods even more challenging to apply. My research aims to make the powerful techniques of formal methods more accessible, bridging the gap between theory and practice.
Towards this end, I have designed verification tooling and demonstrated the verification of multiple pieces of low-level, concurrent systems software. My approach is chiefly based on considering powerful ideas from concurrent separation logic, extending them, and adapting them into the verification tooling for ergonomic, expressive programming languages. With this approach, I have shown that it is practical to verify a high-performance page cache used by SplinterDB (a database used in some production systems at VMware), as well as a state replication algorithm at the heart of NrOS and a memory allocator based on mimalloc. Recently, I have also been integrating these key ideas into Verus, a verification tool for Rust that I co-invented, which has also been adopted for verification efforts by independent researchers. In this talk, I will illustrate the key ideas of my methodology and explain why it is a viable path forward for practical systems verification.
Bio:
Travis Hance is a PhD Candidate in the CS Department at Carnegie Mellon University advised by Bryan Parno. Before attending graduate school, he did undergraduate at MIT and then worked in industry for a few years, where he worked on protocols for collaborative document editing.
Currently, Travis researches formal methods applied to low-level systems software. He enjoys collaborating with researchers and engineers who build complex software that benefits from formal verification. He collaborated with researchers at VMware to build and verify VeriBetrKV, a crash-safe key-value store, and he developed techniques to verify a high-performance page-cache of SplinterDB, a database used in some production systems. He also worked with researchers developing NrOS and led the verification of its novel state replication algorithm. Travis has a particular interest in Rust, due to its unique combination of features that make it well-suited for the verification of systems software, and he is a co-developer of Verus, a tool for verifying Rust code, focusing especially on its support for verified multi-threaded software and low-level libraries. He also works with concurrent separation logic, and he has developed the "Leaf" library, a framework for modular specifications of data structures that involve shared, read-only state.
Faculty Host: Tianyin Xu
Meeting ID: 860 2568 7514 ; Password: csillinois
