It turns out it's harder than you'd think to decide whether or not an optimization is a good idea. Of course there are some relatively simple optimizations that are obviously good, but a lot of those have already been implemented. Also, I'm not sure how many people are going to want to add a solver into their compilation path.
On the other hand, if we simply contribute optimizations then all LLVM users benefit.
We're also using Souper to reveal imprecisions in LLVM dataflow analyses such as known bits -- this turns out to work really well.
It's definitely still an active project, but I'm on sabbatical this academic year and have had much less time than usual for my regular research. I'll be getting back to it in June. Also, Raimondas Sasnauskas, who implemented the instruction synthesizer, finished his postdoc position and moved on.
In any case, there's been a lot of progress since I did that UW talk, for example here are some early synthesis results:
Looks like your other comment hit the max reply depth so this will need to finish up, but in any case I don't agree with your reading of the vice versa.
Frama-C can be used in "interpreter mode" where it acts like a checking C interpreter. It then catches a superset of the bugs that would be caught by Valgrind / ASan / UBSan. On the other hand it is slower and harder to use than those tools.
For new code and for actively maintained old code you are perfectly correct. But there is a huge amount of C code we still rely on that isn't getting enough attention and I don't want that getting broken either.
Delta Debugging provided a name and a generic algorithm for something that people had already been doing, but they hadn't been calling it anything and hadn't formulated it as an abstract problem.
DD just removes stuff. C-Reduce does lots more, such as inlining functions, rewriting the class hierarchy, instantiating templates, ...