Award-winning Software Tool Uses Innovative Approach

School of Computer Science Professor Vijay Ganesh is leading the way in the innovation of SMT solvers, a class of tools key to software engineering, security, and trustworthy artificial intelligence (AI).

Ganesh and his student, John Lu, have been working on their own solver, Z3-alpha, for several years. It recently won several categories at SMT-COMP 2024, a competition held to determine the best solvers from around the world.

SMT solvers are automated logical reasoning tools used widely to test and analyze programs. They are also used to identify potential security issues.

“SMT solvers are like a Swiss Army Knife for all kinds of tasks for software engineering and trustworthy AI. You need a tool that can understand and analyze formulas obtained from analysis of programs,” Ganesh said.

The Z3-alpha solver is derived from the z3 solver from Microsoft Research, but Ganesh and Lu implemented machine learning (ML) into their solver to automatically synthesize strategies, making it more efficient.

Ganesh said the solver illustrates one of his biggest research goals: effectively combining the fields of automated reasoning and ML.

“With this solver, we’re using ML to make automated reasoning more efficient. In another line of research, we are going in the reverse direction by using automated reasoning to analyze, test, and improve ML models,” he said.

Using ML with SMT solvers this way is a relatively new line of research that Ganesh has been working on. He said this is among the first known instances of the successful use of machine learning for SMT solver strategy synthesis.

Ganesh said they want to work to further improve the Z3-alpha solver and apply these ML techniques to other solvers.