Summary: We describe a system to prove properties of programs. The key feature of this approach is a method to automatically synthesize inductive invariants of the loops contained in the program. The method is generic, i.e., it applies to a large set of programming languages and application domains; and lazy, in the sense that it only generates invariants that allow one to derive the required properties. It relies on an existing system called GPiD for abductive reasoning modulo theories (see our work [ibid. 10900, 279–294 (2018; Zbl 1437.68190)]), and on the platform for program verification Why3 [J.-C. Filliâtre and A. Paskevich, ibid. 7792, 125–128 (2013; Zbl 1435.68366)]. Experiments show evidence of the practical relevance of our approach.
For the entire collection see [Zbl 1428.68022].