We believe abstract interpretation, and formal methods in general, has the potential to make a significant contribution to making software safer. Based on a solid theoretical foundation in abstract interpretation and deductive verification we have spent the past fifteen years leveraging these powerful theories to implement practical static analysis tools that scale to applications of hundreds of thousands of lines of code.