Invariant Generation for Multi-Path Loops with Polynomial Assignments

Andreas Humenberger, Maximilian Jaroschek, Laura Kovács

Program analysis requires the generation of program properties expressing conditions to hold at intermediate program locations. When it comes to programs with loops, these properti…