Roland Graf
Wissenschaftlicher Mitarbeiter
- E-Mail Adresse: roland.herrmann(at)informatik.uni-regensburg.de (öffnet Ihr E-Mail-Programm)
- Standort: Bajuwarenstr. 4, BA 604
- Wichtige Informationen: Sprechzeiten nach Vereinbarung per Email
- Lehrstuhl für theoretische Informatik
Ich bin Doktorand am Lehrstuhl für Theoretische Informatik unter der Betreuung von Philipp Rümmer. Meinen M.Sc. und meinen B.Sc. in Mathematik habe ich an der Universität Regensburg erworben.
Forschungsinteressen
Ich forsche zu Entscheidungsprozeduren für Array-Theorien mit Aggregationsfunktionen, insbesondere Summen über Arrays. Solche Verfahren bilden die Grundlage von SMT-Solvern, die unter anderem in der automatischen Verifikation von Software eingesetzt werden. Mein Schwerpunkt liegt auf theoretischen Resultaten, vor allem Beweisen zu Entscheidbarkeit und Komplexität dieser Theorien. Zusätzlich evaluiere ich die entwickelten Verfahren praktisch anhand von Prototypen, die perspektivisch in einen SMT-Solver integriert werden sollen.
Publikationen
Konferenzbeiträge
- 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 Parameterized Transition Systems
Roland Herrmann*, Philipp Rümmer
CIAA 2025, LNCS 15981, Springer, 2025, DOI.
Workshopbeiträge
- 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
*Beiträge vor 2026 sind unter dem Namen Roland Herrmann erschienen.
Vorträge und Veranstaltungen
Vorträge
- Solving Arrays With Sums Using LIA* [slides]
Alpine Verification Meeting, Eger, Ungarn, 2026. [POA] - What's Decidable About Arrays With Sums? [slides]
International School on Modeling and Verification of Parallel Processes (MOVEP), Nancy, Frankreich, 2026. - A New Approach for Showing Termination of Parameterized Transition Systems [slides]
Conference on Implementation and Application of Automata (CIAA), Palermo, Italien, 2025. - What's Decidable About Arrays With Sums? [slides]
Conference on Automated Deduction (CADE), Stuttgart, Deutschland, 2025. - A New Approach for Showing Termination of Parameterized Transition Systems [slides]
Alpine Verification Meeting, Freiburg, Deutschland, 2024.
Sommerschulen und Forschungsaufenthalte
- International School on Modeling and Verification of Parallel Processes (MOVEP'26), Nancy, Frankreich, 2026.
- Sommerschule Marktoberdorf (MOD25), Marktoberdorf, Deutschland, 2025.
- Short-Term Scientific Mission (STSM), COST Action CA20111, Host: Prof. Dr. Dilian Gurov, Stockholm, Schweden, 2025, Titel: Array Logic and Aggregation Functions for Program Verification.
Lehre
| WS 2026/2027 | Theoretische Grundlagen der Informatik I, Prof. Dr. Ernst (Übungen) |
| Seminar: Logik, Automaten und Formale Methoden, Prof. Dr. Rümmer (Mitbetreuung) | |
| SS 2026 | Theoretische Grundlagen der Informatik II, Prof. Dr. Rümmer (Übungen) |
| Theoretische Grundlagen der Informatik III, Prof. Dr. Rümmer (Übungen) | |
| WS 2025/2026 | Theoretische Grundlagen der Informatik I, Prof. Dr. Rümmer (Übungen) |
| Seminar: Logik und Automaten, Prof. Dr. Rümmer (Mitbetreuung) | |
| SS 2025 | Logik und Formale Methoden, Prof. Dr. Rümmer (Übungen) |
| Programmieren II, Prof. Dr. Rümmer (Übungen) | |
| WS 2024/2025 | Theoretische Grundlagen der Informatik I, Prof. Dr. Rümmer (Übungen) |
| SS 2024 | Programmieren II, Prof. Dr. Rümmer (Übungen) |
Gutachtertätigkeiten
Gutachter
- Journal of Automated Reasoning (JAR), 2026
Gutachter (Subreviewer)
- CADE 2025
- FroCoS 2025
- FM 2024
- FMCAD 2024