Expand description
Verified Memory Allocator
Model-checking and proof harnesses for the memory allocator, verifying no double allocation, use-after-free prevention, buddy system consistency, frame conservation, zone correctness, and alignment guarantees.
Structs§
- Alloc
Invariant Checker - Allocator invariant checker
- Allocator
Model - Model of the frame allocator for verification
- Bitmap
Model - Bitmap allocator model for small allocation verification
- Buddy
Block - Buddy block model for buddy system verification
Enums§
- Alloc
Model Error - Errors from allocator verification
- Frame
State - Allocation state of a frame
- Memory
Zone - Memory zones for zone-aware allocation