Automatic Inference of Relational Object Invariants

This conference talk presents a novel approach to automatically infer relational object invariants in software systems. Learn about an Abstract Interpretation-based solution that addresses the challenge of identifying relational properties held by fields of memory objects throughout their lifetime. Discover the innovative object abstraction technique that divides memory into multiple banks and separates the most recently used object for precise representation while summarizing the rest. Explore the implementation of a new composite abstract domain that efficiently expresses relationships between fields of the same abstract object. The presentation demonstrates how this approach achieves significantly better scalability for relational properties compared to existing implementations in the CRAB abstract interpreter, and shows its effectiveness when integrated with the SEABMC bounded model checker for both discharging assertions and improving run-time performance. This talk will be presented at the VMCAI conference in January 2025, sponsored by ACM SIGPLAN.