Todd Millstein and his team have won first place for their tool LoopInvGen in the Invariant Synthesis track of the 5th Syntax Guided Synthesis Competition. The competition was part of the FLoC Olympic Games held at the 2018 Federated Logic Conference in Oxford, UK.
LoopInvGen was created by Ph.D. student Saswat Padhi, Professor Todd Millstein, and collaborator Rahul Sharma of Microsoft Research.
In the Invariant Synthesis track each problem consists of a program and a specification, and the goal is to automatically verify that the program meets (or does not meet) the specification. The programs contain loops, which pose a challenge for automated verification as they require the verification tool to generate an appropriate loop invariant—a predicate that accurately captures the behavior of the loop no matter how many times it is executed.
Each tool submitted to the track was awarded a score based on a combination of the number of benchmarks it solved correctly, the time it took to solve them, and the concision of the generated loop invariants. LoopInvGen scored the most points overall, and it also was the best tool individually in each of those categories.
This is the second year in a row that LoopInvGen has won first place in the Invariant Synthesis track.