VLDB 2026 Research / reviewers in the wild / expert
Roland Herrmann
dblp:253/0970
· DBLP profile ↗
2ranked-venue papers
2as first author
2since 2021 · last 2025
0009-0003-5748-7921ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 2 · 2 first-author · 2 since 2021Artificial intelligence and machine learning · 1 · 1 first-author · 1 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | What's Decidable About Arrays With Sums?abstractAbstract The theory of arrays, supported by virtually all SMT solvers, is one of the most important theories in program verification. The standard theory of arrays, which provides read and write operations, has been extended in various different ways in past research, among others, by adding extensionality, constant arrays, function mapping (resulting in combinatorial array logic), counting, and projections. This paper studies array theories extended with sum constraints, which capture properties of the sum of all elements of an integer array. The paper shows that the theory of extensional arrays extended with constant arrays and sum constraints can be decided in non-deterministic polynomial time. The decision procedure works both for finite and infinite index sorts, as long as the cardinality is fixed a priori. In contrast, adding sum constraints to combinatorial array logic gives rise to an undecidable theory. The paper concludes by studying several fragments in between standard arrays with sums and combinatorial arrays with sums, aiming at providing a complete characterization of decidable and undecidable fragments. Roland Herrmann, Philipp Rümmer |
CADE | 1 |
| 2025 | A New Approach for Showing Termination of Parameterized Transition Systems
Roland Herrmann, Philipp Rümmer |
CIAA | 1 |