Publications of the Vasy team



This Page gives the list of publications of the VASY team (1996-2011).

Publications after January 2012 can be found from the CONVECS team publication page.

Additional references related to the CADP tools can be found from the CADP publication page.

Additional references related to the E-LOTOS language can be found from our E-LOTOS contribution page.


| 2011 | 2010 | 2009 | 2008 | 2007 | 2006 | 2005 | 2004 | 2003 | 2002 | 2001 | 2000 | 1999 | 1998 | 1997 | 1996 |

- 2011 -

Smart Reduction
Pepijn Crouzen and Frédéric Lang

March 2011, 15 pages.

CADP 2010: A Toolbox for the Construction and Analysis of Distributed Processes
Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe

March 2011, 15 pages.

Langages modernes pour la vérification des systèmes asynchrones
Damien Thivolle

April 2011.

Specifying and Verifying the SYNERGY Reconfiguration Protocol with LOTOS NT and CADP
Fabienne Boyer, Olivier Gruber, and Gwen Salaün

June 2011, 15 pages.

CTRL: Extension of CTL with Regular Expressions and Fairness Operators to Verify Genetic Regulatory Networks
Radu Mateescu, Pedro T. Monteiro, Estelle Dumas, and Hidde de Jong

July 2011, 65 pages.

Property-Dependent Reductions for the Modal Mu-Calculus
Radu Mateescu and Anton Wijs

July 2011, 30 pages.

Model Checking and Co-simulation of a Dynamic Task Dispatcher Circuit using CADP
Etienne Lantreibecq and Wendelin Serwe

August 2011, 16 pages.

Process Calculi: Bridges and Application to Distributed Systems
Gwen Salaün

November 2011.

Self-configuration of Legacy Distributed Applications in the Cloud
Xavier Etchevers, Thierry Coupaye, Fabienne Boyer, Noël de Palma, and Gwen Salaün

December 2011, 8 pages.

Also:



- 2010 -

Modélisation et analyse des performances de la bibliothèque MPI en tenant compte de l'architecture matérielle
Meriem Zidouni

May 2010, 200 pages.

Towards Performance Prediction of Compositional Models in GALS Designs
Nicolas Coste

June 2010, 223 pages.

A Study of Shared-Memory Mutual Exclusion Protocols using CADP
Radu Mateescu and Wendelin Serwe

September 2010, 18 pages.

Translating Pi-Calculus into LOTOS NT
Radu Mateescu and Gwen Salaün

October 2010, 16 pages.

Ten Years of Performance Evaluation for Concurrent Systems Using CADP
Nicolas Coste, Hubert Garavel, Holger Hermanns, Frédéric Lang, Radu Mateescu, and Wendelin Serwe

October 2010, 15 pages.

Translating FSP into LOTOS and Networks of Automata
Frédéric Lang, Gwen Salaün, Rémi Hérilier, Jeff Kramer, and Jeff Magee

November 2010, 34 pages.

Also:



- 2009 -

On the Semantics of Communicating Hardware Processes and their Translation into LOTOS for the Verification of Asynchronous Circuits with CADP
Hubert Garavel, Gwen Salaün, and Wendelin Serwe

January 2009, 35 pages.

Parallel Processes with Real-Time and Data: The ATLANTIF Intermediate Format
Jan Stoecker, Frédéric Lang, and Hubert Garavel

February 2009, 15/30 pages.

Hierarchical Adaptive State Space Caching based on Level Sampling
Radu Mateescu and Anton Wijs

March 2009, 15 pages.

Modeling Multiprocessor Cache Protocol Impact on MPI Performance
Ghassan Chehaibar, Meriem Zidouni, and Radu Mateescu

May 2009, 6 pages.

Les résultats du projet OpenEmbeDD
Charles André, Mariano Belaunde, Bernard Berthomieu, Christian Brunette, Agusti Canals, Hubert Garavel, Susanne Graf, Frederic Lang, Vincent Mahé, Michel Nakhlé, Rémi Schnekenburger, Robert De Simone, Jean-Pierre Talpin, François Vernadat

June 2009, 7 pages.

Towards Performance Prediction of Compositional Models in Industrial GALS Designs
Nicolas Coste, Holger Hermanns, Etienne Lantreibecq, and Wendelin Serwe

July 2009, 15 pages.

Verification of GALS Systems by Combining Synchronous Languages and Process Calculi
Hubert Garavel and Damien Thivolle

June 2009, 20 pages.

Verification of an Industrial SystemC/TLM Model using LOTOS and CADP
Hubert Garavel, Claude Helmstetter, Olivier Ponsini, and Wendelin Serwe

July 2009, 10 pages.

Survey on Directed Model Checking
Stefan Edelkamp, Viktor Schuppan, Dragan Bosnacki, Anton Wijs, Ansgar Fehnker, and Husain Aljazzar

July 2009, 23 pages.

Efficient On-the-Fly Computation of Weak Tau-Confluence
Radu Mateescu and Anton Wijs

July 2009, 42 pages.

Extending SPARQL with Temporal Logic
Radu Mateescu, Sébastien Meriot, and Sylvain Rampacek

October 2009, 16 pages.

TLM.OPEN: a SystemC/TLM Front-End for the CADP Verification Toolbox
Claude Helmstetter

October 2009, 9 pages.

Partial Order Reductions using Compositional Confluence Detection
Frederic Lang and Radu Mateescu

November 2009, 16 pages.

A Service-Oriented Architecture for Integrating the Modeling and Formal Verification of Genetic Regulatory Networks
Pedro T. Monteiro, Estelle Dumas, Bruno Besson, Radu Mateescu, Michel Page, Ana T. Freitas, and Hidde de Jong

December 2009, 12 pages.

An Intermediate Model for the Verification of Asynchronous Real-Time Embedded Systems: Definition and Application of the ATLANTIF Language
Jan Stoecker

December 2009, 306 pages.

Also:



- 2008 -

FIACRE: An Intermediate Language for Model Verification in the TopCased Environment
Bernard Berthomieu, Jean-Paul Bodeveix, Patrick Farail, Mamoun Filali, Hubert Garavel, Pierre Gaufillet, Frédéric Lang, and François Vernadat

January 2008, 8 pages.

Quantitative Evaluation in Embedded System Design: Validation of Multiprocessor Multithreaded Architectures
Nicolas Coste, Hubert Garavel, Holger Hermanns, Richard Hersemeule, Yvain Thonnart, and Meriem Zidouni

March 2008, 2 pages.

Specification and Analysis of Asynchronous Systems using CADP
Radu Mateescu

March 2008, 28 pages.

A Schedulerless Semantics of TLM Models Written in SystemC via Translation into LOTOS
Olivier Ponsini and Wendelin Serwe

May 2008, 16 pages.

A Model Checking Language for Concurrent Value-Passing Systems
Radu Mateescu and Damien Thivolle

May 2008, 16 pages.

A Comparison of Two SystemC/TLM Semantics for Formal Verification
Claude Helmstetter and Olivier Ponsini

June 2008, 10 pages.

Bisimulator 2.0: An On-the-Fly Equivalence Checker based on Boolean Equation Systems
Radu Mateescu and Emilie Oudot

June 2008, 2 pages.

Formal Modeling and Discrete-Time Analysis of BPEL Web Services
Radu Mateescu and Sylvain Rampacek

June 2008, 15 pages.

Temporal Logic Patterns for Querying Qualitative Models of Genetic Regulatory Networks
Pedro Tiago Monteiro, Delphine Ropers, Radu Mateescu, Ana Teresa Freitas, and Hidde de Jong

July 2008, 5 pages.

Improved On-the-Fly Equivalence Checking using Boolean Equation Systems
Radu Mateescu and Emilie Oudot

August 2008, 31 pages.

Temporal Logic Patterns for Querying Dynamic Models of Cellular Interaction Networks
Pedro Tiago Monteiro, Delphine Ropers, Radu Mateescu, Ana Teresa Freitas, and Hidde de Jong

September 2008, 20 pages.

Computation Tree Regular Logic for Genetic Regulatory Networks
Radu Mateescu, Pedro Tiago Monteiro, Estelle Dumas, and Hidde de Jong

October 2008, 53 pages.

Adaptation of Service Protocols using Process Algebra and On-the-Fly Reduction Techniques
Radu Mateescu, Pascal Poizat, and Gwen Salaün

December 2008, 16 pages.

Temporal Logic Patterns for Querying Dynamic Models of Cellular Interaction Networks
Pedro Tiago Monteiro, Delphine Ropers, Radu Mateescu, Ana Teresa Freitas, and Hidde de Jong

December 2008, 7 pages.

Is Timed Branching Bisimilarity a Congruence Indeed?
Wan Fokkink, Jun Pang, and Anton Wijs

December 2008, 25 pages.

Formal Modeling and Discrete-Time Analysis of BPEL Web Services
Radu Mateescu and Sylvain Rampacek

December 2008, 12 pages.


- 2007 -

Formal Verification of CHP Specifications with CADP - Illustration on an Asynchronous Network-on-Chip
Gwen Salaün, Wendelin Serwe, Yvain Thonnart, and Pascal Vivet

March 2007, 10 pages.

CADP 2006: A Toolbox for the Construction and Analysis of Distributed Processes
Hubert Garavel, Frédéric Lang, Radu Mateescu, and Wendelin Serwe

July 2007, 5 pages.

Translating FSP into LOTOS and Networks of Automata
Gwen Salaün, Jeff Kramer, Frédéric Lang, and Jeff Magee

July 2007, 21 pages.

Behavioral Adaptation of Component Compositions based on Process Algebra Encodings
Radu Mateescu, Pascal Poizat, and Gwen Salaün

November 2007, 25 pages.

Reflections on the Future of Concurrency Theory in General and Process Calculi in Particular
Hubert Garavel

December 2007, 16 pages.


- 2006 -

State Space Reduction for Process Algebra Specifications
Hubert Garavel and Wendelin Serwe

February 2006, 24 pages.

DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation
Hubert Garavel, Radu Mateescu, Damien Bergamini, Adrian Curic, Nicolas Descoubes, Christophe Joubert, Irina Smarandache-Sturm, and Gilles Stragier

March 2006, 5 pages.

Distributed On-the-Fly Model Checking and Test Case Generation
Christophe Joubert and Radu Mateescu

April 2006, 24 pages.

Bounded Analysis and Decomposition for Behavioural Descriptions of Components
Pascal Poizat, Jean-Claude Royer, and Gwen Salaün

June 2006, 15 pages.

Synchronizing Behavioural Mismatch in Software Composition
Carlos Canal, Pascal Poizat, and Gwen Salaün

June 2006, 15 pages.

CAESAR_SOLVE: A Generic Library for On-the-Fly Resolution of Alternation-Free Boolean Equation Systems
Radu Mateescu

July 2006, 39 pages.

Modélisation et analyse de systèmes asynchrones avec CADP
Radu Mateescu

July 2006, 31 pages.

Refined Interfaces for Compositional Verification
Frédéric Lang

September 2006, 22 pages.


- 2005 -

Distributed Local Resolution of Boolean Equation Systems
Christophe Joubert and Radu Mateescu

February 2005, 8 pages.

BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking
Damien Bergamini, Nicolas Descoubes, Christophe Joubert, and Radu Mateescu

April 2005, 5 pages.

Etude de l'environnement ouvert de developpement intégré Eclipse dans l'optique d'une extension
Nathalie Lépy

July 2005, 43 pages.

Analysis and Verification of Qualitative Models of Genetic Regulatory Networks: A Model-Checking Approach
Grégory Batt, Delphine Ropers, Hidde de Jong, Johannes Geiselmann, Radu Mateescu, Michel Page, and Dominique Schneider

July-August 2005, 6 pages.

Encoding Abstract Descriptions into Executable Web Services: Towards a Formal Development
Antonella Chirichiello and Gwen Salaün

September 2005, 25 pages.

EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, Compositional, and On-the-fly Verification Methods
Frédéric Lang

September 2005, 21 pages.

On-the-Fly State Space Reductions for Weak Equivalences
Radu Mateescu

September 2005, 10 pages.

Translating Hardware Process Algebras into Standard Process Algebras - Illustration with CHP and LOTOS
Gwen Salaün and Wendelin Serwe

September 2005, 25 pages.

Validation of Qualitative Models of Genetic Regulatory Networks by Model Checking: Analysis of the Nutritional Stress Response in Escherichia Coli
Grégory Batt, Delphine Ropers, Hidde de Jong, Johannes Geiselmann, Radu Mateescu, Michel Page, and Dominique Schneider

December 2005, 10 pages.

Vérification distribuée à la volée de grands espaces d´états
Christophe Joubert

December 2005, 172 pages.


- 2004 -

SEQ.OPEN: A Tool for Efficient Trace-Based Verification
Hubert Garavel and Radu Mateescu

April 2004, 6 pages.

Model Checking Genetic Regulatory Networks using GNA and CADP
Grégory Batt, Damien Bergamini, Hidde de Jong, Hubert Garavel, and Radu Mateescu

April 2004, 6 pages.

Abstracting Call-Stacks for Interprocedural Verification of Imperative Programs
Bertrand Jeannet and Wendelin Serwe

May 2004, 15/54 pages.

Model Checking for Software Architectures
Radu Mateescu

May 2004, 6 pages.

ArchWare: Architecting Evolvable Software
Flavio Oquendo, Brian Warboys, Ron Morrison, Régis Dindeleux, Ferdinando Gallo, Hubert Garavel, and Carmen Occhipinti

May 2004, 15 pages.

State Space Reduction for Process Algebra Specifications
Hubert Garavel and Wendelin Serwe

July 2004, 17 pages.

Distributed On-the-Fly Equivalence Checking
Christophe Joubert and Radu Mateescu

September 2004, 15 pages.


- 2003 -

A Set of Performance and Dependability Analysis Components for CADP
Holger Hermanns and Christophe Joubert

January 2003, 6 pages.

A Generic On-the-Fly Solver for Alternation-Free Boolean Equation Systems
Radu Mateescu

January 2003, 21 pages.

Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus
Radu Mateescu and Mihaela Sighireanu

March 2003, 32 pages.

On-the-Fly Verification using CADP
Radu Mateescu

June 2003, 5 pages.

Distributed Model Checking: From Abstract Algorithms to Concrete Implementations
Christophe Joubert

July 2003, 14 pages.

Calculating Tau-Confluence Compositionally
Gordon Pace, Frédéric Lang, and Radu Mateescu

September 2003, 23 pages.

Défense et illustration des algèbres de processus
Hubert Garavel

September 2003, 25 pages.

Compositional Verification Using CADP of the ScalAgent Deployment Protocol for Software Components
Frédéric Tronel, Frédéric Lang, and Hubert Garavel

November 2003, 28 pages.

Logiques temporelles basées sur actions pour la vérification des systèmes asynchrones
Radu Mateescu

December 2003, 39 pages.


- 2002 -

Vérification de circuits : problèmes et solutions - Exemple de TestBuilder
Gilles Badoil

March 2002, 30 pages.

Compositional Verification using SVL Scripts
Frédéric Lang

April 2002, 5 pages.

Compiler Construction using LOTOS NT
Hubert Garavel, Frédéric Lang, and Radu Mateescu

April 2002, 5 pages.

Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled Transition Systems
Radu Mateescu

April 2002, 36 pages.

An Embedded Language Framework for Hardware Compilation
Koen Claessen and Gordon Pace

April 2002, 16 pages.

SPeeDI - a Verification Tool for Polygonal Hybrid Systems
Evgueni Asarin, Gordon Pace, Gerardo Schneider, and Sergio Yovine

July 2002, 5 pages.

On Combining Functional Verification and Performance Evaluation using CADP
Hubert Garavel and Holger Hermanns

July 2002, 24 pages.

NTIF: A General Symbolic Model for Communicating Sequential Processes with Data
Hubert Garavel and Frédéric Lang

December 2002, 30 pages.


- 2001 -

Parallel State Space Construction for Model-Checking
Hubert Garavel, Radu Mateescu, and Irina Smarandache

March 2001, 20 pages.

Specification and Verification of a Dynamic Reconfiguration Protocol for Agent-Based Applications
Manuel Aguilar Cornejo, Hubert Garavel, Radu Mateescu, and Noel de Palma

July 2001, 32 pages.

SVL: a Scripting Language for Compositional Verification
Hubert Garavel and Frédéric Lang

July 2001, 36 pages.

An overview of CADP 2001
Hubert Garavel, Frédéric Lang, and Radu Mateescu

December 2001, 15 pages.


- 2000 -

Efficient Diagnostic Generation for Boolean Equation Systems
Radu Mateescu

January 2000, 23 pages.

Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus
Radu Mateescu and Mihaela Sighireanu

March 2000, 24 pages.

System Design of a CC-NUMA Multiprocessor Architecture using Formal Specification, Model-Checking, Co-Simulation, and Test Generation
Hubert Garavel, César Viho, and Massimo Zendri

November 2000, 36 pages.


- 1999 -

Verification of Temporal Properties of Processes in a Setting with Data
Jan Friso Groote and Radu Mateescu

January 1999, 17 pages.

Contribution à la Définition et à l'Implémentation du Langage E-LOTOS
Mihaela Sighireanu

January 1999, 300 pages.

Hardware Testing using a Communication Protocol Conformance Testing Tool
Hakim Kahlouche, César Viho, and Massimo Zendri

March 1999, 15 pages.

Model Checking for Managers
Wil Janssen, Radu Mateescu, Sjouke Mauw, Peter Fennema, and Petra van der Stappen

September 1999, 16 pages.

Advanced Modelling and Verification Techniques Applied to a Cluster File System
Charles Pecheur

October 1999, 8 pages.

A Graphical Parallel Composition Operator for Process Algebras
Hubert Garavel and Mihaela Sighireanu

October 1999, 18 pages.

Etude de la migration et de la portabilité des applications informatiques d'Unix vers Windows NT
Aldo Mazzilli

December 1999, 125 pages.


- 1998 -

OPEN/CAESAR: An Open Software Architecture for Verification, Simulation, and Testing
Hubert Garavel

March 1998, 18 pages.

Model-Checking Validation of the LOTOS Descriptions of the Invoicing Case Study
Mihaela Sighireanu

March 1998, 16 pages.

Vérification des propriétés temporelles des programmes parallèles
Radu Mateescu

April 1998, 274 pages.

Towards a Second Generation of Formal Description Techniques - Rationale for the Design of E-LOTOS
Hubert Garavel and Mihaela Sighireanu

May 1998, 28 pages.

Advanced Modelling and Verification Techniques Applied to a Cluster File System
Charles Pecheur

May 1998, 55 pages.

XTL: A Meta-Language and Tool for Temporal Logic Model-Checking
Radu Mateescu and Hubert Garavel

July 1998, 10 pages.

An Industrial Experiment in Automatic Generation of Executable Test Suites for a Cache Coherency Protocol
Hakim Kahlouche, César Viho, and Massimo Zendri

September 1998, 16 pages.

Local Model-Checking of an Alternation-Free Value-Based Modal Mu-Calculus
Radu Mateescu

September 1998, 8 pages.

Verifying Business Processes using SPIN
Wil Janssen, Radu Mateescu, Sjouke Mauw, and Jan Springintveld

November 1998, 16 pages.

Requirement Capture, Formal Description and Verification of an Invoicing System
Mihaela Sighireanu and Ken Turner

December 1998, 32 pages.


- 1997 -

CADP'97 - Status, Applications, and Perspectives
Hubert Garavel, Mark Jorgensen, Radu Mateescu, Charles Pecheur, Mihaela Sighireanu, and Bruno Vivien
June 1997, 6 pages.

Validation of the Link Layer Protocol of the IEEE-1394 Serial Bus (``FireWire''): an Experiment with E-LOTOS
Mihaela Sighireanu and Radu Mateescu

June 1997, 37 pages.

Specification and Verification of Various Distributed Leader Election Algorithms for Unidirectional Ring Networks
Hubert Garavel and Laurent Mounier

July 1997, 35 pages.

Specification and Verification of the CO4 Distributed Knowledge System Using LOTOS
Charles Pecheur

November 1997, 97 pages.

Etude et réalisation d'un compilateur E-LOTOS à l'aide du générateur de compilateurs SYNTAX/FNC-2
Bruno Vivien

December 1997, in French, 150 pages.


- 1996 -

Etude du système SYNTAX/FNC-2 pour la génération de compilateurs
Bruno Vivien

June 1996, in French, 54 pages.

Specification and Verification of the PowerScale Bus Arbitration Protocol: An Industrial Experiment with LOTOS
Ghassan Chehaibar, Hubert Garavel, Laurent Mounier, Nadia Tawbi, and Ferruccio Zulian
October 1996, 20 pages.


Version 1.144 - Date 2012/09/17 12:37:28
Back to the VASY Home Page