RESEARCH ACCOMPLISHMENTS AND FUTURE DIRECTIONS
The primary focus of my research is the theory and practice of computer-aided logic reasoning aimed at software engineering, security and mathematics. In this context, I currently lead 4 projects: MapleSAT, The Z3 String Solver, MathCheck, and Attack Resistance. Previously, I led the STP project.
Motivation for Research in Computer-aided Reasoning: Computer-aided logic reasoners are programs that process mathematical formulas symbolically. Examples of such reasoners include Boolean SAT/SMT solvers, computer algebra systems, and proof assistants. These tools have had a deep and sustained impact on many areas of software engineering (SE), security and mathematics. For example, in the last ten years SAT/SMT solvers (e.g., MiniSAT, Z3, STP,...) have enabled many formal verification, testing, program analysis and synthesis techniques. Proof assistants, a la HOL and Coq, are increasingly being used to verify the correctness of mission-critical software. Computer algebra systems or CAS (e.g., Maple, Mathematica,...) have long been used by mathematicians and engineers to symbolically reason about mathematics and mathematical models of myriad kinds of systems. This trend of increasing use of computer-aided reasoners as backends to program analysis, verification and modeling tools will continue unabated as long as problems are modeled using mathematics. Additionally, many of these tools (esp. proof assistants) are now being used by mathematicians to construct proofs for certain long-standing open conjectures (e.g., Kepler conjecture). Finally, while the dramatic impact of these logic tools is reason enough to continue research on the topic, an additional important reason is the sheer intellectual challenge of figuring out the limits of automation of mathematics. This quest started with the work of many logicians, perhaps most importantly David Hilbert. While we know from Godel's and Turing's work that "automating mathematics using computers is impossible in general", we have nonetheless made significant progress thanks to sound heuristics and techniques developed by thousands of scientists.
Research Questions that Interest me Most: Question 1) How can we better assist mathematicians prove theorems using computer-aided reasoners? This remains a perennial question in the field. However, it takes new meaning given that now we have three distinct well-developed classes of computer-aided reasoning tools today, namely, SAT/SMT solvers, proof assistants, and CAS, that efficiently address different aspects symbolic computation. SAT/SMT solvers are good at proof search, proof assistants at proof construction, and CAS encode a lot of domain-knowledge about different branches of mathematics. In addition, we have well-developed machine-learning techniques that can be used for concept search. An immediate question then is whether there is a way to combine these classes of tools (i.e., SAT/SMT solvers, proof assistants, CAS, and machine-learning techniques) such that they compensate for the weakness of the other, and better assist mathematicians in proving theorems or counterexampling conjectures. Question 2) the second big question relates to the efficiency of Boolean SAT solvers. It is well-know that certain kinds of SAT solvers (to be precise, the conflict-driven clause-learning variety) work incredibly efficiently in practice for industrial applications, even though the problem they address, namely, Boolean satisfiability is NP-complete and is believed to be intractable in general. It would be very useful to understand why this is so, bridging the gap between theory and practice. Question 3) the third question relates to a universal template for the construction of mathematical logic-reasoning software. Is there a universal template for creating effective logic-reasoning software, and if so can we characterize it algorithmically and analyze it using ideas from parameterized complexity theory. Question 4) finally, applications are the drivers of research in this field. In the past, logic reasoners enabled many new classes of applications, including, but not limited to, symbolic-execution based analysis, model-checking, and formal verification of proofs and software. Can we build on this success and find new sets of applications in SE, security and mathematics that can be enabled using logic-reasoning software? My current research goals are to answer the above 4 questions. Below I list my past accomplishments, followed by how I am addressing some of these questions.
My Most Significant Contributions: As part of my research so far, I have designed many solvers, the most impactful among them being STP [2,8] that played an important role in the development of symbolic-execution based testing. STP was developed as part of the EXE tool [1,8] (a predecessor of the KLEE symbolic analysis engine [8]), recognized by many as a fundamental breakthrough in SE. Today STP is the foundation for many testing (e.g., KLEE, S2E), program analysis (e.g., BitBlaze, WebBlaze), and exploit construction tools (e.g., AEG). I also designed new solvers for theories of strings, e.g., HAMPI [3,8] and Z3-str [6], used in solving constraints derived from security applications such as vulnerability detection (e.g., Ardilla). My solvers not only enabled applications, but also influenced the design of other solvers (e.g., Boolector [4]). STP, HAMPI, and Z3str2 are currently in use in more than 100 research projects in academia and industry. Additionally, I solved theoretical questions regarding the undecidability of the satisfiability problem for certain theories over strings [7]. More recently, my student Ed Zulkoski and I built a new math assistant, we call MathCheck, that combines a SAT solver with a CAS system to resolve open mathematical conjectures in graph theory. In the future, we plan to extend MathCheck to address questions in number theory and algebra. Additionally, the problem that I am currently very interested in is "why are SAT solvers so efficient for industrial instances?". Towards resolving this question, my student Zack Newsham, collaborators, and I showed that community structure of SAT instances strongly influences the performance of SAT solvers. Another step towards resolving this question relates to understanding the internals of SAT solvers. Towards this end, my student Jimmy Liang, collaborators, and I have provided the first comprehensive understanding of effective branching heuristics (a la VSIDS and its variants) in SAT solvers. Finally, I continue to be interested in solvers designed specifically for applications in SE and security such as concolic testing, exploit construction, formal verification and program analysis. With my student Yunhui Zheng (now at IBM Research), and collaborators, I am extending the string solver Z3-str to support program analysis of Web applications written in JavaScript. Below, I describe in more detail some of these recent contributions.
Current and Future Directions: More recently, my focus has been a problem that has stumped both theoreticians and practitioners alike, namely, "why are Boolean SAT solvers so efficient for large industrial instances even though the Boolean SAT problem is NP-complete?". Towards this goal, I posed three sub-questions. First, can we characterize the structure of industrial instances and their impact on solver performance? Second, can we mathematically model the essential aspects of SAT solvers? Finally, can we use complexity theory to link the structure of industrial instances with the proposed model?
For the first question regarding structure, my collaborators and I showed that industrial instances can be characterized as graphs that have lots of clusters, aka communities, in them, and that the community structure of SAT instances strongly correlate with solver performance [5]. The idea of communities in graphs arose in the study of complex networks in physics. Informally, a community in a graph is a sub-graph with relatively more internal edges than external. We say a Boolean formula has good community structure if it has many small clusters with few inter-community edges, and has bad community structure if it has big clusters with lots of inter-community edges. We showed a strong correlation between the running time of SAT solvers and community structure of input formulas, and that industrial instances have good community structure. My collaborators and I are working on some tantalizing answers to the second and third questions above. One potential answer is the idea that SAT solvers can be characterized as a feedback machine, wherein, the branching heuristic is like a "student" that learns inductively, and boolean constant propagation + conflict analysis is like a "teacher" that provides corrective feedback deductively. Researchers in machine learning and AI have studied similar feedback machines, and we are attempting to use their analysis techniques in the SAT context to better understand the SAT solver algorithm.
In conclusion, the primary impact of my research has been in developing logic-reasoning techniques and applying them to SE, especially symbolic execution-based analysis and testing. I plan to deepen my work and continue developing logic-reasoning for SE and security, and broaden the scope of automated logic-reasoners to mathematics. I am currently working on a novel prover for graph and number theory that is built along a “student-teacher with feedback” prover architecture. This prover combines SAT solvers (the inductive student) with a computer algebra system (the deductive teacher, e.g., SAGE, Maple, Mathematica). Such an architecture brings together the best of combinatorial search with domain-specific knowledge. It is increasingly clear that provers are coming of age and will impact mathematics in fundamental ways. I hope to leverage my understanding of computer-aided logic-reasoning techniques in service of this unprecedented opportunity to influence mathematical practice.
REFERENCES
[1] Cristian Cadar, Vijay Ganesh, Peter Pawlowski, David Dill, Dawson Engler. EXE: Automatically Generating Inputs of Death. CCS 2006.
[2] Vijay Ganesh and David L. Dill. A Decision Procedure for Bit-vector and Arrays. CAV 2007.
[3] Vijay Ganesh, Adam Kiezun, Shay Artzi, Philip Guo, Pieter Hooimiejer and Michael Ernst. HAMPI: A String Solver for Testing, Analysis and Vulnerability Detection. CAV 2011.
[4] Robert Brummayer and Armin Biere. An Efficient Decision Procedure for Bit-vectors and Arrays. TACAS 2009.
[5] Zack Newsham, Vijay Ganesh, Sebastian Fischmeister, Gilles Audemard, and Laurent Simon. Impact of Community Structure on SAT Solver Performance. SAT 2014.
[6] Yunhui Zheng, Xiangyu Zhang, and Vijay Ganesh. Z3-str: A Z3-base String Solver for Web Application Analysis. FSE 2013.
[7] Vijay Ganesh, Mia Minnes, Armando Solar-Lezama, Martin Rinard. Word Equations with Length Constraints: What’s Decidable? HVC 2012.
[8] Saswat Anand. List of important papers in symbolic-execution based testing and analysis. (Also on Google Sites)