Automated Generation of Non-Linear Loop Invariants Utilizing Hypergeometric Sequences

Andreas Humenberger, Maximilian Jaroschek, Laura Kovács

Analyzing and reasoning about safety properties of software systems becomes an especially challenging task for programs with complex flow and, in particular, with loops or recursio…