Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell. VIP: verifying real-world C idioms with integer-pointer casts. Proceedings of the ACM on Programming Languages, 6(POPL):1-32, 2022. [doi]
Abstract is missing.