Formalized Burrows-Wheeler Transform
summary
First mechanized verification of the Burrows‑Wheeler transform and its inverse, formalized in Isabelle/HOL and proven correct, invertible, and terminating; two constructions are shown equivalent—the canonical rotation sort and a suffix‑array based method that uses a prior linear‑time SA characterization—and a verified linear-time inverse is developed (uses auxiliary arrays that are themselves constructible in linear time). Artifacts and proofs are available; the work targets correctness guarantees for BWT use in compression and genomic indexing rather than new compression heuristics.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:21Motivation and background
- 3:38Paper contributions
- 5:21Canonical BWT construction
- 9:38Suffix array construction
- 13:56Key properties of the BWT
- 17:52Inverse BWT construction
- 23:11Conclusion and future work
- 26:24Q&A session
related talks
14mVerification of Algorithm and Code Generation for Signal Transforms- 14mVerification of Algorithm and Code Generation for Signal Transforms
18mA Verified Compiler for a Functional Tensor Language
06mVerified Reversible Programming for Verified Lossless Compression
20mA Mechanized Algebra of Verified Data Structures for Optimizing Sparse Tensor Programs
33mA Historical Perspective on Program Transformation and Recent Developments (Invi...
16mCertified Decision Procedures for Width-Independent Bitvector Predicates
25mA Lazy, Concurrent Convertibility Checker