BFF: Foundational and Automated Verification of Bitfield-Manipulating Programs
summary
A foundational, automated verifier encodes common bitfield patterns as structured bit vectors and implements partial, semantics-preserving operations (masking, merging) so bitwise code is reduced to record- and range-level reasoning instead of general bitvector proofs. It builds on RefinedC and mechanizes soundness in Coq/Iris, verifies real functions from Linux and pKVM page-table code, and runs across four codebases with most proofs automatic and only three manual side conditions required.
AI-written summary · about