FSEN 2025
Mon 7 - Tue 8 April 2025 Västerås, Sweden
Tue 8 Apr 2025 14:30 - 15:30 - Conference session 3 Chair(s): Robbert Jongeling

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.

  • His research interests cover (but are not restricted to) the following areas:
  • Theorem proving and decision procedures, SAT/SMT solving
  • Analysis of programs written in languages like Java, C#, C, C++, Simulink
  • Modeling and analysis of timed/parameterised/concurrent systems
  • Deductive verification, model checking, automatic test case generation
  • Machine learning, automata learning, artificial intelligence, and their application in verification (and vice versa)
  • Embedded systems and software
  • Tue 8 Apr

    Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

    14:30 - 15:30
    Conference session 3Research Papers
    Chair(s): Robbert Jongeling Mälardalen University
    14:30
    60m
    Keynote
    Talk: Verification by Program Transformation
    Research Papers
    Philipp Rümmer University of Regensburg and Uppsala University