Constraint solvers such as Boolean SAT or modular arithmetic solvers are increasingly playing a key role in the construction of reliable and secure software.

In this talk, I will present two solvers STP and HAMPI. STP is a solver for the quantifier-free theory of bit-vectors and arrays, a theory whose satisfiability problem is NP-complete. STP has been used in developing a variety of new software engineering techniques from areas such as formal methods, program analysis and testing. STP enabled a new and exciting testing technique known as Concolic testing. STP-enabled Concolic testers have been used to find hundreds of previously unknown errors in Unix utilities, C/C++ libraries, media players, and commercial software, some with approximately a million lines of code. HAMPI is a solver for a rich theory of equality over bounded string variables, bounded regular expressions and context-free grammars, another theory whose satisfiability problem is NP-complete. HAMPI is primarily aimed at analysis of string-manipulating programs such as web applications and scripts. HAMPI has been used to find many unknown SQL injection vulnerabilities in applications with more than 100,000 lines of PHP code using static and dynamic analysis.

I will discuss the techniques that make these solvers scale to formulas with millions of variables and constraints derived from real-world software engineering applications. I will also discuss some related theoretical results. Finally, I will talk about what the future for solvers might look like with a focus on multi-cores and programming language design.