Candidate: Yusen Su
Date: April 29, 2026
Time: 10:00 AM
Location: In-person
Supervisor: Arie Gurfinkel
All are welcome!
Abstract:
Static program analysis is widely used to infer invariants related to memory safety, particularly invariants over memory objects. Relational object invariants are properties held by the fields of a (memory) object throughout its lifetime. For example, the length of a buffer never exceeds its capacity. Automatic inference of these invariants is particularly challenging because they are often temporarily broken during field updates.
This seminar presents an Abstract Interpretation-based solution to infer object invariants. The key insight is a new object abstraction for memory objects, where memory is divided into multiple memory banks, each containing several objects. Within each bank, objects are abstracted by separating the most recently used (MRU) object, represented precisely with strong updates, while the rest are summarized. For an effective implementation of this approach, a new composite abstract domain is introduced, which forms a reduced product of numerical and equality sub-domains. This design efficiently expresses relationships between a small number of variables (e.g., fields of the same abstract object).
The new domain is built in the CRAB abstract interpreter and evaluated on several benchmarks for memory safety. The experiments show that this new approach is significantly more scalable for relational properties than the existing implementation of CRAB. For precision, the new analysis is integrated as a pre-processing step to SEABMC bounded model checker, and shows that it is effective at both discharging assertions during pre-processing, and significantly improving the run-time of SEABMC.