Vijay's primary area of research is the theory and practice of SAT/SMT solvers, and their application in AI, software engineering, security, mathematics, and physics. In this context he has led the development of many SAT/SMT solvers, most notably, STP, Z3str4, AlphaZ3, MapleSAT, and MathCheck. He has also proved several decidability and complexity results in the context of first-order theories. More recently he has started working on topics at the intersection of learning and reasoning, especially the use of machine learning for efficient solvers, and the use of solvers aimed at making AI more trustworthy, secure, and robust. For his research, Vijay has won over 30 awards, honors, and medals to-date, including an ACM Impact Paper Award at ISSTA 2019, ACM Test of Time Award at CCS 2016, and a Ten-Year Most Influential Paper citation at DATE 2008.