BFF: Foundational and automated verification of bitfield-manipulating programs
F. Zhu, M.J. Sammler, R. Lepigre, D. Dreyer, D. Garg, Proceedings of the ACM on Programming Languages 6 (2022) 1613–1638.