Abstract: Software controls every device, system, and infrastructure serving our society. The rapid growth of complexity and high demand for human resources makes the task of building software tedious and error-prone. With techniques to automated reasoning, we hope to get more trustworthy, secure, and efficient programs; and in this talk, I will overview how such techniques can be built on top of solvers for Satisfiability Modulo Theories (SMT). SMT-based tools not only reveal bugs but also synthesize proofs that no bugs can ever occur. In particular, when verifying program safety, a proof is an inductive invariant; when proving program termination, a proof is a ranking function; and when proving program non-termination, a proof is a recurrence set. SMT-based synthesis of these proofs necessitates exploring a usually large search space, which however can be pruned using the program's source code. I will present an extensible verification framework called FreqHorn that is scalable and fast while solving a wide range of practical verification tasks. FreqHorn enables a broader class of applications, and in the future, it will help push the frontiers in automated program repair, functional synthesis, and security verification.