Excellent post. Aside from the very interesting and important (hence many PLDI publications) work of Sorin Lerner, there is a workshop which deals with the first point of Prof. Regehr: Compiler Optimization meets Compiler Verification, which is a satellite workshop for ETAPS. So for interested people, this might very well be the point to start digging for relevant publications.
