Coursera Flash Sale
40% Off Coursera Plus for 3 Months!
Grab it
Watch this 31-minute conference talk from CPP 2025 where researchers Louis Cheung, Alistair Moffat, and Christine Rizkallah from the University of Melbourne present the first formal verification of the Burrows-Wheeler Transform (BWT) and its inverse. Learn how they used Isabelle/HOL to provide mechanized proof of correctness, invertibility, and termination for both transformations. The BWT is a critical algorithm used in everyday file compression software like bzip2 and sophisticated bioinformatics tools for DNA sequencing, making its verification essential for critical applications. The presentation addresses a gap in formal verification of compression algorithms and establishes a foundation for verifying various algorithms that operate on BWT-transformed sequences. The talk includes supplementary materials available through Zenodo and was presented at the ACM SIGPLAN and SIGLOG sponsored CPP 2025 conference.
