Marieke Huisman

Wander Nauta, Marcus Gerhold, Marieke Huisman

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

Marieke Huisman, Raúl E. Monti

With the progress in deductive program verification research, new tools and techniques have become available to support design-by-contract reasoning about non-trivial programs written in widely-used programming languages. However, deductive program verification remains an activity for experts, with ample experience in programming, specification and verification. We would like to change this situation, by developing program verification techniques that are available to a larger audience. In this paper, we present how we developed prototypal program verification support for Snap!. Snap! is a visual programming language, aiming in particular at high school students. We added specification language constructs in a similar visual style, designed to make the intended semantics clear from the look and feel of the specification constructs. We provide support both for static and dynamic verification of Snap! programs. Special attention is given to the error messaging, to make this as intuitive as possible.

Marieke Huisman, Dilian Gurov, Alexander Malkis

For many decades, formal methods are considered to be the way forward to help the software industry to make more reliable and trustworthy software. However, despite this strong belief and many individual success stories, no real change in industrial software development seems to be occurring. In fact, the software industry itself is moving forward rapidly, and the gap between what formal methods can achieve and the daily software-development practice does not appear to be getting smaller (and might even be growing). In the past, many recommendations have already been made on how to develop formal-methods research in order to close this gap. This paper investigates why the gap nevertheless still exists and provides its own recommendations on what can be done by the formal-methods-research community to bridge it. Our recommendations do not focus on open research questions. In fact, formal-methods tools and techniques are already of high quality and can address many non-trivial problems; we do give some technical recommendations on how tools and techniques can be made more accessible. To a greater extent, we focus on the human aspect: how to achieve impact, how to change the way of thinking of the various stakeholders about this issue, and in particular, as a research community, how to alter our behaviour, and instead of competing, collaborate to address this issue.

Stefan Blom, Saeed Darabi, Marieke Huisman

This paper proposes a technique to specify and verify whether a loop can be parallelised. Our approach can be used as an additional step in a parallelising compiler to verify user annotations about loop dependences. Essentially, our technique requires each loop iteration to be specified with the locations it will read and write. From the loop iteration specifications, the loop (in)dependences can be derived. Moreover, the loop iteration specifications also reveal where synchronisation is needed in the parallelised program. The loop iteration specifications can be verified using permission-based separation logic.

Tri Minh Ngo, Marieke Huisman

Quantitative theories of information flow give us an approach to relax the absolute confidentiality properties that are difficult to satisfy for many practical programs. The classical information-theoretic approaches for sequential programs, where the program is modeled as a communication channel with only input and output, and the measure of leakage is based on the notions of initial uncertainty and remaining uncertainty after observing the final outcomes, are not suitable to multi-threaded programs. Besides, the information-theoretic approaches have been also shown to conflict with each other when comparing programs. Reasoning about the exposed information flow of multi-threaded programs is more complicated, since the outcomes of such programs depend on the scheduler policy, and the leakages in intermediate states also contribute to the overall leakage of the program. This paper proposes a novel model of quantitative analysis for multi-threaded programs that also takes into account the effect of observables in intermediate states along the trace. We define a notion of the leakage of a program trace. Given the fact that the execution of a multi-threaded program is typically described by a set of traces, the leakage of a program under a specific scheduler is computed as the expected value of the leakages of all possible traces. Examples are given to compare our approach with the existing approaches.

Marina Zaharieva-Stojanovski, Marieke Huisman, Stefan Blom

This paper describes a way to formally specify the behaviour of concurrent data structures. When specifying concurrent data structures, the main challenge is to make specifications stable, i.e., to ensure that they cannot be invalidated by other threads. To this end, we propose to use history-based specifications: instead of describing method behaviour in terms of the object's state, we specify it in terms of the object's state history. A history is defined as a list of state updates, which at all points can be related to the actual object's state. We illustrate the approach on the BlockingQueue hierarchy from the java.util.concurrent library. We show how the behaviour of the interface BlockingQueue is specified, leaving a few decisions open to descendant classes. The classes implementing the interface correctly inherit the specifications. As a specification language, we use a combination of JML and permission-based separation logic, including abstract predicates. This results in an abstract, modular and natural way to specify the behaviour of concurrent queues. The specifications can be used to derive high-level properties about queues, for example to show that the order of elements is preserved. Moreover, the approach can be easily adapted to other concurrent data structures.