arXiv subjects

Marcus Gerhold

Publications and source records attributed to Marcus Gerhold.

7 recordsLinked to original sources

arXiv2026

Crash-free Deductive Verifiers

As deductive verifiers mature, their potential user base is growing from the initial core developers to other users. To convince external users of the suitability of verifiers, these tools must run reliably out of the box, give meaningful error messages and display correct results. Yet deductive verifiers are large and complex software systems and their own full verification is often out of reach. We therefore need complementary means to provide such guarantees. This paper advocates the use of fuzzing as a practical way to improve the quality and robustness of deductive verifiers. We outline how fuzz testing can be applied to deductive verifiers, and demonstrate the idea with the prototype tool AValAnCHE, which is integrated with the VerCors verifier. We report on our experiments in which AValAnCHE uncovered several issues in VerCors and demonstrate that the approach also works for other deductive verifiers

cs.SE↗

arXiv2025

Embeddings of Weighted Morrey Spaces

In this master thesis we recall already established definitions and basic properties of classical Morrey spaces in an attempt to expand known facts to their weighted counterparts. To do so, we will recall properties of Muckenhoupt weights, which we will use to derive further properties of weighted Morrey spaces. We will also show the boundedness of the Hardy-Littlewood maximal operator on weighted Morrey spaces. Throughout this thesis we will have a look at example weights and show in which case Morrey spaces equipped with these weights are embedded in each other.

math.FA↗

arXiv2025

Entropy-, Approximation- and Kolmogorov Numbers on Quasi-Banach Spaces

In this bachelor's thesis we introduce three quantities for linear and bounded operators on quasi-Banach spaces which are entropy numbers, approximation numbers and Kolmogorov numbers. At first we establish the three quantities with some basic properties and try to modify known content from the Banach space case. We compare each one of them, with the corresponding other two and give estimates concerning the mean values and limits. As an example, we analyze the identity operator between finite dimensional $\ell_{p}$ spaces $\mbox{id : }\left(\ell_{p}^{n}\rightarrow\ell_{q}^{n}\right)$ for $0<p,q\leq\infty$ and give sharp estimates for entropy numbers. Furthermore we add some known estimates for approximation numbers and Kolmogorov numbers. At last we examine some renowned connections of these quantities to spectral theory on infinite dimensional Hilbert spaces, which are the inequality of Carl and the inequality of Weyl.

math.FA↗

arXiv2025

Time for Quiescence: Modelling quiescent behaviour in testing via time-outs in timed automata

Model-based testing (MBT) derives test suites from a behavioural specification of the system under test. In practice, engineers favour simple models, such as labelled transition systems (LTSs). However, to deal with quiescence - the absence of observable output - in practice, a time-out needs to be set to conclude observation of quiescence. Timed MBT exists, but it typically relies on the full arsenal of timed automata (TA). We present a lifting operator $\chi^{\scriptstyle M}\!$ that adds timing without the TA overhead: given an LTS, $\chi^{\scriptstyle M}\!$ introduces a single clock for a user chosen time bound $M>0$ to declare quiescence. In the timed automaton, the clock is used to model that outputs should happen before the clock reaches value $M$, while quiescence occurs exactly at time $M$. This way we provide a formal basis for the industrial practice of choosing a time-out to conclude quiescence. Our contributions are threefold: (1) an implementation conforms under $\mathbf{ioco}$ if and only if its lifted version conforms under timed $\mathbf{tioco_M}$ (2) applying $\chi^{\scriptstyle M}\!$ before or after the standard $\mathbf{ioco}$ test-generation algorithm yields the same set of tests, and (3) the lifted TA test suite and the original LTS test suite deliver identical verdicts for every implementation.

cs.FL↗

arXiv2023

Reproduction Report for SV-COMP 2023

The Competition on Software Verification (SV-COMP) is a large computational experiment benchmarking many different software verification tools on a vast collection of C and Java benchmarks. Such experimental research should be reproducible by researchers independent from the team that performed the original experiments. In this reproduction report, we present our recent attempt at reproducing SV-COMP 2023: We chose a meaningful subset of the competition and re-ran it on the competition organiser's infrastructure, using the scripts and tools provided in the competition's archived artifacts. We see minor differences in tool scores that appear explainable by the interaction of small runtime fluctuations with the competition's scoring rules, and successfully reproduce the overall ranking within our chosen subset. Overall, we consider SV-COMP 2023 to be reproducible.

cs.LO↗

arXiv2017

A Hierarchy of Scheduler Classes for Stochastic Automata

Stochastic automata are a formal compositional model for concurrent stochastic timed systems, with general distributions and non-deterministic choices. Measures of interest are defined over schedulers that resolve the nondeterminism. In this paper we investigate the power of various theoretically and practically motivated classes of schedulers, considering the classic complete-information view and a restriction to non-prophetic schedulers. We prove a hierarchy of scheduler classes w.r.t. unbounded probabilistic reachability. We find that, unlike Markovian formalisms, stochastic automata distinguish most classes even in this basic setting. Verification and strategy synthesis methods thus face a tradeoff between powerful and efficient classes. Using lightweight scheduler sampling, we explore this tradeoff and demonstrate the concept of a useful approximative verification technique for stochastic automata.

cs.LO↗

arXiv2015

Ioco Theory for Probabilistic Automata

Model-based testing (MBT) is a well-known technology, which allows for automatic test case generation, execution and evaluation. To test non-functional properties, a number of test MBT frameworks have been developed to test systems with real-time, continuous behaviour, symbolic data and quantitative system aspects. Notably, a lot of these frameworks are based on Tretmans' classical input/output conformance (ioco) framework. However, a model-based test theory handling probabilistic behaviour does not exist yet. Probability plays a role in many different systems: unreliable communication channels, randomized algorithms and communication protocols, service level agreements pinning down up-time percentages, etc. Therefore, a probabilistic test theory is of great practical importance. We present the ingredients for a probabilistic variant of ioco and define the πoco relation, show that it conservatively extends ioco and define the concepts of test case, execution and evaluation.

cs.LO↗