Specification and Synthesis of Communicating Processes using an Extended Temporal Logic. - Pierre Wolper (POPL, 1982)

Synthesis of communicating processes from temporal logic specifications. - Pierre Wolper (1982)

Reasoning about Infinite Computation Paths (Extended Abstract) - Pierre Wolper; Moshe Y. Vardi; A. Prasad Sistla (FOCS, 1983)

Yet Another Process Logic (Preliminary Version). - Moshe Y. Vardi; Pierre Wolper (Logic of Programs, 1983)

Temporal Logic Can Be More Expressive - Pierre Wolper (Inf. Control., 1983)

A Temporal Logic for Reasoning about Partially Ordered Computations (Extended Abstract). - Shlomit S. Pinter; Pierre Wolper (PODC, 1984)

Automata Theoretic Techniques for Modal Logics of Programs (Extended Abstract) - Moshe Y. Vardi; Pierre Wolper (STOC, 1984)

Synthesis of Communicating Processes from Temporal Logic Specifications. - Zohar Manna; Pierre Wolper (ACM Trans. Program. Lang. Syst., 1984)

The Complementation Problem for Büchi Automata with Applications to Temporal Logic (Extended Abstract). - A. Prasad Sistla; Moshe Y. Vardi; Pierre Wolper (ICALP, 1985)

An Automata-Theoretic Approach to Automatic Program Verification (Preliminary Report) - Moshe Y. Vardi; Pierre Wolper (LICS, 1986)

Expressing Interesting Properties of Programs in Propositional Temporal Logic. - Pierre Wolper (POPL, 1986)

Reasoning about Fair Concurrent Programs - Costas Courcoubetis; Moshe Y. Vardi; Pierre Wolper (STOC, 1986)

Automata-Theoretic Techniques for Modal Logics of Programs. - Moshe Y. Vardi; Pierre Wolper (J. Comput. Syst. Sci., 1986)

On the Relation of Programs and Computations to Models of Temporal Logic. - Pierre Wolper (Temporal Logic in Specification, 1987)

The Complementation Problem for Büchi Automata with Appplications to Temporal Logic. - A. Prasad Sistla; Moshe Y. Vardi; Pierre Wolper (Theor. Comput. Sci., 1987)

Verifying Properties of Large Sets of Processes with Network Invariants. - Pierre Wolper; Vinciane Lovinfosse (Automatic Verification Methods for Finite State Systems, 1989)

Reasoning about Cryptographic Protocols. - Marie-Jeanne Toussaint; Pierre Wolper (Distributed Computing And Cryptography, 1989)

Realizable and Unrealizable Specifications of Reactive Systems. - Martín Abadi; Leslie Lamport; Pierre Wolper (ICALP, 1989)

Adding Liveness Properties to Coupled Finite-State Machines. - Sudhir Aggarwal; Costas Courcoubetis; Pierre Wolper (ACM Trans. Program. Lang. Syst., 1990)

On the Representation of Infinite Temporal Data and Queries. - Marianne Baudinet; Marc Niézette; Pierre Wolper (PODS, 1991)

Memory-Efficient Algorithms for the Verification of Temporal Properties. - Costas Courcoubetis; Moshe Y. Vardi; Pierre Wolper; Mihalis Yannakakis (Formal Methods Syst. Des., 1992)

Temporal Deductive Databases. - Marianne Baudinet; Jan Chomicki; Pierre Wolper (Temporal Databases, 1993)

Reliable Hashing without Collosion Detection. - Pierre Wolper; Denis Leroy (CAV, 1993)

Partial-Order Methods for Temporal Verification. - Pierre Wolper; Patrice Godefroid (CONCUR, 1993)

Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties. - Patrice Godefroid; Pierre Wolper (Formal Methods Syst. Des., 1993)

An Automata-Theoretic Approach to Branching-Time Model Checking (Extended Abstract). - Orna Bernholtz; Moshe Y. Vardi; Pierre Wolper (CAV, 1994)

Symbolic Verification with Periodic Sets. - Bernard Boigelot; Pierre Wolper (CAV, 1994)

A Partial Approach to Model Checking - Patrice Godefroid; Pierre Wolper (Inf. Comput., 1994)

Reasoning About Infinite Computations - Moshe Y. Vardi; Pierre Wolper (Inf. Comput., 1994)

Simple on-the-fly automatic verification of linear temporal logic. - Rob Gerth; Doron A. Peled; Moshe Y. Vardi; Pierre Wolper (PSTV, 1995)

An Automata-Theoretic Approach to Presburger Arithmetic Constraints (Extended Abstract) - Pierre Wolper; Bernard Boigelot (SAS, 1995)

Handling Infinite Temporal Data. - Froduald Kabanza; Jean-Marc Stévenne; Pierre Wolper (J. Comput. Syst. Sci., 1995)

An Algorithmic Approach for Checking Closure Properties of omega-Regular Languages. - Doron A. Peled; Thomas Wilke; Pierre Wolper (CONCUR, 1996)

Partial-Order Methods for Model Checking: From Linear Time to Branching Time. - Bernard Willems; Pierre Wolper (LICS, 1996)

Where is the Algorithmic Support? - Pierre Wolper (ACM Comput. Surv., 1996)

The Meaning of "Formal". - Pierre Wolper (ACM Comput. Surv., 1996)

Relative Liveness and Behavior Abstraction (Extended Abstract). - Ulrich Nitsche; Pierre Wolper (PODC, 1997)

The Power of QDDs (Extended Abstract). - Bernard Boigelot; Patrice Godefroid; Bernard Willems; Pierre Wolper (SAS, 1997)

A direct symbolic approach to model checking pushdown systems. - Alain Finkel; Bernard Willems; Pierre Wolper (INFINITY, 1997)

The Meaning of "Formal": From Weak to Strong Formal Methods. - Pierre Wolper (Int. J. Softw. Tools Technol. Transf., 1997)

Verifying Systems with Infinite but Regular State Spaces. - Pierre Wolper; Bernard Boigelot (CAV, 1998)

On the Expressiveness of Real and Integer Arithmetic Automata (Extended Abstract). - Bernard Boigelot; Stéphane Rassart; Pierre Wolper (ICALP, 1998)

Algorithms for Synthesizing Reactive Systems: A Perspective (Abstract). - Pierre Wolper (LOPSTR, 1998)

An Algorithmic Approach for Checking Closure Properties of Temporal Logic Specifications and Omega-Regular Languages. - Doron A. Peled; Thomas Wilke; Pierre Wolper (Theor. Comput. Sci., 1998)

Constraint-Generating Dependencies. - Marianne Baudinet; Jan Chomicki; Pierre Wolper (J. Comput. Syst. Sci., 1999)

Linear Repeating Points. - Pierre Wolper (Constraint Databases, 2000)

Constructing Automata from Temporal Logic Formulas: A Tutorial. - Pierre Wolper (European Educational Forum: School on Formal Methods and Performance Analysis, 2000)

On the Construction of Automata from Linear Arithmetic Constraints. - Pierre Wolper; Bernard Boigelot (TACAS, 2000)

An efficient automata approach to some problems on context-free grammars. - Ahmed Bouajjani; Javier Esparza; Alain Finkel; Oded Maler; Peter Rossmanith; Bernard Willems; Pierre Wolper (Inf. Process. Lett., 2000)

An automata-theoretic approach to branching-time model checking. - Orna Kupferman; Moshe Y. Vardi; Pierre Wolper (J. ACM, 2000)

On the Use of Weak Automata for Deciding Linear Arithmetic with Integer and Real Variables. - Bernard Boigelot; Sébastien Jodogne; Pierre Wolper (IJCAR, 2001)

Representing Periodic Temporal Information with Automata. - Pierre Wolper (TIME, 2001)

Checking Properties within Fairness and Behavior Abstractions - Ulrich Ultes-Nitsche; Pierre Wolper (CoRR, 2001)

Module Checking. - Orna Kupferman; Moshe Y. Vardi; Pierre Wolper (Inf. Comput., 2001)

Representing Arithmetic Constraints with Finite Automata: An Overview. - Bernard Boigelot; Pierre Wolper (ICLP, 2002)

Iterating Transducers in the Large (Extended Abstract). - Bernard Boigelot; Axel Legay; Pierre Wolper (CAV, 2003)

An Effective Decision Procedure for Linear Arithmetic with Integer and Real Variables - Bernard Boigelot; Sébastien Jodogne; Pierre Wolper (CoRR, 2003)

Omega-Regular Model Checking. - Bernard Boigelot; Axel Legay; Pierre Wolper (TACAS, 2004)

Handling Liveness Properties in (omega-)Regular Model Checking. - Ahmed Bouajjani; Axel Legay; Pierre Wolper (INFINITY, 2004)

On the Use of Automata-based Techniques in Symbolic Model Checking: Invited Address. - Axel Legay; Pierre Wolper (MTCoord@COORDINATION, 2005)

An effective decision procedure for linear arithmetic over the integers and reals. - Bernard Boigelot; Sébastien Jodogne; Pierre Wolper (ACM Trans. Comput. Log., 2005)

Preface – Workshop Trustworthy Software 2006. - Serge Autexier; Stephan Merz; Leendert W. N. van der Torre; Reinhard Wilhelm; Pierre Wolper (Trustworthy Software, 2006)

On the Use of Automata for Deciding Linear Arithmetic. - Pierre Wolper (TABLEAUX, 2009)

A Framework to Handle Linear Temporal Properties in ( omega-)Regular Model Checking - Ahmed Bouajjani; Axel Legay; Pierre Wolper (CoRR, 2009)

Computing Convex Hulls by Automata Iteration. - François Cantin; Axel Legay; Pierre Wolper (Int. J. Found. Comput. Sci., 2009)

An Automata-Based Symbolic Approach for Verifying Programs on Relaxed Memory Models. - Alexander Linden 001; Pierre Wolper (SPIN, 2010)

On (Omega-)regular model checking. - Axel Legay; Pierre Wolper (ACM Trans. Comput. Log., 2010)

A Verification-Based Approach to Memory Fence Insertion in Relaxed Memory Systems. - Alexander Linden 001; Pierre Wolper (SPIN, 2011)

A Verification-Based Approach to Memory Fence Insertion in PSO Memory Systems. - Alexander Linden 001; Pierre Wolper (TACAS, 2013)

2018 CAV award. - Kim G. Larsen; Natarajan Shankar; Pierre Wolper; Somesh Jha (Formal Methods Syst. Des., 2021)