Computer Science Speaker Series Master Calendar

View Full Calendar

Special Seminar: Travis Hance, "Strong Foundations with Formal Methods: Bridging the Gap Between Theory and Practice"

Event Type
Seminar/Symposium
Sponsor
Illinois Computer Science
Virtual
wifi event
Date
Apr 23, 2024   10:00 am  
Views
110
Originating Calendar
Computer Science Special Seminar Series

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

link for robots only