In deductive verification and software model checking, dealing with certain language constructs can be problematic when the back-end solver is not sufficiently powerful or lacks the required theories. This applies, in particular, to the concept of extended quantifiers found in specification languages like JML and ACSL. Extended quantifiers can be used to compute, among others, the maximum element or the sum of elements of an array and are frequently used in specifications, but tend to be difficult to support in verification tools. In the talk, I will present our ongoing research on how to automatically transform programs with such complicated operators to equivalent programs not containing the operators, and to reason about the correctness of those simpler programs instead. We apply our framework to cover the different kinds of extended quantifiers, which we formalize as monoid homomorphisms. Our approach is generic, however, and can be applied to describe a wide range of program transformations.

The presentation is based on joint work with Jesper Amilon, Zafer Esen, Dilian Gurov, Christian Lidström, Marten Voorberg.

Philipp Rümmer is a professor of theoretical Computer Science at the University of Regensburg. He also hold a position as Senior Lecturer at the Department of Information Technology, Uppsala University.