ABSTRACT. When developing file systems, caching is a common technique to achieve a performant implementation. Integrating write-back caches into a file system does not only affect functional correctness but also impacts crash safety properties of the file system. As parts of written data are only stored in volatile memory, special care has to be taken when integrating write-back caches to guarantee that a power cut during running operations leads to a consistent state. This paper shows how non-order-preserving caches can be added to a virtual file system switch (VFS) and gives a novel crash-safety criterion matching the characteristics of such caches. Broken down to individual files, a power cut can be explained by constructing an alternative run, where all writes since the last synchronization of that file have written a prefix. VFS caches have been integrated modularly into Flashix, a verified file system for flash memory, and both functional correctness and crash-safety of this extension have been verified with the interactive theorem prover KIV.

ABSTRACT. In this feasibility study we discuss reasoning about the correctness of Java interfaces using histories, with a particular application to Java's Collection interface. We introduce a new specification method (in the KeY theorem prover) using histories, that record method invocations and their parameters on an interface. We outline the challenges of proving client code correct with respect to arbitrary implementations, and describe a practical specification and verification effort of part of the Collection interface using KeY (including source and video material)

ABSTRACT. Active objects extend the Actor paradigm with structured communication using method calls and futures. Active objects are, like actors, known to be data race free. Both are inherently concurrent, as they share a fundamental decoupling of communication and synchronisation. Both encapsulate their state, restricting access to one process at a time. Clearly, this rules out low-level races between two processes accessing a shared variable. But is that sufficient to guarantee deterministic results from the execution of an active object program?

In this paper we are interested in so-called high-level races caused by the fact that the arrival order of messages between active objects can be non-deterministic, resulting in non-deterministic overall behaviour. We study this problem in the setting of a core calculus and identify restrictions on active object programs which are sufficient to guarantee deterministic behaviour for active object programs. We formalise these restrictions as a simple extension to the type system of the calculus and prove that well-typed programs exhibit deterministic behaviour.

ABSTRACT. Dataflow test coverage criteria, such as all-defs and all-uses, belong to the most advanced coverage criteria. These criteria are defined by complex artifacts combining variable definitions, uses and program paths. Detection of infeasible (or more generally, polluting) test objectives for such criteria is a particularly challenging task. This short paper evaluates three detection approaches involving dataflow analysis, value analysis and weakest precondition calculus. We compare these approaches, analyze their detection capacities and propose a methodology for their efficient combination. Initial experiments illustrate the benefits of the proposed approach.

ABSTRACT. We consider the problem of estimating the numerical accuracy of programs with operations in fixed-point arithmetic and variables of arbitrary, mixed precision, and possibly non-deterministic value. By applying a set of parameterised rewrite rules, we transform the relevant fragments of the program under consideration into sequences of operations in integer arithmetic over vectors of bits, thereby reducing the problem as to whether the error enclosures in the initial program can ever exceed a given order of magnitude to simple reachability queries on the transformed program. We present a preliminary experimental evaluation of our technique on a particularly complex industrial case study.

ABSTRACT. When targeting modern parallel hardware architectures, constructing correct and high-performing software is complex and time-consuming. In particular, reorderings of memory accesses that violate intended sequentially consistent behaviour are a major source of bugs. Applying synchronisation mechanisms to repair these should be done sparingly, as they negatively impact performance.

In the past, both static analysis approaches and techniques based on explicit-state model checking have been proposed to identify where synchronisation fences have to be placed in a program. The former are fast, but the latter more precise, as they tend to insert fewer fences. Unfortunately, the model checking techniques suffer a form of state space explosion that is even worse than the traditional one.

In this work, we propose a technique using a combination of state space exploration and static analysis. This combination is in terms of precision comparable to purely model checking-based techniques, but it reduces the state space explosion problem to the one typically seen in model checking. Furthermore, experiments show that the combination frequently outperforms both purely model checking and static analysis techniques. In addition, we have added the capability to check for atomicity violations, which is another major source of bugs.

ABSTRACT. We describe a new approach to synthesizing a timed automaton from a set of timed scenarios. The set of scenarios specifies a set of behaviours, i.e., sequences of events that satisfy the time constraints imposed by the scenarios. The language of the constructed automaton is equivalent to that set of behaviours. Every location of the automaton appears in at least one accepting run, and its graph is constructed so as to minimise the number of clocks. The construction allows a particularly efficient clock allocation algorithm.

ABSTRACT. Sorting is one of the fundamental operations in computer science, and many sequential and parallel algorithms have been proposed in the literature. Swap-based sorting algorithms are one category of sorting algorithms where elements are swapped repeatedly to achieve the desired order. Since these algorithms are widely used in practice, their (functional) correctness, i.e., proving sortedness and permutation properties, is of the utmost importance. However, proving the permutation property using automated program verifiers is much more challenging as the formal definition of this property involves existential quantifiers. In this paper, we propose a generic pattern to verify the permutation property for any sequential and parallel swap-based sorting algorithm automatically. To demonstrate our approach, we use VerCors, a verification tool based on separation logic for concurrent and parallel programs, to verify the permutation property of bubble sort, selection sort, insertion sort, parallel odd-even transposition sort, quick sort, two in-place merge sorts and TimSort for any arbitrary size of input.

ABSTRACT. We develop a complementation procedure and an equivalence checker for nondeterministic Büchi automata. Both are formally verified using the proof assistant Isabelle/HOL. The verification covers everything from the abstract correctness proof down to the generated SML code. The complementation follows the rank-based approach. We formalize the abstract algorithm and use refinement to derive an executable implementation. In conjunction with an intersection operation and an emptiness check, this enables deciding language-wise equivalence between nondeterministic Büchi automata. We also improve and extend our library for transition systems and automata presented in previous research. Finally, we develop a command-line executable providing complementation and equivalence checking as a verified reference tool. It can be used to test the output of other, unverified tools. We also include some tests that demonstrate that its performance is sufficient to do this in practice.

ABSTRACT. Many formal verification techniques rely on the concept of system state and base the formalism on transitions between such states. In many systems, however, the concept of system state is poorly defined, particularly for parallel and distributed systems and for cyber-physical systems. In physics, the state of a system depends on the observer, and it is rare for a formal verification framework to clearly define what is an observer. In this talk, I will illustrate this problem with variants of the actor model, which is widely used for developing parallel and distributed software. I will focus on a more deterministic version of the actor model called Reactors (and an implementation language called Lingua Franca) and show that scalability of model checking depends heavily on how one defines the observer.