Skip to main content
University of Regensburg
DE: diese Seite auf deutsch

Roland Graf

Roland Graf

PhD Student

Further info of Roland Graf

I am a PhD student at the Chair of Theoretical Computer Science, supervised by Philipp Rümmer. I obtained my MSc and BSc in Mathematics at the University of Regensburg.

Research interests

My research focuses on decision procedures for array theories with aggregation functions, in particular sums over arrays. Such procedures form the basis of SMT solvers, which are used, amongst other things, in the automatic verification of software. My focus is on theoretical results, particularly proofs concerning the decidability and complexity of these theories. In addition, I evaluate the developed methods in practice using prototypes, which are intended to be integrated into an SMT solver in the future.

Publications

Conference papers

  • What's Decidable About Arrays With Sums? 
    Roland Herrmann*, Philipp Rümmer
    CADE 30 (CADE 2025), LNCS 15943, Springer, 2025, DOI.
  • A New Approach for Showing Termination of Parameterised Transition Systems
    Roland Herrmann*, Philipp Rümmer
    CIAA 2025, LNCS 15981, Springer, 2025, DOI.

Workshop papers

  • An Eager Encoding of Array Summation Constraints
    Patrick Janoschek, Roland Herrmann*, Philipp Rümmer
    SMT 2026
  • Verification of E-Voting Algorithms in Dafny
    Robert Büttner, Fabian Franz Dießl, Patrick Janoschek, Ivana Kostadinovic, Henrik Oback, Kilian Voß, Franziska Alber, Roland Herrmann*, Sibylle Möhle, Philipp Rümmer
    Dafny 2026,     ArXiv

*Papers published before 2026 appeared under the name Roland Herrmann.

Talks and Events

Talks

  • Solving Arrays With Sums Using LIA* [slides]
    Alpine Verification Meeting, Eger, Hungary, 2026. [POA]
  • What is Decidable About Arrays with Sums? [slides]
    International School on Modelling and Verification of Parallel Processes (MOVEP), Nancy, France, 2026.
  • A New Approach for Showing Termination of Parameterised Transition Systems [slides]
    Conference on Implementation and Application of Automata (CIAA), Palermo, Italy, 2025.
  • What's Decidable About Arrays With Sums? [slides]
    Conference on Automated Deduction (CADE), Stuttgart, Germany, 2025.
  • A New Approach for Showing Termination of Parameterised Transition Systems [slides]
    Alpine Verification Meeting, Freiburg, Germany, 2024.

Summer Schools and Research Stays

  • International School on Modelling and Verification of Parallel Processes (MOVEP’26), Nancy, France, 2026.
  • Marktoberdorf Summer School (MOD25), Marktoberdorf, Germany, 2025.
  • Short-Term Scientific Mission (STSM), COST Action CA20111, Host: Prof. Dr Dilian Gurov, Stockholm, Sweden, 2025, Title: Array Logic and Aggregation Functions for Program Verification.

Teaching

Winter Term 2026/2027Introduction to Theoretical Computer Science I, Prof. Dr. Ernst (tutorials)
Seminar: Logic, Automata and Formal Methods, Prof. Dr. Rümmer (co-supervision)
Summer Term 2026Theoretical Computer Science II, Prof. Dr. Rümmer (tutorials)
Theoretical Computer Science III, Prof. Dr. Rümmer (tutorials)
Winter Term 2025/2026Introduction to Theoretical Computer Science I, Prof. Dr. Rümmer (tutorials)
Seminar: Logic and Automata, Prof. Dr. Rümmer (co-supervision)
Summer Term 2025Logic and Formal Methods, Prof. Dr. Rümmer (tutorials)
Programming II, Prof. Dr. Rümmer (tutorials)
Winter Term 2024/2025Introduction to Theoretical Computer Science I, Prof. Dr. Rümmer (tutorials)
Summer Term 2024Programming II, Prof. Dr. Rümmer (tutorials)

Expert assessment work

Reviewer

  • Journal of Automated Reasoning (JAR), 2026

Subreviewer

  • CADE 2025
  • FroCoS 2025
  • FM 2024
  • FMCAD 2024

Publications

To top