Todd Millstein, professor of computer science in the UCLA Samueli School of Engineering, and his team have won first place for their tool LoopInvGen in the 5th Syntax Guided Synthesis Competition. The competition was part of the FLoC Olympic Games, which brings together mathematical logic and computer science at the 2018 Federated Logic Conference in Oxford, England.
Each tool submitted to this specific competition had to solve the problem of whether a program meets a specification, while overcoming challenges in the program. Tools were awarded a score based on a combination of the number of benchmarks it solved correctly, the time it took to solve them and how concisely it did so. LoopInvGen scored the most points overall and it was also the best tool individually in each of those categories.
LoopInvGen was created by Ph.D. student Saswat Padhi, Millstein and collaborator Rahul Sharma of Microsoft Research. This is the second year in a row that LoopInvGen has won first place in this competition.