Location: Davis Centre Room 1302
Post-seminar reception - 4:30 in the Davis Centre Fishbowl (DC 1301)
Over the last two decades, software engineering has witnessed a silent revolution in the form of Boolean SAT solvers. These solvers are now integral to many analysis, synthesis, verification, and testing approaches. This is largely due to a dramatic improvement in the scalability of these solvers vis-a-vis large real-world formulas. What is surprising is that the Boolean satisfiability problem is NP-complete, believed to be intractable in general, and yet these solvers easily solve instances containing millions of variables and clauses in them. How can that be?
Dr. Vijay Ganesh is an associate professor at the University of Waterloo. Prior to joining Waterloo in 2012, he was a research scientist at MIT (2007-2012) and completed his PhD in computer science from Stanford University in 2007. Vijay's primary area of research is the theory and practice of automated mathematical reasoning algorithms aimed at software engineering, formal methods, security, and mathematics. In this context he has led the development of many SAT/SMT solvers, most notably, STP, Z3 string, MapleSAT, and MathCheck. He has also proved several decidability and complexity results in the context of first-order theories. He has won over 25 awards, honours, and medals to-date for his research, including an ACM Test of Time Award at CCS 2016, an Ontario Early Researcher Award 2016, two Google Faculty Research Awards in 2011 and 2013, and a Ten-Year Most Influential Paper citation at DATE 2008.