Rodolphe Lepigre

VIP: verifying real-world C idioms with integer-pointer casts

2022 · Proceedings of the ACM on Programming Languages

Systems code often requires fine-grained control over memory layout and pointers, expressed using low-level ( e.g. , bitwise) operations on pointer values. Since these operations go beyond what basic pointer arithmetic in C allows, they …