This paper addresses the problem of verifying and correcting programs when they are moved from a sequential consistency execution environment to a relaxed memory context. Specifically, it considers the PSO (Partial Store Order) memory model, which corresponds to the use of a store buffer for each shared variable and each process. We also will consider, as an intermediate step, the TSO (Total Store Order) memory model, which corresponds to the use of one store buffer per process. The proposed approach extends a previously developed verification tool that uses finite automata to symbolically represent the possible contents of the store buffers. Its starting point is a program that is correct for the usual Sequential Consistency (SC) memory model, but that might be incorrect under PSO with respect to safety properties. This program is then first analyzed and corrected for the TSO memory model, and then this TSO-safe program is analyzed and corrected under PSO, producing a PSO-safe program. To obtain a TSO-safe program, only store-load fences (TSO only allows store-load relaxations) are introduced into the program. Finaly, to produce a PSO-safe program, only store-store fences (PSO additionally allows store-store relaxations) are introduced. An advantage of our technique is that the underlying symbolic verification tool makes a full exploration of program behaviors possible even for cyclic programs, which makes our approach broadly applicable. The method has been tested with an experimental implementation and can effectively handle a series of classical examples.

Checking infinite-state systems is frequently done by encoding infinite sets of states as regular languages. Computing such a regular representation of, say, the set of reachable states of a system requires acceleration techniques that can finitely compute the effect of an unbounded number of transitions. Among the acceleration techniques that have been proposed, one finds both specific and generic techniques. Specific techniques exploit the particular type of system being analyzed, for example, a system manipulating queues or integers, whereas generic techniques only assume that the transition relation is represented by a finite-state transducer, which has to be iterated. In this article, we investigate the possibility of using generic techniques in cases where only specific techniques have been exploited so far. Finding that existing generic techniques are often not applicable in cases easily handled by specific techniques, we have developed a new approach to iterating transducers. This new approach builds on earlier work, but exploits a number of new conceptual and algorithmic ideas, often induced with the help of experiments, that give it a broad scope, as well as good performances.

This talk presents a survey of automata-based techniques for representing and manipulating linear arithmetic constraints. After introducing the basic concepts used in this approach, both representing integer constraints by finite-word automata and real constraints by infinite-word automata is discussed. Various results about the construction of automata from constraints and about the specific properties of automata representing arithmetic constraints are then presented. Finally, it is shown how this approach leads to simple and natural decision procedures that are in some ways related to tableaux.

Since the topic emerged several years ago, work on regular model checking has mostly been devoted to the verification of state reachability and safety properties. Though it was known that linear temporal properties could also be checked within this framework, little has been done about working out the corresponding details. This paper addresses this issue in the context of regular model checking based on the encoding of states by finite or infinite words. It works out the exact constructions to be used in both cases, and proposes a partial solution to the problem resulting from the fact that infinite computations of unbounded configurations might never contain the same configuration twice, thus making cycle detection problematic.

This paper considers the problem of computing the real convex hull of a finite set of n-dimensional integer vectors. The starting point is a finite-automaton representation of the initial set of vectors. The proposed method consists in computing a sequence of automata representing approximations of the convex hull and using extrapolation techniques to compute the limit of this sequence. The convex hull can then be directly computed from this limit in the form of an automaton-based representation of the corresponding set of real vectors. The technique is quite general and has been implemented. Also, our result fits in a wider scheme whose objective is to improve the techniques for converting automata-based representation of constraints to formulas.

If read digit by digit, a n-dimensional vector of integers represented in base r can be viewed as a word over the alphabet r n . It has been known for some time that, under this encoding, the sets of integer vectors recognizable by finite automata are exactly those definable in Presburger arithmetic if independence with respect to the base is required, and those definable in a slight extension of Presburger arithmetic if only a specific base is considered. Using the same encoding idea, but moving to infinite words, finite automata on infinite words can recognize sets of real vectors. This leads to the question of which sets of real vectors are recognizable by finite automata, which is the topic of this paper. We show that the recognizable sets of real vectors are those definable in the theory of reals and integers with addition and order, extended with a special base-dependent predicate that tests the value of a specified digit of a number. Furthermore, in the course of proving that sets of vectors defined in this theory are recognizable by finite automata, we show that linear equations and inequations have surprisingly compact representations by automata, which leads us to believe that automata accepting sets of real vectors can be of more than theoretical interest.

Checking infinite-state systems is frequently done by encoding infinite sets of states as regular languages. Computing such a regular representation of, say, the reachable set of states of a system requires acceleration techniques that can finitely compute the effect of an unbounded number of transitions. Among the acceleration techniques that have been proposed, one finds both specific and generic techniques. Specific techniques exploit the particular type of system being analyzed, e.g. a system manipulating queues or integers, whereas generic techniques only assume that the transition relation is represented by a finite-state transducer, which has to be iterated. In this paper, we survey two generic techniques that have been presented in [3] and [4]. Those techniques build on earlier work, but exploits a number of new conceptual and algorithmic ideas, often induced with the help of experiments, that give it a broad scope, as well as good performance.

On 18-19 May 2006, the Saarland University organized a two-day workshop about Trustworthy Software in order to present and foster the research competence in the SaarLorLuxWallonie region in the area of developing safe, secure and reliable software, computers and networks. As part of the Interreg III C E-Bird project Recherches sans fronti\`eres/Forschen ohne Grenzen it provided an excellent forum especially for young scientists to present and discuss recent results, new ideas and future research directions to a transnational audience from the SaarLorLuxWallonie region. The workshop consisted of 21 regular presentations and one invited talk. Abstracts of all presentations are collected in this paper, including links to extended abstracts or full papers. The first section directs to the preface of the proceedings.

Queue-content Decision Diagrams (QDDs) are finite-automaton based data structures for representing (possibly infinite) sets of contents of a finite collection of unbounded FIFO queues. Their intended use is to serve as a symbolic representation of the possible queue contents that can occur in the state space of a protocol modeled by finite-state machines communicating through unbounded queues. This is done with the help of a loop-first search, a state-space exploration technique that attempts whenever possible to compute symbolically the effect of repeatedly executing a loop any number of times, making it possible to analyze protocols with infinite state spaces though without the guarantee of termination. This paper first solves a key problem concerning the use of QDDs in this context: it precisely characterizes when, and shows how, the operations required by a loop-first search can be applied to QDDs. Then, it addresses the problem of exploiting QDDs and loop-first searches to broaden the range of properties that can be checked from simple state reachability to temporal logic. Finally, a sufficient criterion for the termination of a loop-first search using QDDs is given.

Translating linear temporal logic formulas to automata has proven to be an effective approach for implementing linear-time model-checking, and for obtaining many extensions and improvements to this verification method. On the other hand, for branching temporal logic, automata-theoretic techniques have long been thought to introduce an exponential penalty, making them essentially useless for model-checking. Recently, Bernholtz and Grumberg have shown that this exponential penalty can be avoided, though they did not match the linear complexity of non-automata-theoretic algorithms. In this paper we show that alternating tree automata are the key to a comprehensive automata-theoretic framework for branching temporal logics. Not only, as was shown by Muller et al., can they be used to obtain optimal decision procedures, but, as we show here, they also make it possible to derive optimal model-checking algorithms. Moreover, the simple combinatorial structure that emerges from the automata-theoretic approach opens up new possibilities for the implementation of branching-time model checking, and has enabled us to derive improved space complexity bounds for this long-standing problem.

Since the topic emerged several years ago, work on regular model checking has mostly been devoted to the verification of state reachability and safety properties. Though it was known that liveness properties could also be checked within this framework, little has been done about working out the corresponding details, and experimentally evaluating the approach. This paper addresses these issues in the context of regular model checking based on the encoding of states by finite or infinite words. It works out the exact constructions to be used in both cases, and solves the problem resulting from the fact that infinite computations of unbounded configurations might never contain the same configuration twice, thus making cycle detection problematic. Several experiments showing the applicability of the approach were successfully conducted.

This paper considers finite-automata based algorithms for handling linear arithmetic with both real and integer variables. Previous work has shown that this theory can be dealt with by using finite automata on infinite words, but this involves some difficult and delicate to implement algorithms. The contribution of this paper is to show, using topological arguments, that only a restricted class of automata on infinite words are necessary for handling real and integer linear arithmetic. This allows the use of substantially simpler algorithms, which have been successfully implemented.

The problem of complementing Büchi automata arises when developing decision procedures for temporal logics of programs. Unfortunately, previously known constructions for complementing Büchi automata involve a doubly exponential blow-up in the size of the automaton. We present a construction that involves only an exponential blow-up. We use this construction to prove a polynomial space upper bound for the propositional temporal logic of regular events and to prove a complexity hierarchy result for quantified propositional temporal logic.

In this paper, we apply Propositional Temporal Logic (PTL) to the specification and synthesis of the synchronization part of communicating processes. To specify a process, we give a PTL formula that describes its sequence of communications. The synthesis is done by constructing a model of the given specifications using a tableau-like satisfiability algorithm for PTL. This model can then be interpreted as a program.

“Regular model checking” is the name of a family of techniques for analyzing infinite-state systems in which states are represented by words or trees, sets of states by finite automata on these objects, and transitions by finite automata operating on pairs of state encodings, i.e. finite-state transducers. In this context, the central problem is then to compute the iterative closure of a finite-state transducer. This paper addresses the use of regular model-checking like techniques for systems whose states are represented by infinite (omega) words. Its main motivation is to show the feasibility and usefulness of this approach through a combination of the necessary theoretical developments, implementation, and experimentation. The iteration technique that is used is adapted from recent work of the authors on the iteration of finite-word transducers. It proceeds by comparing successive elements of a sequence of approximations of the iteration, detecting an “increment” that is added to move from one approximation to the next, and extrapolating the sequence by allowing arbitrary repetitions of this increment. By restricting oneself to weak deterministic Büchi automata, and using a number of implementation optimizations, examples of significant size can be handled. The proposed transducer iteration technique can just as well be exploited to compute the closure of a given set of states by the transducer iteration, which has proven to be a very effective way of using the technique. Examples such as a leaking gas burner in which time is modeled by real variables have been handled completely within the automata-theoretic setting.

This paper considers finite-automata based algorithms for handling linear arithmetic with both real and integer variables. Previous work has shown that this theory can be dealt with by using finite automata on in finite words, but this involves some difficult and delicate to implement algorithms. The contribution of this paper is to show, using topological arguments, that only a restricted class of automata on in finite words are necessary for handling real and integer linear arithmetic. This allows the use of substantially simpler algorithms and opens the path to the implementation of a usable system for handling this combined theory.

In computer system design, we distinguish between closed and open systems. A closed system is a system whose behavior is completely determined by the state of the system. An open system is a system that interacts with its environment and whose behavior depends on this interaction. The ability of temporal logics to describe an ongoing interaction of a reactive program with its environment makes them particularly appropriate for the specification of open systems. Nevertheless, model-checking algorithms used for the verification of closed systems are not appropriate for the verification of open systems. Correct model checking of open systems should check the system with respect to arbitrary environments and should take into account uncertainty regarding the environment. This is not the case with current model-checking algorithms and tools. In this paper we introduce and examine the problem of model checking of open systems (module checking, for short). We show that while module checking and model checking coincide for the linear-time paradigm, module checking is much harder than model checking for the branching-time paradigm. We prove that the problem of module checking is EXPTIME-complete for specifications in CTL and 2EXPTIME-complete for specifications in CTL*. This bad news is also carried over when we consider the program-complexity of module checking. As good news, we show that for the commonly-used fragment of CTL (universal, possibly, and always possibly properties), current model-checking tools do work correctly, or can be easily adjusted to work correctly, with respect to both closed and open systems.

Translating linear temporal logic formulas to automata has proven to be an effective approach for implementing linear-time model-checking, and for obtaining many extensions and improvements to this verification method. On the other hand, for branching temporal logic, automata-theoretic techniques have long been thought to introduce an exponential penalty, making them essentially useless for model-checking. Recently, Bernholtz and Grumberg [1993] have shown that this exponential penalty can be avoided, though they did not match the linear complexity of non-automata-theoretic algorithms. In this paper, we show that alternating tree automata are the key to a comprehensive automata-theoretic framework for branching temporal logics. Not only can they be used to obtain optimal decision procedures, as was shown by Muller et al., but, as we show here, they also make it possible to derive optimal model-checking algorithms. Moreover, the simple combinatorial structure that emerges from the automata-theoretic approach opens up new possibilities for the implementation of branching-time model checking and has enabled us to derive improved space complexity bounds for this long-standing problem.

This paper is motivated by the fact that verifying liveness properties under a fairness condition is often problematic, especially when abstraction is used. It shows that using a more abstract notion than truth under fairness, specifically the concept of relative liveness property can lead to interesting possibilities. Technically, it is first established that deciding relative liveness is a PSPACE-complete problem and it is shown that relative liveness properties ca ai-ways be satisfied by some fair implementation. Thereafter, the interaction between behavior abstraction and relative Iiveness properties is studied and it is proved that relative liveness properties can be verified on behavior abstractions, if the abstracting homomorphism is simple in the sense of Ochsenschlager. To be able to verify liveness properties of a system [3], it is almost always necessary to include a fairness hypothesis in the system description [9]. Indeed, int reducing a fairness hypothesis makes it possible to ignore behaviors that correspond to extreme execution scenarios and that, in any case, would not occur in any reasonable implementation. Even though th:s intuition is clear, making fairness precise is somewhat more complicated: should one be " weakly " or " strongly " fair, " transition " or " process " fair, or isn't " justice " or even " compassion " what fairness should really be [15]? Of course, there is a rational way of choosing which fairness notion is adequate for a given problem by considering the nature of the model being used and making reason-" Ulrich Nitsche was supported by a DA AD-fellowship HSP 11/AUFE to visit the University of Li&ge. Parts of this work have been done during his visit.

This paper gives a simple and direct algorithm for computing the always regular set of reachable states of a pushdown system. It then exploits this algorithm for obtaining model checking algorithms for linear-time temporal logic as well as for the logic CTL∗. For the latter, a new technical tool is introduced: pushdown automata with transitions conditioned on regular predicates on the stack content. Finally, this technical tool is also used to establish that CTL∗ model checking remains decidable when the formulas are allowed to include regular predicates on the stack content.