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:
Measuring the Compatibility of Service Interaction Protocols Realizability and Dynamic Reconfiguration of Chor Specifications Client Update: A Solution for Service Evolution On Checking the Compatibility of Service Interaction Protocols
Meriem Ouederni, Gwen Salaün, and Ernesto Pimentel
March 2011, 8 pages.
Nima Roohi and Gwen Salaün
March 2011, 11 pages.
Meriem Ouederni, Gwen Salaün, and Ernesto Pimentel
July 2011, 8 pages.
Meriem Ouederni
October 2011.
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:
Semi-automatic Specification of Behavioural Service Adaptation Contracts Tau Be or not Tau Be? - A Perspective on Service Compatibility and Substitutability PARAM: A Model Checker for Parametric Markov Models Concurrency and Composition in a Stochastic World Handling Data-Based Concurrency in Context-Aware Service Protocols Analysis and Verification of Service Interaction Protocols - A Brief Survey A Case Study in Model-Based Adaptation of Web Services Quantifying Service Compatibility: A Step Beyond the Boolean Approaches
Javier Cámara, José Antonio Martín, Gwen Salaün, Carlos Canal, and Ernesto Pimentel
March 2010, 15 pages.
Meriem Ouederni and Gwen Salaün
June 2010, 14 pages.
Ernst Moritz Hahn, Holger Hermanns, Björn Wachter, and Lijun Zhang
July 2010, 5 pages.
Christian Eisentraut, Holger Hermanns, and Lijun Zhang
August 2010, 19 pages.
Javier Cubo, Ernesto Pimentel, Gwen Salaün, and Carlos Canal
September 2010, 18 pages.
Gwen Salaün
September 2010, 12 pages.
Javier Cámara, José Antonio Martín, Gwen Salaün, Carlos Canal, and Ernesto Pimentel
October 2010, 15 pages.
Meriem Ouederni, Gwen Salaün, and Ernesto Pimentel
December 2010, 8 pages.
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:
SimSoC: A full System Simulation Software for Embedded Systems Full Simulation Coverage for SystemC Transaction-Level Models of Systems-on-a-Chip
Vania Joloboff, Claude Helmstetter, and Hui Xiao
September 2009, 7 pages.
Claude Helmstetter, Florence Maraninchi, and Laurent Maillet-Contoz
October 2009, 38 pages.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
Back to the VASY Home Page