I am an assistant professor at Waterloo's ECE department, cross-appointed with the School of Computer Science in the Faculty of Mathematics, and the leader of the Waterloo Computer-aided Reasoning Group. The focus of my research is the theory and practice of computer-aided mathematical reasoning tools, and their application to software engineering and math. More specifically, my research interests are:

1) Computer-aided logic reasoning tools such as Boolean SAT/SMT solvers, and proof assistants (checkout my software page)
2) Application of solvers in formal verification, software testing, security, and mathematics (checkout my software page)
3) Mathematical logic, and foundations of mathematics

Checkout my research statement here. I currently lead 4 projects: MapleSAT, The Z3 String Solver, MathCheck SAT+CAS system, and Attack Resistance. Previously, I led the STP project from 2005-2012.

Papers: Google Scholar (most-cited first) or SemanticScholar or DBLP or Microsoft Academic Search or here.

Awards, Honors, Keynote Speeches, and Distinctions

  1. ACM Test of Time Award at CCS 2016
  2. Best Paper Award at ACSAC 2016
  3. Ontario Early Researcher Award 2016, Canada
  4. Winner of two gold medals at the SAT Competition 2016 (Main and Application Track)
  5. Symbolic Computation + Satisfiability Checking (SC^2) Track Invited Paper @ CASC 2016
  6. IJCAI 'Sister Conference Best Paper Track' Invited Paper 2016
  7. Keynote Address at CSTVA 2012 and 2016
  8. IBM Faculty Award 2015
  9. Paper on MathCheck conjecture verifier selected for the JAR Journal Special Issue on Best Papers at CADE 2015
  10. Paper on Z3str2 String Solver selected for FMSD Journal Special Issue on the Best Papers at CAV 2015
  11. Best Paper Award at Software Product Lines Conference 2015 (SPLC 2015)
  12. Paper titled "Impact of Community Structure on SAT Solver Performance" judged best student paper at SAT 2014
  13. Google Faculty Research Award 2013 (General area: software engineering. Specific topic: security testing)
  14. Heidelberg Laureate Forum 2013 Invitee
  15. Google Faculty Research Award 2011 (General area: software engineering. Specific topic: SMT solvers)
  16. Invited Tutorial on SMT Solvers at CAV 2011
  17. ACM Distinguished (SIGSOFT) Paper Award @ ISSTA 2009 (for the HAMPI string solver paper)
  18. Ten-year Most Influential Paper at DATE for the "Expression ADL Paper" (awarded in 2008)
  19. Constraint solver, STP, won the highly-competitive international SMTCOMP (bit-vectors category) competition for solvers in 2006/2010 and placed second in 2011/2014


  Undergraduate courses

     Compilers (W2014, S2014, W2015, S2017)
     Computer Security (W2013, S2014, S2017)
     Algorithms and Data Structures (F2015)
  Graduate courses
     Computer-aided Reasoning (W2013, F2013, W2015, F2016)

Professional Service

Contact Information

Department of Electrical and Computer Engineering          
University of Waterloo
200 University Avenue West
Waterloo, Ontario, Canada N2L 3G1
Office: DC 2530
Email: vganesh@uwaterloo.ca
Tel: +1 (519) 888-4567 x32866