Predicate abstraction and CEGAR for disproving termination of higher-order functional programs

From MaRDI portal