Software bugs are pervasive, but current techniques to find bugs are limited. Over the past decade, there are major algorithmic advances in constraint solvers, which enables the application of automated reasoning to find bugs in software. In this talk, I will give an introduction to this field, and talk about how automated reasoning relates to existing techniques such as testing and static analysis. I will briefly talk about existing automated reasoning tools that programmers can use to improve the quality of code. Then, I will talk about the leading edge research that we are doing to scale automated reasoning to real-world programs, often at least in the order of hundreds of thousands of lines of code.