SAT and SMT Solvers for Software Engineering and Security

Boolean SAT and SMT solvers increasingly play a central role in the construction of reliable and secure software, regardless of whether such reliability/security is ensured through formal methods, program analysis or testing. This dramatic influence of solvers on software engineering as a discipline is a recent phenomenon, largely attributable to impressive gains in solver efficiency and expressive power. Dr. Vijay Ganesh will motivate the need for SAT and SMT solvers, sketch out their research story thus far, and then describe his contributions to solver research. Specifically, he will talk about a SAT solver called MapleCMS, and a string SMT solver, called Z3str2, developed in his lab. He will also talk about real-world applications enabled by his solvers, and the techniques he developed that helped make them efficient.