Keynote

SMT Solvers for Software Reliability and Security

Vijay Ganesh, MIT

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 SMT solvers on software engineering as a discipline is a recent phenomenon, largely attributable to impressive gains in solver efficiency and expressive power.

In my talk, I will motivate the need for SMT solvers, sketch out their research story thus far, and then describe my contributions to solver research. Specifically, I will talk about two SMT solvers that I designed and implemented, namely, STP and HAMPI, currently being used in 100+ research projects. I will talk about real-world applications enabled by my solvers, and the techniques I developed that helped make them efficient.

Time permitting, I will also talk about some theoretical results in the context of SMT solving.

Dr. Vijay Ganesh is a Research Scientist at MIT since October 2007. He completed his PhD in computer science from Stanford University in September 2007.

He is broadly interested in making software systems reliable and secure, primarily through the use of SMT solvers. Dr. Ganesh recently received a Google Faculty Research Award 2012 for research on SMT solvers, and won an ACM best paper award in 2009. His SMT solvers have won the international SMTCOMP competition (held along with the CAV conference) multiple times.

He has also done research in automatic software testing, hardware description languages and program obfuscation.