Abstract
The Burrows-Wheeler transform (BWT) is an invertible lossless transformation that permutes input sequences into alternate sequences of the same length that frequently contain long localized regions that involve clusters consisting of just a few distinct symbols, and sometimes also include long runs of same-symbol repetitions. Moreover, there is a one-to-one correspondence between the BWT and suffix arrays. As a consequence, the BWT is widely used in data compression and as an indexing data structure for pattern search. In this formalization, we present the formal verification of both the BWT and its inverse, building on a formalization of suffix arrays.
License
Topics
Related publications
- Cheung, L., & Rizkallah, C. (2024). Formalized Burrows-Wheeler Transform (Artefact). Zenodo. https://doi.org/10.5281/ZENODO.14279882
- Cheung, L., Moffat, A., & Rizkallah, C. (2025). Formalized Burrows-Wheeler Transform. Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs, 187–197. https://doi.org/10.1145/3703595.3705883
- Ferragina, P., & Manzini, G. (n.d.). Opportunistic data structures with applications. Proceedings 41st Annual Symposium on Foundations of Computer Science, 390–398. https://doi.org/10.1109/sfcs.2000.892127
- Wikipedia
Session BurrowsWheeler
- Nat_Mod_Helper
- Rotated_Substring
- Count_Util
- Rank_Util
- Select_Util
- Rank_Select
- SA_Util
- SA_Count
- BWT
- BWT_SA_Corres
- IBWT