BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:IC Monday Seminar : "Solvers for Software Reliability and Security
 "
DTSTART:20110314T151500
DTSTAMP:20260407T043140Z
UID:3e3039e708b8c0bf211214bc8119a56278fdc6a8cd8236b1f4b75959
CATEGORIES:Conferences - Seminars
DESCRIPTION:Dr. Vijay Ganesh\, Massachusetts Institute of Technology - IC 
 Faculty candidate\nAbstract : Constraint solvers such as Boolean SAT or mo
 dular arithmetic solvers are increasingly playing a key role in the constr
 uction 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 b
 it-vectors and arrays\, a theory whose satisfiability problem is NP-comple
 te. STP has been used in developing a variety of new software engineering 
 techniques from areas such as formal methods\, program analysis and testin
 g. STP enabled a new and exciting testing technique known as Concolic test
 ing. STP-enabled Concolic testers have been used to find hundreds of previ
 ously 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 vari
 ables\, bounded regular expressions and context-free grammars\, another th
 eory 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 vulnerabil
 ities in applications with more than 100\,000 lines of PHP code using stat
 ic and dynamic analysis. I will discuss the techniques that make these sol
 vers scale to formulas with millions of variables and constraints derived 
 from real-world software engineering applications. I will also discuss som
 e related theoretical results. Finally\, I will talk about what the future
  for solvers might look like with a focus on multi-cores and programming l
 anguage design. Bio : Dr. Vijay Ganesh is a Research Scientist at MIT (Oct
 ober 2007 - present). He completed his PhD in computer science from Stanfo
 rd University in September 2007\, and a Bachelor of Technology degree from
  College of Engineering\, Trivandrum\, India. His primary research interes
 ts are constraint solvers and their applications to software reliability a
 nd computer security. His STP solver was the co-winner of the SMTCOMP comp
 etition for bit-vector solvers in2006 and 2010\, and his paper on HAMPI wo
 n the ACM Distinguished Paper Award in 2009.
LOCATION:BC 410 https://plan.epfl.ch/?room==BC%20410
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR