Brief Bio and CV

Dr. Vijay Ganesh is an assistant professor at the University of Waterloo since 2012. Prior to that he was a research scientist at MIT, 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 reasoning 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, The Z3 string solver, MapleSAT, and MathCheck. He has also proved several decidability and complexity results in the context of theories over string equations, regular expression membership, and integers. For his research, he has won over 21 research awards, best paper awards, distinctions, and medals. He recently won an ACM Test of Time Award at CCS 2016, the Early Researcher Award (ERA) given by the Ontario Government in 2016, Outstanding Paper Award at ACSAC 2016, an IBM Research Faculty Award in 2015, two Google Research Faculty Awards in 2013 and 2011, and a Ten-Year Most Influential paper award at DATE 2008. In total, he has won 9 best paper awards/honors of different kinds at conferences like CAV, IJCAI, CADE, ISSTA, SAT, SPLC, DATE and CCS. His solvers STP and MapleSAT have won numerous awards at the highly competitive international SMT and SAT solver competitions. In 2013 he was invited to the first Heidelberg Laureate Forum, a gathering where a select group of young researchers from around the world met with Turing, Fields and Abel Laureates.

You can explore Vijay's mathematical genealogy here, and in a concise format here. You can find Vijay Ganesh's Brief Bio in text format here.

Briefer Bio for Invited Talks

Dr. Vijay Ganesh is an assistant professor at the University of Waterloo since 2012. Prior to that he was a research scientist at MIT, 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 reasoning 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, The Z3 string solver, MapleSAT, and MathCheck. He has also proved several decidability and complexity results relating to the SATisfiability problem for various mathematical theories. For his research, he has won over 21 awards, honors, and medals including an ACM Test of Time Award at CCS 2016, two Google Faculty Research Awards in 2011 and 2013, and a Ten-Year Most Influential Paper Award at DATE 2008.