Browse ORBi by ORBi project

- Background
- Content
- Benefits and challenges
- Legal aspects
- Functions and services
- Team
- Help and tutorials

A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems Linden, Alexander ; Wolper, Pierre in Proceedings of the 19th international conference on Tools and algorithms for the construction and analysis of systems (2013, March) 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 ... [more ▼] 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. [less ▲] Detailed reference viewed: 134 (25 ULg)A Verification-Based Approach to Memory Fence Insertion in Relaxed Memory Systems Linden, Alexander ; Wolper, Pierre in Model Checking Software , 18th International SPIN Workshop (2011, July) 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 ... [more ▼] 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 TSO (Total Store Order) relaxation, which corresponds to the use of store buffers, and its extension x86-TSO, which in addition allows synchronization and lock operations. The proposed approach uses 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 memory model, but that might be incorrect under x86-TSO. This program is then analyzed for this relaxed memory model and when errors are found (with respect to safety properties), memory fences are inserted in order to avoid these errors. The approach proceeds iteratively and heuristically, inserting memory fences until correctness is obtained, which is guaranteed to happen. An advantage of our technique is that the underlying symbolic verification tool makes a full exploration 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. [less ▲] Detailed reference viewed: 186 (57 ULg)An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models Linden, Alexander ; Wolper, Pierre in Lecture Notes in Computer Science (2010, September) This paper addresses the problem of verifying programs for the relaxed memory models implemented in modern processors. Specifically, it considers the TSO (Total Store Order) relaxation, which corresponds ... [more ▼] This paper addresses the problem of verifying programs for the relaxed memory models implemented in modern processors. Specifically, it considers the TSO (Total Store Order) relaxation, which corresponds to the use of store buffers. The proposed approach proceeds by using finite automata to symbolically represent the possible contents of the store buffers. Store, load and commit operations then correspond to operations on these finite automata. The advantage of this approach is that it operates on (potentially infinite) sets of buffer contents, rather than on individual buffer configurations. This provides a way to tame the explosion of the number of possible buffer configurations, while preserving the full generality of the analysis. It is thus possible to check even designs that exploit the relaxed memory model in unusual ways. An experimental implementation has been used to validate the feasibility of the approach. [less ▲] Detailed reference viewed: 244 (82 ULg)On (Omega-)regular model checking ; Wolper, Pierre in ACM Transactions on Computational Logic (2010), 12(1), 46 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 ... [more ▼] 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. [less ▲] Detailed reference viewed: 53 (13 ULg)Computing Convex Hulls by Automata Iteration Cantin, François ; ; Wolper, Pierre in International Journal of Foundations of Computer Science (2009), 20(4), 647-667 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 ... [more ▼] 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. [less ▲] Detailed reference viewed: 78 (23 ULg)Computing Convex Hulls by Automata Iteration Cantin, François ; ; Wolper, Pierre in Lecture Notes in Computer Science (2008, July), 5148 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 ... [more ▼] 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 automatonbased 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. [less ▲] Detailed reference viewed: 96 (37 ULg)Automates et vérification Wolper, Pierre in Encyclopédie de l'informatique et des systèmes d'information (2006) La vérification de programmes consiste à analyser les comportements possibles de programmes en vue de déterminer s’ils seront toujours conformes à ce qui est attendu. Pour ce faire, les caractéristiques ... [more ▼] La vérification de programmes consiste à analyser les comportements possibles de programmes en vue de déterminer s’ils seront toujours conformes à ce qui est attendu. Pour ce faire, les caractéristiques souhaitées des comportements sont exprimées formellement et confrontées, par des techniques mathématiques rigoureuses, à l’ensemble des comportements du programme à analyser. Dans ce contexte, les automates jouent un triple rôle. Tout d’abord, ils sont fréquemment utilisés en tant que langage de programmation simplifié pour décrire les programmes à analyser. Ensuite, ils servent de formalisme de description de propriétés de comportements, soit directement, soit par traduction à partir d’un langage logique. Finalement, ils s’avèrent très utiles en tant que formalisme de description d’ensembles infinis de valeurs. [less ▲] Detailed reference viewed: 90 (22 ULg)On the Use of Automata-based Techniques in Symbolic Model Checking: invited address ; Wolper, Pierre in Electronic Notes in Theoretical Computer Science (2006, March 09), 150(1), 3-8 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 ... [more ▼] 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 [B. Boigelot and A. Legay and P. Wolper, Iterating Transducers in the Large, Proc. 15th Int. Conf. on Computer Aided Verification, Boulder, USA, Lecture Notes in Computer Science, volume 2725, year 2003, pages 223–235] and [B. Boigelot and A. Legay and P. Wolper, Omega-Regular Model Checking, Proc. 10th Int. Conf. on Tools and and Algorithms for the Construction and Analysis of Systems, Barcelona, Spain, Lecture Notes in Computer Science, volume 2988, year 2004, pages 561–575]. 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. [less ▲] Detailed reference viewed: 53 (9 ULg)Introduction à la Calculabilit́e Wolper, Pierre Book published by Dunod - 3e (2006) Dans le monde de l'informatique en perpétuelle évolution, une connaissance élémentaire de la théorie de la calculabilité reste plus que jamais indispensable à l'informaticien, qui se pose sans cesse la ... [more ▼] Dans le monde de l'informatique en perpétuelle évolution, une connaissance élémentaire de la théorie de la calculabilité reste plus que jamais indispensable à l'informaticien, qui se pose sans cesse la question des limites de l'informatique. La théorie de la calculabilité apporte des réponses. Elle démontre notamment que certains problèmes informatiques ne peuvent pas être résolus par des programmes. Cet ouvrage présente les éléments essentiels de cette science qui consiste à étudier ce qu'il est possible ou non de résoudre grâce à l'outil informatique, quelle que soit la machine utilisée. Il aborde en premier lieu les langages formels, les automates et les grammaires puis introduit la notion de calculabilité par le biais des machines de Turing et des fonctions récursives. En dernier lieu, sont étudiées les notions de complexité, et plus particulièrement les problèmes NP-complets. Ce manuel comporte de nombreux exercices d'application, ainsi que leurs corrigés. Cette troisième édition s'enrichit d'une section sur l'interprétation de la non-calculabilité et approfondit la notion de NP-complétude. Si ce livre constitue avant tout un cours destiné aux étudiants en informatique, il s'adresse également aux professionnels désireux de mieux comprendre cette science. [less ▲] Detailed reference viewed: 648 (74 ULg)Handling Liveness Properties in (ω-)Regular Model Checking ; ; Wolper, Pierre in Electronic Notes in Theoretical Computer Science (2005, December 28), 138(3), 101-115 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 ... [more ▼] 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. [less ▲] Detailed reference viewed: 59 (3 ULg)An effective decision procedure for linear arithmetic over the integers and reals Boigelot, Bernard ; Jodogne, Sébastien ; Wolper, Pierre in ACM transactions on Computational Logic (2005), 6(3), 614--633 This article 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 ... [more ▼] This article 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 article 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. [less ▲] Detailed reference viewed: 55 (15 ULg)Omega-regular model checking Boigelot, Bernard ; ; Wolper, Pierre in Lecture Notes in Computer Science (2004), 2988 "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 ... [more ▼] "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 Buchi 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. [less ▲] Detailed reference viewed: 61 (10 ULg)Iterating transducers in the large Boigelot, Bernard ; ; Wolper, Pierre in Lecture Notes in Computer Science (2003), 2725 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 ... [more ▼] 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 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 performance. [less ▲] Detailed reference viewed: 39 (7 ULg)Representing arithmetic constraints with finite automata: An overview Boigelot, Bernard ; Wolper, Pierre in Lecture Notes in Computer Science (2002, July), 2401 Linear numerical constraints and their first-order theory, whether defined over the reals or the. integers, are basic tools that appear in many areas of Computer Science. This paper overviews a set of ... [more ▼] Linear numerical constraints and their first-order theory, whether defined over the reals or the. integers, are basic tools that appear in many areas of Computer Science. This paper overviews a set of techniques based on finite automata that lead to decision procedures and other useful algorithms, as well as to a normal form, for the first-order linear theory of the integers, of the reals, and of the integers and reals combined. This approach has led to an implemented tool, which has the so far unique capability of handling the linear. first-order theory of the integers and reals combined. [less ▲] Detailed reference viewed: 35 (7 ULg)Representing Periodic Temporal Information with Automata Wolper, Pierre in Proc. Eighth International Symposium on Temporal Representation and Reasoning (2001, June) Motivated by issues in temporal databases and in the verification of infinite-state systems, this talk considers the problem of representing periodic dense time information. Doing so requires handling a ... [more ▼] Motivated by issues in temporal databases and in the verification of infinite-state systems, this talk considers the problem of representing periodic dense time information. Doing so requires handling a theory that combines discrete and continuous variables, since discrete variables are essential for representing periodicity. An automata-based approach for dealing with such a combined theory is thus introduced. [less ▲] Detailed reference viewed: 38 (3 ULg)On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables Boigelot, Bernard ; Jodogne, Sébastien ; Wolper, Pierre in Lecture Notes in Computer Science (2001), 2083 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 ... [more ▼] 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. [less ▲] Detailed reference viewed: 37 (6 ULg)Module checking ; ; Wolper, Pierre in Information & Computation (2001), 164(2), 322-344 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 ... [more ▼] 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. (C) 2001 Academic Press. [less ▲] Detailed reference viewed: 43 (9 ULg)Constructing Automata from Temporal Logic Formulas: A Tutorial Wolper, Pierre in Lecture Notes in Computer Science (2001), 2090 This paper presents a tutorial introduction to the construction of finite-automata on infinite words from linear-time temporal logic formulas. After defining the source and target formalisms, it describes ... [more ▼] This paper presents a tutorial introduction to the construction of finite-automata on infinite words from linear-time temporal logic formulas. After defining the source and target formalisms, it describes a first construction whose correctness is quite direct to establish, but whose behavior is always equal to the worst-case upper bound. It then turns to the techniques that can be used to improve this algorithm in order to obtain the quite effective algorithms that are now in use. [less ▲] Detailed reference viewed: 63 (10 ULg)Introduction à la Calculabilité Wolper, Pierre Book published by Dunod - 2e (2001) Detailed reference viewed: 107 (21 ULg)An efficient automata approach to some problems on context-free grammars ; ; et al in Information Processing Letters (2000), 74(5-6), 221-227 Book and Otto (1993) solve a number of word problems for monadic string-rewriting systems using an elegant automata-based technique. In this note we observe that the technique is also very interesting ... [more ▼] Book and Otto (1993) solve a number of word problems for monadic string-rewriting systems using an elegant automata-based technique. In this note we observe that the technique is also very interesting from a pedagogical point of view, since it provides a uniform solution to several elementary problems on context-free languages. [less ▲] Detailed reference viewed: 37 (0 ULg) |
||