Vijay Ganesh is an associate professor in the Department of Electrical and Computer Engineering, cross-appoined with the School of Computer Science, faculty of mathematics, and the leader of the Waterloo Computer-aided Reasoning Group. The focus of his research is the theory and practice of computer-aided mathematical reasoning algorithms and their applications in software engineering, security, and mathematics.

Dr. Ganesh currently leads the following projects:
  1. SAT Solvers and Machine Learning (MapleSAT)
  2. Complexity-theoretic analysis of SAT/SMT and AR
  3. SAT-based Cryptanalysis and parallel SAT solvers
  4. Z3str3 string, arithmetic, and regular expression solver
  5. MathCheck SAT+CAS combinatorial conjecture verifier
  6. Attack resistant security defense mechanisms and obfuscations
  7. Testing, verification, and analysis of physics simulation software
  8. Testing, verification, and analysis of smart contracts (advisor: quantstamp)
From 2005-2012, Dr. Vijay Ganesh led the STP Bitvector and Array solver project.

Papers: Google Scholar (most-cited first), SemanticScholar, DBLP, my publications page.

Notable Awards, Honors, Medals, and Distinctions

  1. IJCAI Sister Conference Best Paper Track Invited Paper 2018
  2. Silver medal at SAT 2017 Competition (main track)
  3. Silver medal at SAT 2017 Competition (no-limits track)
  4. Invited Paper at Constraint Programming 2017 (CP 2017) conference
  5. Among top 3 best papers at SAT 2017
  6. ACM Test of Time Award at CCS 2016
  7. Best Paper Award at ACSAC 2016
  8. Ontario Early Researcher Award 2016, Canada
  9. Gold medal at the SAT Competition 2016 (Main Track)
  10. Gold medal at the SAT Competition 2016 (Application Track)
  11. Symbolic Computation + Satisfiability Checking (SC^2) Track Invited Paper @ CASC 2016
  12. IJCAI Sister Conference Best Paper Track Invited Paper 2016
  13. IBM Faculty Award 2015
  14. Paper on MathCheck conjecture verifier selected for the JAR Journal Special Issue on Best Papers at CADE 2015
  15. Paper on Z3str2 String Solver selected for FMSD Journal Special Issue on the Best Papers at CAV 2015
  16. Best Paper Award at Software Product Lines Conference 2015 (SPLC 2015)
  17. Paper titled "Impact of Community Structure on SAT Solver Performance" judged best student paper at SAT 2014
  18. STP solver ranked second at the annual SMTCOMP competition 2014 (bit-vector category)
  19. Google Faculty Research Award 2013 (Only 6 winners worldwide in software engineering in 2013)
  20. Heidelberg Laureate Forum 2013 Invitee
  21. Google Faculty Research Award 2011 (Only 9 winners worldwide in software engineering in 2011)
  22. STP solver ranked second at the annual SMTCOMP competition 2011 (bit-vector category)
  23. STP solver ranked first at the annual SMTCOMP competition 2010 (bit-vector category)
  24. ACM Distinguished (SIGSOFT) Paper Award @ ISSTA 2009 (for the HAMPI string solver paper)
  25. Expression ADL paper cited as the ten-year most influential paper at DATE  (published 1999, citation in 2008)
  26. STP solver ranked first at the annual SMTCOMP competition 2006 (bit-vector category)

Teaching

  Undergraduate courses

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

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