Computer Science Building, Room 142
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 variant of 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.
BIO:
http://people.csail.mit.edu/vganesh
Dr. Vijay Ganesh is a Research Scientist at MIT (October 2007 - present). He completed his PhD in computer science from Stanford University in September 2007, and a Bachelor of Technology degree from College of Engineering, Trivandrum, India. His primary research interests are constraint solvers and their applications to software reliability and computer security. His STP solver was the co-winner of the SMTCOMP competition for bit-vector solvers in 2006 and 2010, and his paper on HAMPI won the ACM Distinguished Paper Award in 2009.