On December 5, 2022, TU Wien Informatics researchers Daneshvar Amrollahi, Marcel Moosbrugger and Miroslav Stankovic were awarded the Radhia Cousot Young Researcher Best Paper Award at the 29th Static Analysis Symposium (SAS 2022) in Auckland, New Zealand. They received the award for their paper Solving Invariant Generation for Unsolvable Loops, a joint work with their collaborators Ezio Bartocci, George Kenison, and Laura Kovács.

Daneshvar Amrollahi was part of the Probabilistic Invariant Generation (ProbInG) project at the Automated Program Reasoning (APRe) group at TU Wien Informatics from July 2021 to February 2022. Marcel Moosbrugger, graduate of our Bachelor with Honors Excellence program, and Miroslav Stankovic are both PreDocs at the Formal Methods in Systems Engineering Research Unit.

Abstract

Automatically generating invariants, key to computer-aided analysis of probabilistic and deterministic programs and compiler optimisation, is a challenging open problem. Whilst the problem is in general undecidable, the goal is settled for restricted classes of loops. For the class of solvable loops, introduced by Kapur and Rodríguez-Carbonell in 2004, one can automatically compute invariants from closed-form solutions of recurrence equations that model the loop behaviour. In this paper we establish a technique for invariant synthesis for loops that are not solvable, termed unsolvable loops. Our approach automatically partitions the program variables and identifies the so-called defective variables that characterise unsolvability. We further present a novel technique that automatically synthesises polynomials, in the defective variables, that admit closed-form solutions and thus lead to polynomial loop invariants. Our implementation and experiments demonstrate both the feasibility and applicability of our approach to both deterministic and probabilistic programs.

About the Radhia Cousot Young Researcher Best Paper Award

Starting in 2014, the program committee of each SAS conference selects a paper for the Radhia Cousot Young Researcher Best Paper Award, in memory of Radhia Cousot and her fundamental contributions to static analysis, as well as being one of the main promoters and organizers of the SAS series of conferences.

About the Static Analysis Symposium

Static Analysis is increasingly recognized as a fundamental tool for program verification, bug detection, compiler optimization, program understanding, and software maintenance. The series of International Static Analysis Symposia (SAS) serves as the primary venue for presentation of theoretical, practical, and application advances in the area.

Curious about our other news? Subscribe to our news feed, calendar, or newsletter, or follow us on social media.