THIS SITE

Information for

Vijay Ganesh

Assistant Professor

Contact InformationVijay Ganesh

Phone: 519-888-4567 x32866
Location: DC 2530

Website

Biography Summary

Dr. Vijay Ganesh is an assistant professor at the University of Waterloo's Electrical and Computer Engineering department, with a cross-appointment at the David R. Cheriton School of Computer Science. 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 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 integer arithmetic. He has won over 25 research awards, best paper awards, distinctions, and medals for his research to-date. 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, a Ten-Year Most Influential paper citation at DATE 2008, and 10 best paper awards/honors of different kinds at conferences like CAV, IJCAI, CADE, ISSTA, SAT, SPLC, 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.

Research Interests

  • Logic Reasoners Such As Boolean SAT/SMT Solvers And First-order Provers
  • Formal Methods
  • Automated Testing
  • Security
  • Program Analysis
  • Mathematical Logic
  • Foundations Of Mathematics
  • Information Systems
  • Software Engineering

Education

  • 2007, Doctorate, Computer Science, Stanford University
  • 2000, Master's, Electrical Engineering, Stanford University

Courses

  • ECE 750 - Special Topics in Computer Software
  • ECE 458 - Computer Security
  • ECE 351 - Compilers
  • SE 499 - Project

Selected/Recent Publications

  • {'i}n, The Meaning of Attack-Resistant Programs, arXiv preprint arXiv:1502.04023, 2015
  • Biere, Armin and Ganesh, Vijay and Grohe, Martin and Nordström, Jakob and Williams, Ryan, Theory and Practice of SAT Solving (Dagstuhl Seminar 15171), Dagstuhl Reports, 5(4), 2015
  • {'e}z{'e}quel, Jean-Marc and Rumpe, Bernhard and Beyersdorff, Olaf and others, Dagstuhl Reports, Vol. 4, Issue 10 ISSN 2192-5283, , 2015
  • Jayaraman, Karthick and Tripunitara, Mahesh and Ganesh, Vijay and Rinard, Martin and Chapin, Steve, Mohawk: Abstraction-refinement and bound-estimation for verifying access control policies, ACM Transactions on Information and System Security (TISSEC), 15(4), 2013
  • Ganesh, Vijay and Minnes, Mia and Solar-Lezama, Armando and Rinard, Martin, (Un) Decidability Results for Word Equations with Length and Regular Expression Constraints, arXiv preprint arXiv:1306.6054, 2013
  • Ganesh, Vijay and Carbin, Michael and Rinard, Martin, Cryptographic path hardening: Hiding vulnerabilities in software through cryptography, arXiv preprint arXiv:1202.0359, 2012
  • Michel, Raphaël and Hubaux, Arnaud and Ganesh, Vijay and Heymans, Patrick, An SMT-based approach to automated configuration, SMT Workshop 2012 10th International Workshop on Satisfiability Modulo Theories SMT-COMP, 2012
  • Ganesh, Vijay, STP/HAMPI and Computer Security, arXiv preprint arXiv:1204.2989, 2012
  • {o}rner, Nikolaj and Ganesh, Vijay and Michel, Raphaël and Veanes, Margus, An SMT-LIB format for sequences and regular expressions, Strings, 2012
  • Kiezun, Adam and Ganesh, Vijay and Artzi, Shay and Guo, Philip J and Hooimeijer, Pieter and Ernst, Michael D, HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars, ACM Transactions on Software Engineering and Methodology (TOSEM), 21(4), 2012
  • Jayaraman, Karthick and Ganesh, Vijay and Tripunitara, Mahesh and Rinard, Martin C and Chapin, Steve J, Arbac policy for a large multi-national bank, arXiv preprint arXiv:1110.2849, 2011
  • Barrett, Clark and Stump, Aaron and Tinelli, Cesare, The SMT-LIB Standard Version 2.0 DRAFT, , 2010
  • Cadar, Cristian and Ganesh, Vijay and Pawlowski, Peter M and Dill, David L and Engler, Dawson R, EXE: automatically generating inputs of death, ACM Transactions on Information and System Security (TISSEC), 12(2), 2008
  • Cadar, Cristian and Ganesh, Vijay and Pawlowski, Peter and Dill, David and Engler, Dawson, EXE: A system for automatically generating inputs of death using symbolic execution, Proceedings of the ACM Conference on Computer and Communications Security, 2006
  • Ganesh, Vijay, Logic and Complexity (Term Paper for cs357, spring 2001.), , 2001
  • {'e}sar and Owre, Sam and Rue{ss}, Harald and Rushby, John and Rusu, Vlad and Sa{i}di, Hassen and Shankar, Natarajan and others, An overview of SAL, Proceedings of the 5th NASA Langley Formal Methods Workshop, 2000
  • Grun, Peter and Halambi, Ashok and Khare, Asheesh and Ganesh, Vijay and Dutt, Nikil and Nicolau, Alexandru, EXPRESSION: An ADL for system level design exploration, Department of Information and Computer Science, University of California, Irvine, Technical Report, 1998, 98 - 29
  • Newsham, Zack and Ganesh, Vijay and Fischmeister, Sebastian, Predicting SAT Solver Performance on Heterogeneous Hardware,
  • {i}n, The Meaning of Attack-Resistant Systems,
  • Cadar, Cristian and Ganesh, Vijay and Sasnauskas, Raimondas and Sen, Koushik, Symbolic Execution and Constraint Solving,
  • Zulkoski, Edward and Ganesh, Vijay and Czarnecki, Krzysztof, MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers,
  • Cadar, Christian and Ganesh, Vijay and Sasnauskas, Raimondas and Sen, Koushik and Cadar, Cristian and Ganesh, Vijay and Sasnauskas, Raimondas and Sen, Koushik, Symbolic Execution and Constraint Solving (Dagstuhl Seminar 14442)$}$$}$, Dagstuhl Reports$}$, 4, 98 - 114
  • Khan, Asif and Rayside, Derek and Ganesh, Vijay, Synthesis of Microfluidics Chips using SMT Solvers,
  • Liang, Jia Hui and Ganesh, Vijay and Czarnecki, Krzysztof and Raman, Venkatesh, SAT-based analysis of large real-world feature models is easy, Proceedings of the 19th International Conference on Software Product Line, January 2015, 91 - 100
  • {'i}n, Short Paper: The Meaning of Attack-Resistant Systems, Proceedings of the 10th ACM Workshop on Programming Languages and Analysis for Security, January 2015, 49 - 55
  • Zheng, Yunhui and Zhang, Xiangyu and Ganesh, Vijay, Z3-str: A z3-based string solver for web application analysis, Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, January 2013, 114 - 124
  • Long, Fan and Ganesh, Vijay and Carbin, Michael and Sidiroglou, Stelios and Rinard, Martin, Automatic input rectification, Software Engineering (ICSE), 2012 34th International Conference on, January 2012, 80 - 90
  • Heymans, Patrick and Michel, Raphaël and Ganesh, Vijay and Hubaux, Arnaud and others, An SMT-based Approach to Automated Configuration, 10th International Workshop on Satisfiability Modulo Theories (SMT), January 2012, 107 - 117
  • Jayaraman, Karthick and Ganesh, Vijay and Tripunitara, Mahesh and Rinard, Martin and Chapin, Steve, Automatic error finding in access-control policies, Proceedings of the 18th ACM conference on Computer and communications security, January 2011, 163 - 174
  • Kiezun, Adam and Ganesh, Vijay and Guo, Philip J and Hooimeijer, Pieter and Ernst, Michael D, HAMPI: a solver for string constraints, Proceedings of the eighteenth international symposium on Software testing and analysis, January 2009, 105 - 116
  • Ganesh, Vijay and Leek, Tim and Rinard, Martin, Taint-based directed whitebox fuzzing, Software Engineering, 2009. ICSE 2009. IEEE 31st International Conference on, January 2009, 474 - 484
  • Jayaraman, Karthick and Harvison, David and Ganesh, Vijay and Kiezun, Adam, jFuzz: A Concolic Whitebox Fuzzer for Java., NASA Formal Methods, January 2009, 121 - 125
  • Ganesh, Vijay and Saidi, Hassen and Shankar, Natarajan, Slicing SAL, Computer Science Laboratory, January 1999
  • Zheng, Yunhui and Ganesh, Vijay and Subramanian, Sanu and Tripp, Omer and Dolby, Julian and Zhang, Xiangyu, Effective search-space pruning for solvers of string equations, regular expressions and length constraints, Computer Aided Verification, , 254 manuscript pages
  • Newsham, Zack and Lindsay, William and Ganesh, Vijay and Liang, Jia Hui and Fischmeister, Sebastian and Czarnecki, Krzysztof, SATGraf: Visualizing the Evolution of SAT Formula Structure in Solvers, Theory and Applications of Satisfiability Testing--SAT 2015, , 70 manuscript pages
  • Liang, Jia Hui and Ganesh, Vijay and Zulkoski, Ed and Zaman, Atulan and Czarnecki, Krzysztof, Understanding VSIDS Branching Heuristics in Conflict-Driven Clause-Learning SAT Solvers, Hardware and Software: Verification and Testing, , 241 manuscript pages
  • Newsham, Zack and Ganesh, Vijay and Fischmeister, Sebastian and Audemard, Gilles and Simon, Laurent, Impact of community structure on SAT solver performance, Theory and Applications of Satisfiability Testing--SAT 2014, , 268 manuscript pages
  • Ganesh, Vijay and Minnes, Mia and Solar-Lezama, Armando and Rinard, Martin, Word equations with length constraints: what’s decidable?, Hardware and Software: Verification and Testing, , 226 manuscript pages
  • Ganesh, Vijay and O’donnell, Charles W and Soos, Mate and Devadas, Srinivas and Rinard, Martin C and Solar-Lezama, Armando, Lynx: A programmatic SAT solver for the RNA-folding problem, Theory and Applications of Satisfiability Testing--SAT 2012, , 156 manuscript pages
  • Ganesh, Vijay and Kieżun, Adam and Artzi, Shay and Guo, Philip J and Hooimeijer, Pieter and Ernst, Michael, HAMPI: A string solver for testing, analysis and vulnerability detection, Computer Aided Verification, , 19 manuscript pages
  • Halambi, Ashok and Grun, Peter and Ganesh, Vijay and Khare, Asheesh and Dutt, Nikil and Nicolau, Alex, EXPRESSION: A language for architecture exploration through compiler/simulator retargetability, Design, Automation, and Test in Europe, , 45 manuscript pages
  • Ganesh, Vijay and Dill, David L, A decision procedure for bit-vectors and arrays, Computer Aided Verification, , 531 manuscript pages
  • Berezin, Sergey and Ganesh, Vijay and Dill, David L, An online proof-producing decision procedure for mixed-integer linear arithmetic, Tools and Algorithms for the Construction and Analysis of Systems, , 536 manuscript pages
  • Ganesh, Vijay and Berezin, Sergey and Dill, David L, Deciding Presburger arithmetic by model checking and comparisons with other methods, Formal Methods in Computer-Aided Design, , 186 manuscript pages
  • Ganesh, Vijay and Berezin, Sergey and Dill, David L, Technical Report: A Decision Procedure for Fixed-Width Bit-Vectors, January 2005,
  • Ganesh, Vijay and Berezin, Sergey and Tinelli, Cesare and Dill, David L, Combination results for many sorted theories with overlapping signatures, January 2004,
  • Ganesh, Vijay, Decision procedures for bit-vectors, arrays and integers, January
  • Ganesh, Vijay and Dill, David L, System description of STP, January