Search-based Inference of Class Invariants

Many techniques in formal verification and software testing rely on repOk routines to verify the consistency and validity of software components with complex data representations. A repOk function encodes the state properties necessary for an instance to be a valid object of the class under analysis, enabling early error detection and simplifying debugging. However, writing a correct and complete repOk can be challenging, even for advanced Large Language Models (LLMs). In this talk I will introduce Express, the first search-based algorithm designed to automatically generate a correct repOk for a given class. Express leverages simulated annealing, using the source code and test suite of the class under analysis to iteratively construct a repOk.