Linden, A. (2013).

*On the Verification of Programs on Relaxed Memory Models*. Unpublished doctoral thesis, Université de Liège, Liège, Belgique.Classical model-checking tools verify concurrent programs under the
traditional "Sequential Consistency" (SC) memory model, in which all
accesses to the shared memory are immediately visible globally, and ...

Linden, A., & Wolper, P. (2013). A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems.

*Proceedings of the 19th international conference on Tools and algorithms for the construction and analysis of systems*(pp. 339-353). Springer.Peer reviewed

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 ...

Linden, A., & Wolper, P. (2011). A Verification-Based Approach to Memory Fence Insertion in Relaxed Memory Systems.

*Model Checking Software , 18th International SPIN Workshop*(pp. 144-160). Berlin, Germany: Springer.Peer reviewed

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 ...

Linden, A., & Wolper, P. (2010, September). An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models.

*Lecture Notes in Computer Science*, 212-226.Peer reviewed

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 ...

Legay, A., & Wolper, P. (2010). On (Omega-)regular model checking.

*ACM Transactions on Computational Logic, 12*(1), 46.Peer reviewed (verified by ORBi)

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 ...

Cantin, F., Legay, A., & Wolper, P. (2009). Computing Convex Hulls by Automata Iteration.

*International Journal of Foundations of Computer Science, 20*(4), 647-667.Peer reviewed (verified by ORBi)

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 ...

Cantin, F., Legay, A., & Wolper, P. (2008). Computing Convex Hulls by Automata Iteration.

*Lecture Notes in Computer Science, 5148*, 112-121.Peer reviewed

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 ...

Wolper, P. (2006). Automates et vérification.

*Encyclopédie de l'informatique et des systèmes d'information*(pp. 977--986). Paris, France: Vuibert.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 ...

Legay, A., & Wolper, P. (2006). On the Use of Automata-based Techniques in Symbolic Model Checking: invited address.

*Electronic Notes in Theoretical Computer Science, 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 requires ...

Van Lishout, F. (2006).

*Single-player games: introduction to a new solving method*. Unpublished DEA/DES thesis, University of Liège, Liège, Belgium.In many games, the machine has become stronger than the best human players. Machines have already beaten the human World Champion in famous games like Checkers, Chess, Scrabble and Othello. However, mankind ...

Wolper, P. (2006).

*Introduction à la Calculabilit́e*(3e). Dunod.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 ...

Bouajjani, A., Legay, A., & Wolper, P. (2005). Handling Liveness Properties in (ω-)Regular Model Checking.

*Electronic Notes in Theoretical Computer Science, 138*(3), 101-115.Peer reviewed

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 ...

Boigelot, B., Jodogne, S., & Wolper, P. (2005). An effective decision procedure for linear arithmetic over the integers and reals.

*ACM Transactions on Computational Logic, 6*(3), 614--633.Peer reviewed (verified by ORBi)

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 ...

Boigelot, B., Legay, A., & Wolper, P. (2004). Omega-regular model checking.

*Lecture Notes in Computer Science, 2988*, 561-575.Peer reviewed

"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 ...

Boigelot, B., Legay, A., & Wolper, P. (2003). Iterating transducers in the large.

*Lecture Notes in Computer Science, 2725*, 223-235.Peer reviewed

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 ...

Boigelot, B., & Wolper, P. (2002). Representing arithmetic constraints with finite automata: An overview.

*Lecture Notes in Computer Science, 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 ...

Wolper, P. (2001). Representing Periodic Temporal Information with Automata.

*Proc. Eighth International Symposium on Temporal Representation and Reasoning*(pp. 179). IEEE Computer Society.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 ...

Boigelot, B., Jodogne, S., & Wolper, P. (2001). On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables.

*Lecture Notes in Computer Science, 2083*, 611--625.Peer reviewed

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 ...

Kupferman, O., Vardi, M. Y., & Wolper, P. (2001). Module checking.

*Information and Computation, 164*(2), 322-344.Peer reviewed (verified by ORBi)

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 ...

Wolper, P. (2001). Constructing Automata from Temporal Logic Formulas: A Tutorial.

*Lecture Notes in Computer Science, 2090*, 261--277.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 ...

Bouajjani, A., Esparza, J., Finkel, A., Maler, O., Rossmanith, P., Willems, B., & Wolper, P. (2000). An efficient automata approach to some problems on context-free grammars.

*Information Processing Letters, 74*(5-6), 221-227.Peer reviewed (verified by ORBi)

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 ...

Wolper, P., & Boigelot, B. (2000). On the construction of automata from linear arithmetic constraints.

*Lecture Notes in Computer Science, 1785*, 1-19.This paper presents an overview of algorithms for constructing automata from linear arithmetic constraints. It identifies one case in which the special structure of the automata that are constructed allows a ...

Kupferman, O., Vardi, M. Y., & Wolper, P. (2000). An automata-theoretic approach to branching-time model checking.

*Journal of the ACM, 47*(2), 312-360.Peer reviewed (verified by ORBi)

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 ...

Baudinet, M., Chomicki, J., & Wolper, P. (1999). Constraint-generating dependencies.

*Journal of Computer and System Sciences, 59*(1), 94-115.Peer reviewed (verified by ORBi)

Traditionally, dependency theory has been developed for uninterpreted data. Specifically, the only assumption that is made about the data domains is that data values can be compared for equality. However, data ...

Boigelot, B. (1998).

*Symbolic Methods for Exploring Infinite State Spaces*. Unpublished doctoral thesis, Université de Liège, Liège, Belgium.In this thesis, we introduce a general method for computing the
set of reachable states of an infinite-state system. The basic
idea, inspired by well-known state-space exploration methods for
finite-state ...

Boigelot, B., Rassart, S., & Wolper, P. (1998). On the Expressiveness of Real and Integer Arithmetic Automata.

*Lecture Notes in Computer Science, 1443*, 152-163.Peer reviewed

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 to the n. It has been known for some time that, under this encoding, the
sets of ...

Peled, D., Wilke, T., & Wolper, P. (1998). An algorithmic approach for checking closure properties of temporal logic specifications and ω-regular languages.

*Theoretical Computer Science, 195*(2), 183--203.Peer reviewed (verified by ORBi)

In concurrency theory, there are several examples where the interleaved model of concurrency can distinguish between execution sequences which are not significantly different. One such example is sequences ...

Wolper, P., & Boigelot, B. (1998). Verifying Systems with Infinite but Regular State Spaces.

*Lecture Notes in Computer Science, 1427*, 88-97.Thanks to the development of a number of efficiency enhancing
techniques, state-space exploration based verification, and in
particular model checking, has been quite successful for finite-state
systems ...

Boigelot, B., Godefroid, P., Willems, B., & Wolper, P. (1997). The Power of QDDs.

*Lecture Notes in Computer Science, 1302*, 172-186.Peer reviewed

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 ... ...

Wolper, P. (1997). The meaning of formal: from weak to strong formal methods.

*International Journal on Software Tools for Technology Transfer, 1*(1-2), 6--8.Peer reviewed (verified by ORBi)

This short note reflects on what makes formal methods "formal". It concludes that there are weak and
strong ways of being formal, the latter being linked to the formality of the method being exploitable, and exploited, in software tools.

Wolper, P. (1996). The Meaning of ``Formal''.

*ACM Computing Surveys, 28*(4es), 127.Peer reviewed (verified by ORBi)

Wolper, P. (1996). Where is the Algorithmic Support?

*ACM Computing Surveys, 28*(4es), 58.Peer reviewed (verified by ORBi)

Gerth, R., Peled, D., Vardi, M. Y., & Wolper, P. (1995). Simple On-the-fly Automatic Verification of Linear Temporal Logic. In P., Dembinski & M., Sredniawa (Eds.),

*Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification*. IFIP.Peer reviewed

We present a tableau-based algorithm for obtaining an automaton from a temporal logic formula. The algorithm is geared towards being used in model checking in an “on-the-fly” fashion, that is the automaton can ...

Kabanza, F., Stevenne, J.-M., & Wolper, P. (1995). Handling infinite temporal data.

*Journal of Computer and System Sciences, 51*(1), 3--17.Peer reviewed (verified by ORBi)

In this paper, we present a powerful framework for describing, storing, and reasoning about infinite temporal information. This framework is an extension of classical relational databases. It represents ...

Wolper, P., & Boigelot, B. (1995). An Automata-Theoretic Approach to Presburger Arithmetic Constraints.

*Lecture Notes in Computer Science, 983*, 21-32.This paper introduces a finite-automata based representation of
Presburger arithmetic definable sets of integer vectors. The
representation consists of concurrent automata operating on the
binary encodings ...

Boigelot, B., & Wolper, P. (1994). Symbolic Verification with Periodic Sets.

*Lecture Notes in Computer Science, 818*, 55-67.Peer reviewed

Symbolic approaches attack the state explosion problem by introducing
implicit representations that allow the simultaneous manipulation of
large sets of states. The most commonly used representation in ... ...

Godefroid, P., & Wolper, P. (1994). A Partial Approach To Model Checking.

*Information and Computation, 110*(2), 305--326.Peer reviewed (verified by ORBi)

This paper presents a model-checking method for linear-time temporal logic that can avoid most of the state explosion due to the modelling of concurrency by interleaving. The method relies on the concept of ...

Vardi, M. Y., & Wolper, P. (1994). Reasoning about Infinite Computations.

*Information and Computation, 115*(1), 1-37.Peer reviewed (verified by ORBi)

We investigate extensions of temporal logic by connectives defined by finite automata on infinite words. We consider three different logics, corresponding to three different types of acceptance conditions ...

Baudinet, M., Chomicki, J., & Wolper, P. (1993).

*Temporal Databases: Beyond Finite Extensions (position paper)*. Paper presented at International Woorkshop on an Infrastructure for Temporal Databases, Arlington, Texas.We argue that temporal databases should not be restricted to relations with finite extensions. many temporal events are periodic and have no natural bounds. Moreover, such events have a more compact ...

Godefroid, P., & Wolper, P. (1993). Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties.

*Formal Methods in System Design, 2*(2), 149--164.Peer reviewed (verified by ORBi)

This article presents an algorithm for detecting deadlocks in concurrent finite-state systems without incurring most of the state explosion due to the modeling of concurrency by interleaving. For systems that ...

Courcoubetis, C., Vardi, M. Y., Wolper, P., & Yannakakis, M. (1992). Memory Efficient Algorithms for the Verification of Temporal Properties.

*Formal Methods in System Design, 1*, 275--288.Peer reviewed (verified by ORBi)

This paper addresses the problem of designing memory-efficient algorithms for the verification of temporal properties of finite-state programs. Both the programs and their desired temporal properties are ...

Courcoubetis, C., Vardi, M., Wolper, P., & Yannakakis, M. (1991). Memory efficient algorithms for the verification of temporal properties.

*Computer-Aided Verification, 2nd International Conference Proceedings*(pp. 233-242). Berlin, Germany: Springer.Peer reviewed

This paper addresses the problem of designing memory efficient algorithms for the verification of temporal properties of finite-state programs. Both the programs and their desired temporal properties are ...

Godefroid, P., & Wolper, P. (1991). A Partial Approach To Model Checking.

*Proceedings 6th IEEE Symposium on Logic in Computer Science*(pp. 406--415). New York, NY: IEEE.Peer reviewed

This paper presents a model-checking method for linear-time temporal logic that avoids the state explosion due to the modelling of concurrency by interleaving. The method relies on the concept of Mazurkiewicz ...

Vardi, M. Y., & Wolper, P. (1986). An Automata-Theoretic Approach to Automatic Program Verification.

*Proceedings of the First Symposium on Logic in Computer Science*(pp. 322--331). IEEE Computer Society.Peer reviewed

We describe an automata-theoretic approach to the automatic verification of concurrent finite-state programs by
model checking.The basic idea underlying this approach is that for any temporal formula we can ...

Vardi, M. Y., & Wolper, P. (1986). Automata-Theoretic Techniques for Modal Logics of Programs.

*Journal of Computer and System Science, 32*(2), 183-221.Peer reviewed (verified by ORBi)

We present a new technique for obtaining decision procedures for modal logics of programs. The technique centers around a new class of finite automata on infinite trees for which the emptiness problem can be ...

Wolper, P. (1985). The Tableau Method for Temporal Logic: An Overview.

*Logique et Analyse*, (110--111), 119--136.Peer reviewed

An overview of the tableau decision method for propositional temporal logic is presented. The method is described in detail for linear time temporal logic. It is then discussed how it can be applied to other ...

Manna, Z., & Wolper, P. (1984). Synthesis of Communicating Processes from Temporal Logic Specifications.

*ACM Transactions on Programming Languages and Systems, 6*(1), 68-93.Peer reviewed (verified by ORBi)

In this paper, Propositional Temporal Logic (PTL) is applied to the specification and synthesis of
the synchronization part of communicating processes. To specify a process, a PTL formula that
describes its ...

Vardi, M. Y., & Wolper, P. (1984). Automata-Theoretic Techniques for Modal Logics of Programs.

*Proc. 16th ACM Symposium on Theory of Computing*(pp. 446--456). New York, USA: ACM.Peer reviewed

We present a new technique for obtaining decision procedures for modal logics of programs. The technique centers around a new class of finite automata on infinite trees for which the emptiness problemcan be ...

Vardi, M. Y., & Wolper, P. (1984). Yet Another Process Logic. In E., Clarke & D., Kozen,

*Logics of Programs*(pp. 501--512). Springer-Verlag.Peer reviewed

We present a process logic that differs from the one introduced by Harel, Kozen and Parikh in several ways. First, we use the extended temporal logic of Wolper for statements about paths. Second, we allow a ...

Wolper, P. (1983). Temporal Logic Can Be More Expressive.

*Information and Control, 56*(1--2), 72--99.Peer reviewed (verified by ORBi)

We first review Temporal Logic and prove that there are some properties of sequences that it cannot express,
though these are expressible using for instance regular expressions. Then, we show how Temporal ...