I thought abstraction interpretation on the level that astree claims to implement is supposed to be extremely hard, which is why almost nobody else tries to do it. I only know of two that try:
[1] https://blogs.grammatech.com/how-sound-static-analysis-compl...