Marcel Moosbrugger presented our joint work (see here) on invariant generation for unsolvable loops at the ACM SIGPLAN 29th Static Analysis Symposium (SAS 2022).
Abstract Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem.