Automatic Inference of Relational Object Invariants for Improved Memory Safety Analysis

This paper presents a novel abstract interpretation-based technique and domain, MRUD, for automatically inferring relational object invariants, significantly improving the precision and scalability of memory safety analysis in programs with complex data structures.