Heike Wehrheim

TACAS Conference 2026 Conference Paper

jMT: Testing Correctness of Java Memory Models

• Lukas Panneke
• Heike Wehrheim

FM Conference 2026 Conference Paper

Towards Proving Liveness on Weak Memory

• Lara Bargmann
• Heike Wehrheim

Abstract Reasoning about concurrent programs executed on weak memory models is an inherently complex task. So far, existing proof calculi for weak memory models only cover safety properties. In this paper, we provide the first proof calculus for reasoning about liveness. Our proof calculus is based on Manna and Pnueli’s proof rules for response under weak fairness, formulated in linear temporal logic. Our extension includes the incorporation of memory fairness into rules as well as the usage of ranking functions defined over weak memory state. We have applied our reasoning technique to the Ticket lock algorithm and have proved it to guarantee starvation freedom under memory models Release-Acquire and Strong Coherence for any number of concurrent threads.

FormaliSE Conference 2025 Conference Paper

Detecting Redundant Preconditions

• Nicola Thoben
• Heike Wehrheim

Software specifications often come in the form of contracts, detailing in particular pre- and postconditions of functions, libraries or modules. Research on contracts often centers around questions of contract inference or contract validation. In this paper, we study the less investigated aspect of quality of contracts. More specifically, we define the concept of redundancy for preconditions and propose three techniques with differing efficiency and effectiveness for detecting redundant preconditions. All three techniques are implemented within a software verification tool, and we present results of an experimental evaluation on a dataset of more than 60 C programs. The results confirm differences in precision and resource consumption of the techniques but also reveal unexpected outcomes about the completeness of the most precise, predicate analysis based technique.

FormaliSE Conference 2022 Conference Paper

Property-Driven Testing of Black-Box Functions

• Arnab Sharma
• Vitalik Melnikov
• Eyke Hüllermeier
• Heike Wehrheim

Testing is one of the most frequent means of quality assurance for software. Property-based testing aims at generating test suites for checking code against user-defined properties. Test input generation is, however, most often independent of the property to be checked, and is instead based on random or user-defined data generation. In this paper, we present property-driven unit testing of functions with numerical inputs and outputs. Alike property-based testing, it allows users to define the properties to be tested for. Contrary to property-based testing, it also uses the property for a targeted generation of test inputs. Our approach is a form of learning-based testing where we first of all learn a model of a given black-box function using standard machine learning algorithms, and in a second step use model and property for test input generation. This allows us to test both predefined functions as well as machine learned regression models. Our experimental evaluation shows that our property-driven approach is more effective than standard property-based testing techniques.

TCS Journal 2005 Journal Article

Slicing techniques for verification re-use

• Heike Wehrheim

In this paper we discuss which properties of a formally verified component are preserved when the component is changed due to an adaption to a new use. More specifically, we will investigate when a temporal logic property of an Object-Z class is preserved under a modification or extension of the class with new features. To this end, we use the slicing technique from program analysis which provides us with a representation of the dependencies within the class in the form of a program dependence graph. This graph can be used to determine the effect of a change to the class's behaviour and thus to the validity of a temporal logic formula.

MFCS Conference 1997 Conference Paper

Dependency-Based Action Refinement

• Arend Rensink
• Heike Wehrheim

Abstract Action refinement in process algebras has been widely studied in the last few years as a means to support top-down design of systems. A specific notion of refinement arises when a dependency relation on the actions (in the Mazurkiewicz sense) is used to control the inheritance of orderings from the abstract level. In this paper we present a rather simple operational semantics for dependency-based action refinement. We show the consistency of the operational with a (previously published) denotational semantics. We moreover show that bisimulation is a congruence for dependency-based refinement. Finally, we give an illustrative example.

MFCS Conference 1996 Conference Paper

Causal Testing

• Ursula Goltz
• Heike Wehrheim

Abstract We suggest an equivalence notion for event structures as a semantic model of concurrent systems. It combines the notion of testing (or failure) equivalence with respect to the timing of choices between different executions with a precise account of causalities between action occurrences as in causal semantics. This fills an open gap in the lattice of equivalences considered in comparative concurrency semantics. We show that our notion coincides with a “canonical” equivalence obtained as the usual testing performed on causal trees. Furthermore, we show that it is invariant under action refinement, thus fulfilling a standard criterion for non-interleaving equivalences.