Roland Herrmann

dblp:253/0970 · DBLP profile ↗
← Back
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
YearPublicationVenuePosition
2025 What's Decidable About Arrays With Sums?
abstract
Abstract 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
CADE1
2025 A New Approach for Showing Termination of Parameterized Transition Systems
Roland Herrmann, Philipp Rümmer
CIAA1