A quantifier-elimination based heuristic for automatically generating inductive assertions for programs
automated software analysis and verification
scientific article; zbMATH DE number 5156698