I am an assistant professor in the Department of Electrical and Computer Engineering, cross-appoined with the School of Computer Science, Faculty of Mathematics, University of Waterloo, Canada, 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 applications in software engineering, security, and mathematics. My research interests are:
1) Computer-aided logic reasoning tools such as Boolean SAT/SMT solvers, and proof assistants (checkout software page)
2) Application of solvers in formal verification, software testing, security, and mathematics (checkout software page)
3) Mathematical logic, and foundations of mathematics
You can view my research statement here. I currently leads 4 projects: MapleSAT, The Z3 String Solver, MathCheck SAT+CAS system, and Attack Resistance. Previously, I led the STP project from 2005-2012.
The focus of my research is the theory and practice of computer-aided mathematical reasoning tools, and their applications in software engineering, security, and mathematics. My research interests are:
1) Computer-aided logic reasoning tools such as Boolean SAT/SMT solvers, and proof assistants (checkout software page)
2) Application of solvers in formal verification, software testing, security, and mathematics (checkout software page)
3) Mathematical logic, and foundations of mathematics
You can view my research statement here. I currently leads 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), SemanticScholar, DBLP, my publications page.
Awards, Honors, Medals, and Distinctions
- Winner of silver medal at SAT 2017 Competition (main track)
- Winner of silver medal at SAT 2017 Competition (no-limits track)
- ACM Test of Time Award at CCS 2016
- Best Paper Award at ACSAC 2016
- Ontario Early Researcher Award 2016, Canada
- Winner of gold medal at the SAT Competition 2016 (Main Track)
- Winner of gold medal at the SAT Competition 2016 (Application Track)
- Symbolic Computation + Satisfiability Checking (SC^2) Track Invited Paper @ CASC 2016
- IJCAI 'Sister Conference Best Paper Track' Invited Paper 2016
- IBM Faculty Award 2015
- Paper on MathCheck conjecture verifier selected for the JAR Journal Special Issue on Best Papers at CADE 2015
- Paper on Z3str2 String Solver selected for FMSD Journal Special Issue on the Best Papers at CAV 2015
- Best Paper Award at Software Product Lines Conference 2015 (SPLC 2015)
- Paper titled "Impact of Community Structure on SAT Solver Performance" judged best student paper at SAT 2014
- Google Faculty Research Award 2013 (Only 6 winners worldwide in software engineering in 2013)
- Heidelberg Laureate Forum 2013 Invitee
- Google Faculty Research Award 2011 (Only 9 winners worldwide in software engineering in 2011)
- ACM Distinguished (SIGSOFT) Paper Award @ ISSTA 2009 (for the HAMPI string solver paper)
- Ten-year Most Influential Paper at DATE for the "Expression ADL Paper" (awarded in 2008)
- STP solver ranked first in 2010 at the annual SMTCOMP competition (bitvector category)
- STP solver ranked first in 2006 at the annual SMTCOMP competition (bitvector category)
- STP solver ranked second in 2014 at the annual SMTCOMP competition (bitvector category)
- STP solver ranked second in 2011 at the annual SMTCOMP competition (bitvector category)
Teaching
Compilers (W2014, S2014, W2015, S2017)
Computer Security (W2013, S2014, S2017)
Algorithms and Data Structures (F2015)
Graduate courses
Computer-aided Reasoning (W2013, F2013, W2015, F2016, F2017)
Professional Service
- Co-chair: Association of Symbolic Logic (ASL) Special Session on Computer-aided Proofs 2017
- Co-chair: SC^2 Workshop (Symbolic Computation + Satisfiability Checking) 2017
- Co-chair: David Dill @ 60 Workshop at CAV 2017
- Lead Organizer: Fields Institute workshop on "Theoretical Foundations of SAT Solving" 2016
- Co-chair: SMT 2015
- Co-chair: CSTVA 2014
- Dagstuhl Co-organizer
- Steering committees: CSTVA Steering Committee Member 2017-present, The International SAT/SMT/AR Summer School Steering Committee Member 2017-present, SMT Steering Committee Member 2014-2015
- Technical Program Committee (TPC) Member/Organizer: CAV 2018, FM 2018, IJCAR 2018, FSCD 2018, FroCos 2017, SYNASC 2017, CP 2017, Association of Symbolic Logic (ASL) Special Session 2017, ICSE (NIER) 2017, PLDI (ERC) 2017, SC^2 2017, Fields Institute SAT Workshop 2016, USE 2016, SC^2 Workshop 2016, Formal Methods 2016, VSTTE 2016, PAAR 2016, ICCS 2016, ISAIM 2016, POPL (ERC) 2016, ICDCIT 2016, SPSM 2015, ASSESS 2015, CSTVA 2015, VSTTE 2015, SMT 2015, Formal Methods 2015, AAAI 2015, USE 2015, CSTVA 2014, ASSESS 2014, FroCos 2013, CSTVA 2013, SMT 2012, IEEE NCA 2012, SMT 2011, IEEE NCA 2011
- Organizer of Summer School on SAT/SMT Solvers 2011 held at MIT from June 12-17, 2011. (Reviews by Sean Heelan)
- Reviewer for many top formal methods, software engineering and testing conferences/journals (CACM, FMSD, TSE)
- Organizer of Summer School on Combination of Decision Procedures 2004 held at Stanford University from Aug 6-12, 2004
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 |