My research focuses broadly on easing the task of developing reliable and efficient programs via program analysis. This area combines two disciplines: automated theorem proving and abstract interpretation. In the next 10 years, I am hoping to develop useful techniques in order to change the ways modern software is built addressing the above challenges. These methods will be implemented in real tools and will increase our understanding of the limitations of automatic methods.