@string{lncs = "Lecture Notes in Computer Science"}
@string{sv = "Springer"}
@string{tcs = "Theoretical Computer Science"}
@string{entcs = "Electronic Notes in Theoretical Computer Science"}
@string{eptcs = "Electronic Proceedings in Theoretical Computer Science"}
@string{nh = "North-Holland"}
@string{ch = "Chapman \& Hall"}
@string{siam = "SIAM Journal of Computing"}
@string{isdn = "Computer Networks and ISDN Systems"}
@string{cwi = "Centrum voor Wiskunde en Informatica"}

@inproceedings{Aguilar-Garavel-Mateescu-dePalma-01,

author =	{Manuel Aguilar Cornejo and Hubert Garavel and Radu Mateescu
		and No\"{e}l {de Palma}},
title =		{Specification and Verification of a Dynamic Reconfiguration
		Protocol for Agent-Based Applications},
booktitle =	{Proceedings of the 3rd IFIP WG 6.1 International Working
		Conference on Distributed Applications and Interoperable
		Systems (DAIS'01), Krakow, Poland},
year =		{2001},

editor =	{Aleksander Laurentowski and Jacek Kosinski and Zofia Mossurska
		and Radoslaw Ruchala},
publisher =	{Kluwer Academic Publishers},
pages =		{229--242},
month =		sep,
note =          {Full version available as INRIA Research Report~RR-4222},

annote =	{etude de cas avec SVL}
}

@inproceedings{Batt-Bergamini-deJong-et-al-04,

author =	{Gr\'egory Batt and Damien Bergamini and Hidde de Jong and
		Hubert Garavel and Radu Mateescu},
title =		{Model Checking Genetic Regulatory Networks using GNA and CADP},
booktitle =     {Proceedings of the 11th International SPIN Workshop on Model
		Checking of Software (SPIN'04), Barcelona, Spain},
year =		{2004},

editor =	{Susanne Graf and Laurent Mounier},
publisher =     sv,
series =        lncs,
volume =        {2989},
pages =		{156--161},
month =		apr,

annote = 	{connexion de GNA et CADP}
}

@inproceedings{Bergamini-Descoubes-Joubert-Mateescu-05,

author =	{Damien Bergamini and Nicolas Descoubes and Christophe Joubert
		and Radu Mateescu},
title =		{BISIMULATOR: A Modular Tool for On-the-Fly Equivalence
		Checking},
booktitle =	{Proceedings of the 11th International Conference on Tools and
		Algorithms for the Construction and Analysis of Systems
		(TACAS'05), Edinburgh, Scotland, UK},
year =		{2005},

editor =	{Nicolas Halbwachs and Lenore Zuck},
publisher =	sv,
series =	lncs,
volume =	{3440},
pages =		{581--585},
month =		apr,

annote = 	{description de BISIMULATOR}
}

@article{Bolognesi-Brinksma-87,

author =	{Tommaso Bolognesi and Ed Brinksma},
title =		{{Introduction to the ISO Specification Language LOTOS}},
journal =	isdn,
year =		{1988},

volume =	{14},
number =	{1},
pages =		{25--59},
month =		jan
}

@inproceedings{Boyer-Gruber-Salaun-11,

author =	{Fabienne Boyer and Olivier Gruber and Gwen Sala\"un},
title =		{{Specifying and Verifying the SYNERGY Reconfiguration
		Protocol with LOTOS~NT and CADP}},
booktitle =	{Proceedings of the 17th International Symposium on Formal
		Methods (FM'11), Limerick, Ireland},
year =		{2011},

editor =	{Michael Butler and Wolfram Schulte},
publisher =	sv,
series =	lncs,
volume =	{6664},
pages = 	{103--117},
month =		jun,

annote = 	{etude de cas Synergy}
}

@unpublished{Champelovier-Clerc-Garavel-et-al-10-v6.7,

author =	{David Champelovier and Xavier Clerc and Hubert Garavel and
		Yves Guerte and Christine McKinty and Vincent Powazny and
		Fr\'ed\'eric Lang and Wendelin Serwe and Gideon Smeding},
title =		{{Reference Manual of the LNT to LOTOS Translator
		(Version 6.7)}},
month =		jul,
year =		{2017},
note =		{{INRIA}, Grenoble, France},

annote =        {Manuel LNT version 6.7}
}

@inproceedings{Chehaibar-Garavel-Mounier-Tawbi-Zulian-96,

author =	{Ghassan Chehaibar and Hubert Garavel and Laurent Mounier and
		Nadia Tawbi and Ferruccio Zulian},
title =		{{Specification and Verification of the PowerScale Bus 
		Arbitration Protocol: An Industrial Experiment with LOTOS}},
booktitle =	{Proceedings of the IFIP Joint International Conference on
		Formal Description Techniques for Distributed Systems and 
		Communication Protocols, and Protocol Specification, Testing,
		and Verification (FORTE/PSTV'96), Kaiserslautern, Germany},
year =		{1996},

editor =	{Reinhard Gotzhein and Jan Bredereke},
pages =		{435--450},
publisher =	ch,
month =		oct,
note =		{Full version available as INRIA Research Report~RR-2958},

annote = 	{PowerScale}
}

@inproceedings{Chehaibar-Zidouni-Mateescu-09,

author =	{Ghassan Chehaibar and Meriem Zidouni and Radu Mateescu},
title =		{Modeling Multiprocessor Cache Protocol Impact on MPI
		Performance},
booktitle =	{Proceedings of the 2009 IEEE International Workshop on
		Quantitative Evaluation of Large-Scale Systems and
		Technologies {QuEST}'09 (Bradford, UK)},
year =		{2009},

publisher =	{IEEE Computer Society Press},
month =		may,


annote = 	{Etude de cas du benchmark ping-pong - Multival}
}

@inproceedings{Chirichiello-Salaun-05,

author =        {Antonella Chirichiello and Gwen Sala{\"u}n},
title =         {Encoding Abstract Descriptions into Executable Web Services:
		Towards a Formal Development},
booktitle =     {Proceedings of the IEEE/WIC/ACM International Conference on 
		Web Intelligence WI'05 (Compi{\`e}gne, France)},
year =          {2005},

publisher =	{IEEE Press},
pages =         {457--463},
month =         sep,

note =          {Extended version available as Technical Report 08-2005 of
		Universit{\`a} di Roma ``La Sapienza'' (DIS department)},

annote =        {Web services avec LOTOS et CADP}
}

@inproceedings{Coste-Garavel-Hermanns-et-al-08,

author =	{Nicolas Coste and Hubert Garavel and Holger Hermanns and
		Richard Hersemeule and Yvain Thonnart and Meriem Zidouni},
title =		{Quantitative Evaluation in Embedded System Design: Validation
		of Multiprocessor Multithreaded Architectures},
booktitle =	{Special Session at Design, Automation \& Test in Europe 
		 {DATE}'08 (Munich, Germany)},
year =		{2008},

month =		mar,

annote = 	{CADP, Multival}
}

@inproceedings{Coste-Garavel-Hermanns-et-al-10,

author =	{Nicolas Coste and Hubert Garavel and Holger Hermanns and
		Fr\'ed\'eric Lang and Radu Mateescu and Wendelin Serwe},
title =		{{Ten Years of Performance Evaluation for Concurrent Systems
		Using CADP}},
booktitle =	{Proceedings of the 4th International Symposium on Leveraging
		Applications of Formal Methods, Verification and Validation
		ISoLA 2010 (Amirandes, Heraclion, Crete), Part II},
year =		{2010},

editor =	{Tiziana Margaria and Bernhard Steffen},
publisher =	sv,
series =	lncs,
volume =	{6416},
pages = 	{128--142},
month =		oct,

annote =	{survey of CADP performance evaluation tools and case studies}
}

@inproceedings{Coste-Hermanns-Lantreibecq-Serwe-09,

author =	{Nicolas Coste and Holger Hermanns and Etienne Lantreibecq and
		Wendelin Serwe},
title =		{{Towards Performance Prediction of Compositional Models in
		Industrial GALS Designs}},
booktitle =	{Proceedings of the 21th International Conference on
		Computer Aided Verification (CAV'09), Grenoble, France},
year =		{2009},

editor =	{Ahmed Bouajjani and Oded Maler},
publisher =	sv,
series =	lncs,
volume =	{5643},
pages =		{204--218},
month =		jul,

annote = 	{}
}

@inproceedings{Crouzen-Lang-11,

author =	{Pepijn Crouzen and Fr\'ed\'eric Lang},
title =		{{Smart Reduction}},
booktitle =	{Proceedings of Fundamental Approaches to Software Engineering
		(FASE'11), Saarbr\"ucken, Germany},
year =		{2011},

editor =	{Dimitra Giannakopoulou and Fernando Orejas},
publisher =	sv,
series =	lncs,
volume =	{6603},
pages =		{111--126},
month =		mar,

annote =	{operateur smart reduction de SVL}
}

@article{DeMeer-Roth-Vuong-92,

author =	{Jan de Meer and Rudolf Roth and Son Vuong},
title =		{{Introduction to Algebraic Specifications Based on the
		 Language ACT ONE}},
journal =	isdn,
year =		{1992},

volume =	{23},
number =	{5},
pages =		{363--392},

annote =	{presentation de ACT ONE}
}

@inproceedings{Etchevers-Coupaye-Boyer-et-al-11,

author =	{Xavier Etchevers and Thierry Coupaye and Fabienne Boyer and
		No\"{e}l {de Palma} and Gwen Sala\"{u}n},
title =		{{Self-configuration of Legacy Distributed Applications in the
		Cloud}},
booktitle =	{Proceedings of the 4th IEEE/ACM International Conference on
		Utility and Cloud Computing (UCC'12), Melbourne, Australia},
year =		{2011},

month =		dec,

annote = 	{etude de cas avec CADP/LNT}
}

@inproceedings{Evrard-Lang-13,

author =	{Hugues Evrard and Fr\'ed\'eric Lang},
title =		{{Formal Verification of Distributed Branching Multiway
		Synchronization Protocols}},
booktitle =	{Proceedings of the IFIP Joint International Conference on
		Formal Techniques for Distributed Systems (FORTE/FMOODS'13),
		Florence, Italy},
year =		{2013},

editor =	{Dirk Beyer and Michele Boreale},
publisher =	sv,
series =	lncs,
volume =	{7892},
pages = 	{146--160},
month =		jun,

annote =	{verification du protocole de Sjodin implemente dans DLC}
}

@inproceedings{Evrard-Lang-15,

author =	{Hugues Evrard and Fr\'ed\'eric Lang},
title =		{{Automatic Distributed Code Generation from Formal Models
		of Asynchronous Concurrent Processes}},
booktitle =	{Proceedings of the 23rd Euromicro International Conference
		on Parallel, Distributed and Network-based Processing --
		Special Session on Formal Approaches to Parallel and
		Distributed Systems (PDP/4PAD'15), Turku, Finland},
year =		{2015},

editor =	{Marco Aldinucci and Masoud Daneshtalab and Ville Lepp\"{a}nen
		and Johan Lilius},
publisher =	{IEEE Computer Society Press},
pages =		{459--466},
month =		mar,

annote =	{Presentation de l'outil DLC}
}

@article{Evrard-Lang-17,

author =	{Hugues Evrard and Fr\'ed\'eric Lang},
title =		{{Automatic Distributed Code Generation from Formal Models of
		Asynchronous Processes Interacting by Multiway Rendezvous}},
journal =	{Journal of Logical and Algebraic Methods in Programming},
year =		{2017},

publisher =	{Elsevier},
volume =	{88},
pages =		{121--153},

annote =	{DLC}
}

@phdthesis{Fernandez-88,

author =	{Jean-Claude Fernandez},
school =	{Universit\'e Joseph~Fourier (Grenoble)},
title =		{{ALDEBARAN~: un syst\`eme de v\'erification par r\'eduction
		de processus communicants}},
type =		{{Th\`ese de Doctorat}},
year =		{1988},
month =		may
}

@techreport{Fernandez-89-a,

author =	{Jean-Claude Fernandez},
title =		{{ALDEBARAN: A Tool for Verification of Communicating
		Processes}},
institution =	{Laboratoire de G\'enie Informatique -- Institut IMAG},
year =		{1989},

type =		{Rapport SPECTRE},
number =	{C14},
address =	{Grenoble},
month =		sep
}

@manual{Fernandez-89-b,

title =		{{ALDEBARAN: User's Manual}},

author =	{Jean-Claude Fernandez},
organization =	{Laboratoire de G\'enie Informatique -- Institut IMAG},
address =	{Grenoble},
month =		jan,
year =		{1989},

annote =        {ALDEBARAN, obsolete}
}

@article{Fernandez-90,

author =	{Jean-Claude Fernandez},
title =		{{An Implementation of an Efficient Algorithm for Bisimulation
		Equivalence}},
journal =	scp,
year =		{1990},

volume =	{13},
number =	{2--3},
pages =		{219--236},
month =		may,

annote =	{presentation d'ALDEBARAN}
}

@inproceedings{Fernandez-Mounier-90,

author =	{Jean-Claude Fernandez and Laurent Mounier},
title =		{{Verifying Bisimulations ``On the Fly''}},
booktitle =	{Proceedings of the 3rd International Conference on Formal
		Description Techniques (FORTE'90), Madrid, Spain},
year =		{1990},

editor =	{Juan Quemada and Jos\'e Manas and Enrique V\'azquez},
publisher =	nh,
month =		nov
}

@inproceedings{Fernandez-Mounier-91-a,

author =	{Jean-Claude Fernandez and Laurent Mounier},
title =		{{``On the Fly'' Verification of Behavioural Equivalences and
		Preorders}},
booktitle =	{Proceedings of the 3rd Workshop on Computer-Aided
		Verification (CAV'91), Aalborg, Denmark},
year =		{1991},

editor =	{Kim G. Larsen and A. Skou},
publisher =	sv,
series =	lncs,
volume =	{575},
pages =		{181--191},
month = 	jul,

annote = {}
}

@inproceedings{Fernandez-Mounier-91-b,
 
author =	{Jean-Claude Fernandez and Laurent Mounier},
title =		{{A Tool Set for Deciding Behavioral Equivalences}},
booktitle =	{Proceedings of CONCUR'91, Amsterdam, The Netherlands},
year =		{1991},
 
month = 	aug
}

@techreport{Fernandez-Mounier-95,

author =	{Jean-Claude Fernandez and Laurent Mounier},
title =		{{A Local Checking Algorithm for Boolean Equation Systems}},
institution =	{VERIMAG},
year =		{1995},

type =		{Rapport SPECTRE},
number =	{95-07},
address =	{Grenoble},
month =		mar,

annote =	{papier sur EVALUATOR}
}

@inproceedings{Fernandez-Garavel-Mounier-Rasse-Rodriguez-Sifakis-91,

author =	{Jean-Claude Fernandez and Hubert Garavel and Laurent Mounier
		and Anne Rasse and Carlos Rodr\'{\i}guez and Joseph Sifakis},
title =		{Une bo\^{\i}te \`a outils pour la v\'erification de programmes
		LOTOS},
booktitle =	{Actes du Colloque Francophone pour l'Ing\'enierie des 
		Protocoles (CFIP'91), Pau, France},
year =		{1991},

editor =	{Omar Rafiq},
pages =		{479--500},
publisher =	{Herm\`es},
address =	{Paris},
month =		sep,

annote =	{presentation de la boite a` outils}
}

@inproceedings{Fernandez-Garavel-Mounier-Rasse-Rodriguez-Sifakis-92,

author =	{Jean-Claude Fernandez and Hubert Garavel and Laurent Mounier
		and Anne Rasse and Carlos Rodr\'{\i}guez and Joseph Sifakis},
title =		{{A Toolbox for the Verification of LOTOS Programs}},
booktitle =	{Proceedings of the 14th International Conference on
		Software Engineering (ICSE'14), Melbourne, Australia},
year =		{1992},

editor =	{Lori A. Clarke},
pages =		{246--259}, 
publisher =	{ACM},
month =		may,

annote =	{presentation de la boite a outils}
}

@inproceedings{Fernandez-Garavel-Kerbrat-Mounier-Mateescu-Sighireanu-96,

author =	{Jean-Claude Fernandez and Hubert Garavel and Alain Kerbrat
		and Radu Mateescu and Laurent Mounier and Mihaela Sighireanu},
title =		{{CADP (C{\AE}SAR/ALDEBARAN Development Package):
		A Protocol Validation and Verification Toolbox}},
booktitle =	{Proceedings of the 8th Conference on Computer-Aided 
		Verification (CAV'96), New Brunswick, New Jersey, USA},
year =		{1996},

editor =	{Rajeev Alur and Thomas A. Henzinger},
publisher =	sv,
series =	lncs,
volume =        {1102},
pages =		{437--440},
month =		aug,

annote = 	{presentation de la boite a outils}
}

@inproceedings{Fernandez-Jard-Jeron-Nedelka-Viho-96-a,

author =	{Jean-Claude Fernandez and Claude Jard and Thierry J\'eron
		and Laurence Nedelka and C\'esar Viho},
title = 	{Using On-the-Fly Verification Techniques for the Generation 
		of Test Suites},
booktitle =	{Proceedings of the 8th International Conference on 
		Computer-Aided Verification (Rutgers University, New
		Brunswick, NJ, USA)},
year =		{1996},

editor =	{R. Alur and T. A. Henzinger},
publisher =	sv,
series =	lncs,
volume =	{1102},
pages = 	{348--359},
month = 	aug,
note =		{Also available as INRIA Research Report~RR-2987},

annote =	{TGV-1}
}

@article{Fernandez-Jard-Jeron-Nedelka-Viho-96-b,

author =	{Jean-Claude Fernandez and Claude Jard and Thierry J\'eron
		and Laurence Nedelka and C\'esar Viho},
title = 	{An Experiment in Automatic Generation of Test Suites for 
		Protocols with Verification Technology},
journal = 	scp,
year = 		{1997},

editor =	{Jan-Friso Groote and Martin Rem},
volume =	{29},
number =	{1--2},
pages =		{123--146},
month =		jul,

note = 		{Special issue on Industrially Relevant Applications of Formal
		Analysis Techniques. Also available as INRIA Research 
		Report~RR-2923},

annote =	{TGV-2}
}

@inproceedings{Fernandez-Kerbrat-Mounier-93,

author =	{Jean-Claude Fernandez and Alain Kerbrat and Laurent Mounier},
title = 	{{Symbolic Equivalence Checking}},
booktitle =	{Proceedings of the 5th Workshop on Computer-Aided  
		Verification (CAV'93), Heraklion, Greece},
year =		{1993},

editor =	{Costas Courcoubetis},
publisher =	sv,
volume =	{697},
series =	lncs,
month = 	jun,

annote =	{Implementation de l'algo MMG avec des BDD}
}

@techreport{Fidge-94,

author =	{Colin Fidge},
title =		{A Comparative Introduction to CSP, CCS and LOTOS},
institution =	{Software Verification Research Centre, Department of Computer
		Science, University of Queensland},
year =		{1994},

type =		{TR},
number =	{93-24},
address =	{Queensland 4072, Australia},
month =		apr,

annote =	{}
}

@phdthesis{Garavel-89-b,

author =	{Hubert Garavel},
school =	{Universit\'e Joseph~Fourier (Grenoble)},
title =		{{Compilation et v\'erification de programmes LOTOS}},
type =		{{Th\`ese de Doctorat}}, 
year =		{1989},
month =		nov,

annote =	{presentation de CAESAR}
}

@inproceedings{Garavel-89-c,

author =	{Hubert Garavel},
title =		{{Compilation of LOTOS Abstract Data Types}},
booktitle =	{Proceedings of the 2nd International Conference on Formal
		Description Techniques {FORTE}'89 (Vancouver B.C., Canada)},
year =		{1989},

editor =	{Son T. Vuong},
pages =		{147--162},
publisher =	nh,
month =		dec,

annote =	{presentation de CAESAR.ADT}
}

@techreport{Garavel-90-a,

author =	{Hubert Garavel},
title =		{C{\AE}SAR Reference Manual},
institution =	{Laboratoire de G\'enie Informatique -- Institut IMAG},
year =		{1990},

type =		{Rapport SPECTRE},
number =	{C18},
address =	{Grenoble},
month =		nov
}

@article{Garavel-90-b,

author =	{Hubert Garavel},
title =		{Introduction au langage LOTOS},
journal =	{Revue de l'Association des Anciens El\`eves de l'ENSIMAG},
year =		{1990}

}

@techreport{Garavel-92-a,

author =	{Hubert Garavel},
title =		{The OPEN/C{\AE}SAR Reference Manual},
institution =	{Laboratoire de G\'enie Informatique -- Institut IMAG},
year =		{1992},

type =		{Rapport SPECTRE},
number =	{C33},
address =	{Grenoble},
month =		may,
annote =	{version 1.0}
}

@inproceedings{Garavel-95-a,

author =	{Hubert Garavel},
title =		{{On the Introduction of Gate Typing in E-LOTOS}},
booktitle =	{Proceedings of the 15th IFIP International Workshop on 
		 Protocol Specification, Testing and Verification (PSTV'95),
		 Warsaw, Poland},
year =		{1995},

editor =	{Piotr Dembinski and  Marek Sredniawa},
pages =		{283--298},
publisher =	ch,
month =		jun,

annote =	{portes typees en E-LOTOS}
}

@inproceedings{Garavel-96,

author =	{Hubert Garavel},
title =		{{An Overview of the Eucalyptus Toolbox}},
booktitle =     {Proceedings of the COST 247 International Workshop on Applied 
		Formal Methods in System Design (Maribor, Slovenia)},
year =		{1996},

editor =	{Z. Brezo\v{c}nik and T. Kapus},
pages =         {76--88},
publisher =     {University of Maribor, Slovenia},
month =         jun,

annote =        {EUCALYPTUS, Eucalyptus-2}
}

@inproceedings{Garavel-98,

author =	{Hubert Garavel},
title =		{{OPEN/C{\AE}SAR: An Open Software Architecture for 
		Verification, Simulation, and Testing}},
booktitle =	{Proceedings of the 4th International Conference on Tools
		and Algorithms for the Construction and Analysis of Systems
		(TACAS'98), Lisbon, Portugal},
year =		{1998},

editor =	{Bernhard Steffen},
publisher =     sv,
series =        lncs,
volume =        {1384},
pages =         {68--84},
month =         mar,

note =          {Full version available as INRIA Research Report~RR-3352},

annote = 	{OPEN/CAESAR}
}

@inproceedings{Garavel-03,

author =	{Hubert Garavel},
title =		{D\'efense et illustration des alg\`ebres de processus},
booktitle =	{Actes de l'Ecole d'\'et\'e Temps R\'eel ETR 2003 (Toulouse,
		France)},
year =		{2003},

editor =	{Zoubir Mammeri},
publisher =	{Institut de Recherche en Informatique de Toulouse},
month =		sep,

annote = 	{}
}

@inproceedings{Garavel-07,

author =	{Hubert Garavel},
title =		{{Reflections on the Future of Concurrency Theory in General
		and Process Calculi in Particular}},
booktitle =	{Proceedings of the LIX Colloquium on Emerging Trends in
		Concurrency Theory, Ecole Polytechnique de Paris, France,
		November 13--15, 2006},
year =		{2008},

series =	entcs,
volume =	{209},
pages =		{149--164},
publisher =     {Elsevier Science Publishers},
editor =	{Catuscia Palamidessi and Frank D. Valencia},
month =		apr,

note =          {Also available as INRIA Research Report~RR-6368},

annote = 	{applied concurrency theory}
}

@article{Garavel-15-b,

author =        {Hubert Garavel},
title =         {{Revisiting Sequential Composition in Process Calculi}},
journal =       {Journal of Logical and Algebraic Methods in Programming},
year =          {2015},
volume =	{84},
number =	{6},
pages =		{742--762},
month =         nov,

annote =	{LNT}
}

@article{Garavel-19,

author =        {Hubert Garavel},
title =         {{Nested-Unit Petri Nets}},
journal =       {Journal of Logical and Algebraic Methods in Programming},
year =          {2019},
volume =	{104},
pages =		{60--85},
month =         apr,

annote =	{NUPN}
}

@inproceedings{Garavel-Hautbois-93,

author =	{Hubert Garavel and Ren\'e-Pierre Hautbois},
title =		{{An Experiment with the Formal Description in LOTOS of the 
		 Airbus A340 Flight Warning Computer}},
booktitle =	{First AMAST International Workshop on Real-Time Systems,
		Iowa City, Iowa, USA},
year =		{1993},

editor =	{Maurice Nivat and Charles Rattray and Teodor Rus and 
		Giuseppe Scollo},
month =		nov,

annote =	{}
}

@inbook{Garavel-Hautbois-94,

author =	{Hubert Garavel and Ren\'e-Pierre Hautbois},
title =		{Experimenting LOTOS in Aerospace Industry},
editor =	{Teodor Rus and Charles Rattray},
booktitle =	{Theories and Experiences for Real-Time System Development},
chapter =	{11},
publisher =	{World Scientific},
year =		{1994},

volume =	{2},
series =	{AMAST Series in Computing},

annote =	{}
}

@inproceedings{Garavel-Helmstetter-Ponsini-Serwe-09,

author =	{Hubert Garavel and Claude Helmstetter and Olivier Ponsini and
		Wendelin Serwe},
title =		{Verification of an Industrial SystemC/TLM Model using LOTOS and
		CADP},
booktitle =	{Proceedings of the 7th ACM-IEEE International Conference
		on Formal Methods and Models for Codesign (MEMOCODE'09),
                Cambridge, MA, USA},
year =		{2009},

publisher =	{IEEE Computer Society Press},
month =		jun,


annote =	{etude de cas du Blitter}
}

@inproceedings{Garavel-Hermanns-02,

author =	{Hubert Garavel and Holger Hermanns},
title =		{{On Combining Functional Verification and Performance 
		Evaluation using CADP}},
booktitle =	{Proceedings of the 11th International Symposium of Formal
		Methods Europe (FME'02), Copenhagen, Denmark},
year =		{2002},

editor =	{Lars-Henrik Eriksson and Peter A. Lindsay},
publisher =	sv,
series = 	lncs,
volume = 	{2391},
pages =		{410--429},
month =		jul,

note = 		{Full version available as INRIA Research Report 4492},

annote = 	{CADP pour l'evaluation de performances}
}

@inproceedings{Garavel-Jorgensen-Mateescu-Pecheur-Sighireanu-Vivien-97,

author =	{Hubert Garavel and Mark Jorgensen and Radu Mateescu and
		Charles Pecheur and Mihaela Sighireanu and Bruno Vivien},
title =		{CADP'97 -- Status, Applications and Perspectives},
booktitle =     {Proceedings of the 2nd COST 247 International Workshop on
		Applied Formal Methods in System Design (Zagreb, Croatia)},
editor =	{Ignac Lovrek},
year =          {1997},
month =         jun,

annote = 	{CADP 97}
}

@inproceedings{Garavel-Lang-01,

author =	{Hubert Garavel and Fr\'ed\'eric Lang},
title =		{{SVL: a Scripting Language for Compositional Verification}},
booktitle =	{Proceedings of the 21st IFIP WG 6.1 International Conference
                 on Formal Techniques for Networked and Distributed Systems
                 (FORTE'01), Cheju Island, Korea},
year =		{2001},
editor =	{Myungchul Kim and Byoungmoon Chin and Sungwon Kang and 
		Danhyung Lee},
pages =	        {377--392},
publisher =	{Kluwer Academic Publishers},
month =		aug,
note =		{Full version available as INRIA Research Report~RR-4223},

annote = 	{Presentation of the SVL language and compiler}
}

@inproceedings{Garavel-Lang-02,

author =      {Hubert Garavel and Fr\'ed\'eric Lang},
title =       {{NTIF: A General Symbolic Model for Communicating Sequential 
	      Processes with Data}},
booktitle =   {Proceedings of the 22nd IFIP WG 6.1 International Conference on
	      Formal Techniques for Networked and Distributed Systems
              (FORTE'02), Houston, TX, USA},
year =        2002,

editor =      {Doron Peled and Moshe Vardi},
publisher =   sv,
series =      lncs,
volume =      {2529},
pages =       {276--291},
month =       nov,
note =	      {Full version available as INRIA Research Report~RR-4666},

annote =      {Presentation of NTIF concepts}
}

@article{Garavel-Lang-Mateescu-01,

author =	{Hubert Garavel and Fr\'ed\'eric Lang and Radu Mateescu},
title =		{An Overview of CADP 2001},
journal = 	{European Association for Software Science and Technology
		(EASST) Newsletter},
year = 		{2002},

volume =	{4},
pages =		{13--24},
month =		aug,

note =		{Also available as INRIA Technical Report~RT-0254
		(December 2001)},

annote =	{CADP 2001 "Ottawa"}
}

@inproceedings{Garavel-Lang-Mateescu-02,

author =        {Hubert Garavel and Fr\'ed\'eric Lang and Radu Mateescu},
title =         {{Compiler Construction using LOTOS NT}},
booktitle =     {Proceedings of the 11th International Conference on Compiler
                Construction (CC'02), Grenoble, France},
year =          {2002},

editor =        {R. Nigel Horspool},
publisher =	sv,
series =        lncs,
volume =        {2304},
pages =		{9--13},
month =		apr,

annote =	{Utilisation de LOTOS NT/TRAIAN pour construction compilateurs}
}

@article{Garavel-Lang-Mateescu-15,

author =	{Hubert Garavel and Fr\'ed\'eric Lang and Radu Mateescu},
title =		{{Compositional Verification of Asynchronous Concurrent
		Systems Using CADP}},
journal =	{Acta Informatica},
year =		2015,

volume =	{52},
number =	{4},
pages =		{337--392},
month =		apr,

annote =	{Article de synthese sur les techniques de verification
		compositionnelle dans CADP}
}

@inproceedings{Garavel-Lang-Mateescu-Serwe-07,

author =	{Hubert Garavel and Fr\'ed\'eric Lang and Radu Mateescu
		and Wendelin Serwe},
title =		{CADP 2006: A Toolbox for the Construction and Analysis
		of Distributed Processes},
booktitle =	{Proceedings of the 19th International Conference on
		Computer Aided Verification (CAV'07), Berlin, Germany},
year =		{2007},

editor =	{Werner Damm and Holger Hermanns},
publisher =	sv,
series =	lncs,
volume =	{4590},
pages =		{158--163},
month =		jul,

annote = 	{CADP 2006}
}

@inproceedings{Garavel-Lang-Mateescu-Serwe-11,

author =	{Hubert Garavel and Fr\'ed\'eric Lang and Radu Mateescu
		and Wendelin Serwe},
title =		{CADP 2010: A Toolbox for the Construction and Analysis
		of Distributed Processes},
booktitle =	{Proceedings of the 17th International Conference on
		Tools and Algorithms for the Construction and Analysis of
		Systems (TACAS'11), Saarbr\"ucken, Germany},
year =		{2011},

editor =	{Parosh A. Abdulla and {K. Rustan M.} Leino},
publisher =	sv,
series =	lncs,
volume =	{6605},
pages =		{372--387},
month =		mar,

annote = 	{CADP 2010}
}

@article{Garavel-Lang-Mateescu-Serwe-13,

author =	{Hubert Garavel and Fr\'ed\'eric Lang and Radu Mateescu
		 and Wendelin Serwe},
title =		{{CADP 2011: A Toolbox for the Construction and Analysis
		 of Distributed Processes}},
journal = 	{Springer International Journal on Software Tools for
		 Technology Transfer (STTT)},
year = 		{2013},

volume =	{15},
number =	{2},
pages =		{89--107},
month =		apr,


annote = 	{CADP 2011}
}

@inproceedings{Garavel-Lang-Mounier-18,

author =	{Hubert Garavel and Fr\'ed\'eric Lang and Laurent Mounier},
title =		{{Compositional Verification in Action}},
editor =	{Falk Howar and Jiri Barnat},
booktitle =	{Proceedings of the 23rd International Conference on Formal
		 Methods for Industrial Critical Systems (FMICS'18), Maynooth,
		 Ireland -- Essays Dedicated to Susanne Graf at the Occasion
		 of Her 60th Birthday},

publisher =	sv,
series =	lncs,
volume =	{11119},
pages =         {189--210},
year =		{2018},
month =		sep,

annote = 	{Festschrift, Gschrift}
}

@inproceedings{Garavel-Lang-Serwe-17,

author =	{Hubert Garavel and Fr\'ed\'eric Lang and Wendelin Serwe},
title = 	{{From LOTOS to LNT}},
booktitle =     {ModelEd, TestEd, TrustEd -- Essays Dedicated to Ed Brinksma 
		 on the Occasion of His 60th Birthday},
year =		{2017},

editor =	{Joost-Pieter Katoen and Rom Langerak and Arend Rensink},
publisher =     sv,
series =        lncs,
volume =        {10500},
pages =		{3--26},
month =		oct,

annote = 	{LNT}
}

@inproceedings{Garavel-Mateescu-Bergamini-et-al-06,

author =	{Hubert Garavel and Radu Mateescu and Damien Bergamini and
		Adrian Curic and Nicolas Descoubes and Christophe Joubert and
		Irina Smarandache-Sturm and Gilles Stragier},
title =		{DISTRIBUTOR and BCG\_MERGE: Tools for Distributed Explicit
		State Space Generation},
booktitle =	{Proceedings of the 12th International Conference on Tools and
		Algorithms for the Construction and Analysis of Systems
		(TACAS'06), Vienna, Austria},
year =		{2006},

editor =	{Holger Hermanns and Jens Palberg},
publisher =	sv,
series =	lncs,
volume =	{3920},
pages =		{445--449},
month =		mar # "--" # apr,

annote = 	{description de DISTRIBUTOR et BCG\_MERGE}
}

@article{Garavel-Mateescu-Serwe-12,

author =	{Hubert Garavel and Radu Mateescu and Wendelin Serwe},
title =		{{Large-scale Distributed Verification using CADP: Beyond
		Clusters to Grids}},
journal = 	entcs,
year = 		{2013},

volume =	{296},
pages =		{145--161},
month =		aug,


annote = 	{PBG_OPEN}
}

@inproceedings{Garavel-Mateescu-Smarandache-01,

author =	{Hubert Garavel and Radu Mateescu and Irina Smarandache},
title =		{Parallel State Space Construction for Model-Checking},
booktitle =	{Proceedings of the 8th International SPIN Workshop on Model
		Checking of Software (SPIN'01), Toronto, Canada},
year =		{2001},

editor =	{Matthew B. Dwyer},
publisher =	sv,
series =        lncs,
volume =        {2057},
pages =		{217--234},
month =		may,
note =		{Revised version available as INRIA Research Report~RR-4341
		(December 2001)},

annote = 	{Article sur DISTRIBUTOR V1}
}

@inproceedings{Garavel-Mateescu-04,

author =	{Hubert Garavel and Radu Mateescu},
title =		{SEQ.OPEN: A Tool for Efficient Trace-Based Verification},
booktitle =     {Proceedings of the 11th International SPIN Workshop on Model
		Checking of Software (SPIN'04), Barcelona, Spain},
year =		{2004},

editor =	{Susanne Graf and Laurent Mounier},
publisher =     sv,
series =        lncs,
volume =        {2989},
pages =		{150--155},
month =		apr,

annote = 	{description de SEQ.OPEN}
}

@inproceedings{Garavel-Mateescu-19,

author =	{Hubert Garavel and Radu Mateescu},
title = 	{{Reflections on Bernhard Steffen's Physics of Software Tools}},
booktitle =	{Models, Mindsets, Meta: The What, the How, and the Why Not?},
year =		{2019},

editor =	{Tiziana Margaria and Susanne Graf and Kim Larsen},
publisher =	sv,
series =	lncs,
volume =	{11200},
pages =		{186--207},
month =		jun,

annote = 	{CADP and other tools}
}

@article{Garavel-Mounier-96,

author =	{Hubert Garavel and Laurent Mounier},
title =		{{Specification and Verification of Various Distributed Leader 
		Election Algorithms for Unidirectional Ring Networks}},
journal = 	scp,
year = 		{1997},

editor =	{Jan-Friso Groote and Martin Rem},
volume =	{29},
number =	{1--2},
pages =		{171--197},
month =		jul,

note = 		{Special issue on Industrially Relevant Applications of Formal
		Analysis Techniques. Full version available as INRIA Research 
		Report~RR-2986},

annote =	{Token ring}
}

@techreport{Garavel-Rodriguez-90,

author =	{Hubert Garavel and Carlos Rodr\'{\i}guez},
title =		{An Example of LOTOS Specification: The Matrix Switch Problem},
institution =	{Laboratoire de G\'enie Informatique -- Institut IMAG},
year =		{1990},

type =		{Rapport SPECTRE},
number =	{C22},
address =	{Grenoble},
month =		jun,

annote =	{Un exemple de specification en LOTOS}
}

@article{Garavel-Salaun-Serwe-09,

author =	{Hubert Garavel and Gwen Sala\"un and Wendelin Serwe},
title =		{{On the Semantics of Communicating Hardware Processes and
		their Translation into LOTOS for the Verification of
		Asynchronous Circuits with CADP}},
journal = 	{Science of Computer Programming},
year = 		{2009},

volume =	{74},
number =	{3},
pages =		{100--127},
month =		jan,


annote =	{CHP2LOTOS}
}

@inproceedings{Garavel-Serwe-04,

author =	{Hubert Garavel and Wendelin Serwe},
title =		{{State Space Reduction for Process Algebra Specifications}},
booktitle =	{Proceedings of the 10th International Conference on Algebraic
		Methodology and Software Technology (AMAST'04), Stirling,
		Scotland, UK},
year =		{2004},

editor =	{Charles Rattray and Savitri Maharaj and Carron Shankland},
publisher =	sv,
series =	lncs,
volume =	{3116},
pages =		{164--180},
month =		jul,

annote = 	{remise a zero amelioree des variables dans CAESAR}
}

@article{Garavel-Serwe-06,

author =	{Hubert Garavel and Wendelin Serwe},
title =		{{State Space Reduction for Process Algebra Specifications}},
journal =	tcs,
year =		{2006},

volume =	{351},
number =	{2},
pages =		{131--145},
month =		feb,

annote =	{remise a zero amelioree des variables dans CAESAR}
}

@inproceedings{Garavel-Sifakis-90,

author =	{Hubert Garavel and Joseph Sifakis},
title =		{{Compilation and Verification of LOTOS Specifications}},
booktitle =	{Proceedings of the 10th IFIP International Symposium on
		Protocol Specification, Testing and Verification (PSTV'90),
		Ottawa, Canada},
year =		{1990},

editor =	{L. Logrippo and R. L. Probert and H. Ural},
pages =		{379--394},
publisher =	nh,
month =		jun,

annote =	{Presentation de CAESAR}
}

@techreport{Garavel-Sighireanu-95-a,
author =	{Hubert Garavel and Mihaela Sighireanu},
title =		{Defect Report concerning ISO Standard 8807 and Proposal for a 
		 Correct Flattening of LOTOS Parameterized Types},
institution =	{VERIMAG},
year =		{1995},

type =		{Rapport SPECTRE},
number =	{95-11},
address =	{Grenoble},
month =		jul,
note =		{{I}nput Document [OTT6] to the ISO/IEC JTC1/SC21/WG7 Meeting
		on Enhancements to LOTOS (1.21.20.2.3), Ottawa (Canada),
		July 20--26, 1995}
}

@inproceedings{Garavel-Sighireanu-96-a,

author =        {Hubert Garavel and Mihaela Sighireanu},
title =         {{On the Introduction of Exceptions in LOTOS}},
booktitle =	{Proceedings of the IFIP Joint International Conference on
		Formal Description Techniques for Distributed Systems and 
		Communication Protocols, and Protocol Specification, Testing,
		and Verification (FORTE/PSTV'96), Kaiserslautern, Germany},
year =		{1996},

editor =	{Reinhard Gotzhein and Jan Bredereke},
pages =		{469--484},
publisher =	ch,
month =		oct,

annote =        {Rapport Recherche INRIA containing all proofs of trap}
}

@inproceedings{Garavel-Sighireanu-98-a,

author =	{Hubert Garavel and Mihaela Sighireanu},
title =		{{Towards a Second Generation of Formal Description Techniques
		-- Rationale for the Design of E-LOTOS}},
booktitle =	{Proceedings of the 3rd International Workshop on Formal
		Methods for Industrial Critical Systems (FMICS'98), Amsterdam,
		The Netherlands},
year =		{1998},

editor =	{Jan-Friso Groote and Bas Luttik and {Jos van} Wamel},
pages =		{187--230},
publisher =	{CWI},
address =	{Amsterdam},
month =		may,

note = 		{Invited lecture},

annote =	{LOTOS NT, E-LOTOS}
}

@inproceedings{Garavel-Sighireanu-99,

author =        {Hubert Garavel and Mihaela Sighireanu},
title =         {{A Graphical Parallel Composition Operator for Process 
		Algebras}},
booktitle =	{Proceedings of the IFIP Joint International Conference on
		Formal Description Techniques for Distributed Systems and 
		Communication Protocols, and Protocol Specification, Testing,
		and Verification (FORTE/PSTV'99), Beijing, China},
year =		{1999},

editor =	{Jianping Wu and Qiang Gao and Samuel T. Chanson},
pages =		{185--202},
publisher =	{Kluwer Academic Publishers},
month =		oct,

annote =        {E-LOTOS}
}

@inproceedings{Garavel-Thivolle-09,

author =	{Hubert Garavel and Damien Thivolle},
title =		{{Verification of GALS Systems by Combining Synchronous
		Languages and Process Calculi}},
booktitle =     {Proceedings of the 16th International SPIN Workshop on Model
		 Checking of Software (SPIN'09), Grenoble, France},
year =		{2009},

editor =	{Corina Pasareanu},
publisher =     sv,
series =        lncs,
volume =        {5578},
pages =		{241--260},
month =		jun,

annote = 	{SAM 2 CADP}
}

@inproceedings{Garavel-Turlier-93,

author =	{Hubert Garavel and Philippe Turlier},
title =		{{C{\AE}SAR.ADT~: un compilateur pour les types abstraits
		alg\'ebriques du langage LOTOS}},
booktitle =	{Actes du Colloque Francophone pour l'Ing\'enierie des 
		Protocoles (CFIP'93), Montr\'eal, Canada},
year =		{1993},

editor =	{Rachida Dssouli and Gregor v. Bochmann},
pages =		{325--339},
publisher =	{Herm\`es},
address =	{Paris},
month =		sep,

annote =	{CAESAR.ADT}
}

@techreport{Garavel-Viho-Zendri-00,

author =	{Hubert Garavel and C\'esar Viho and Massimo Zendri},
title =		{System Design of a CC-NUMA Multiprocessor Architecture using
		Formal Specification, Model-Checking, Co-Simulation, and
		Test Generation},
institution =	{INRIA},
year = 		{2000},

type =		{Research Report},
number =	{RR-4041},
address =	{},
month =		nov,

annote = 	{POLYKID}
}

@article{Garavel-Viho-Zendri-01,

author =	{Hubert Garavel and C\'esar Viho and Massimo Zendri},
title =		{{System Design of a CC-NUMA Multiprocessor Architecture using
		Formal Specification, Model-Checking, Co-Simulation, and
		Test Generation}},
journal = 	{Springer International Journal on Software Tools for
		Technology Transfer (STTT)},
year = 		{2001},

volume =	{3},
number =	{3},
pages =		{314--331},
month =		jul,
note =		{Also available as INRIA Research Report~RR-4041},

annote = 	{POLYKID}
}

@unpublished{Helmstetter-09,

author =        {Claude Helmstetter},
title =         {TLM.OPEN: a SystemC/TLM Front-End for the CADP Verification
		Toolbox},
note =          {Workshop on Simulation Based Development of Certified
		Embedded Systems {SBDCES}'09 (Awaji Island, Hyogo, Japan)},

month =         oct,
year =          {2009},


annote =	{TLM.OPEN}
}

@inproceedings{Hermanns-Joubert-03,

author =        {Holger Hermanns and Christophe Joubert},
title =         {A Set of Performance and Dependability Analysis Components
		for CADP},
booktitle =     {Proceedings of the 9th International Conference on Tools and 
                Algorithms for the Construction and Analysis of Systems 
                (TACAS'03), Warsaw, Poland},
year =          {2003},

editor =        {Hubert Garavel and John Hatcliff},
publisher =     sv,
series =        lncs,
volume =        {2619},
pages =		{425--430},
month =         apr,

annote =	{Outils PDAC}
}

@techreport{ISO-8807,

author =	{ISO/IEC},
title =		{{LOTOS -- A Formal Description Technique Based on the Temporal
		Ordering of Observational Behaviour}},
institution =	{International Organization for Standardization -- Information
		Processing Systems -- Open Systems Interconnection},
year =		{1989},

type =		{International Standard},
number =	{8807},
address =	{Geneva},
month =		sep,

annote =	{definition formelle de LOTOS [IS]}
}

@article{Jard-Jeron-05,

author =	{Claude Jard and Thierry J\'eron},
title =		{TGV: Theory, Principles and Algorithms -- A Tool for the
		Automatic Synthesis of Conformance Test Cases for
		Non-Deterministic Reactive Systems},
journal = 	{Springer International Journal on Software Tools for
		Technology Transfer (STTT)},
year = 		{2005},

volume =	{7},
number =	{4},
pages =		{297--315},
month =		aug,

annote = 	{description detaillee de TGV}
}

@inproceedings{Joubert-Mateescu-04,

author = 	{Christophe Joubert and Radu Mateescu},
title = 	{Distributed On-the-Fly Equivalence Checking},
booktitle =	{Proceedings of the 3rd International Workshop on Parallel
		and Distributed Methods in Verification (PDMC'04), London, UK},
year = 		{2004},

editor = 	{Lubos Brim and Martin Leucker},
series = 	entcs,
volume = 	{128},
issue = 	{3},
publisher = 	{Elsevier}
}

@inproceedings{Joubert-Mateescu-05,

author =	{Christophe Joubert and Radu Mateescu},
title =		{Distributed Local Resolution of Boolean Equation Systems},
booktitle =	{Proceedings of the 13th Euromicro Conference on Parallel,
		Distributed and Network-Based Processing (PDP'05), Lugano,
		Switzerland},
year =		{2005},

editor =	{Francisco Tirado and Manuel Prieto},
publisher =	{IEEE Computer Society},
pages =		{264--271},
month =		feb,

annote = 	{algo de resolution distribue pour les SEB mono-bloc}
}

@inproceedings{Joubert-Mateescu-06,

author =	{Christophe Joubert and Radu Mateescu},
title =		{Distributed On-the-Fly Model Checking and Test Case
		Generation},
booktitle =     {Proceedings of the 13th International SPIN Workshop on Model
		Checking of Software (SPIN'06), Vienna, Austria},
year =		{2006},

editor =	{Antti Valmari},
publisher =     sv,
series =        lncs,
volume =        {3925},
pages =		{126--145},
month =		mar # "--" # apr,

annote = 	{Algorithme MB-DSOLVE et application pour EVALUATOR 3.5 et
		EXTRACTOR}
}

@inproceedings{Kahlouche-Viho-Zendri-98,

author =	{Hakim Kahlouche and C\'esar Viho and Massimo Zendri},
title =		{{An Industrial Experiment in Automatic Generation of
		 Executable Test Suites for a Cache Coherency Protocol}},
booktitle =	{Proceedings of the IFIP 11th International Workshop on Testing
		of Communicating Systems (IWTCS'98), Tomsk, Russia},
year =		{1998},

editor =	{Alexandre Petrenko and Nina Yevtushenko},
publisher =	ch,
month =		sep,

annote = 	{TGV LOTOS}
}

@inproceedings{Kahlouche-Viho-Zendri-98,

author =	{Hakim Kahlouche and C\'esar Viho and Massimo Zendri},
title =		{{An Industrial Experiment in Automatic Generation of
		 Executable Test Suites for a Cache Coherency Protocol}},
booktitle =	{Proceedings of the IFIP 11th International Workshop on Testing
		of Communicating Systems (IWTCS'98), Tomsk, Russia},
year =		{1998},

editor =	{Alexandre Petrenko and Nina Yevtushenko},
publisher =	ch,
month =		sep,

annote = 	{TGV LOTOS}
}

@inproceedings{Kerbrat-94,

author =	{Alain Kerbrat},
title =		{Reachable State Space Analysis of LOTOS Programs},
booktitle =	{Proceedings of the 7th International Conference on Formal
		Description Techniques for Distributed Systems and 
		Communication Protocols {FORTE}'94 (Bern, Switzerland)},
year =		{1994},

editor =	{Dieter Hogrefe and Stefan Leue},
month =		oct,

annote =	{identique a Kerbrat-94-a ; conserve pour compatibilite
                 ascendante car l'article Kerbrat-94 est dans la distribution
                 et le site Web de CADP}
}

@inproceedings{Kerbrat-BenAtallah-95,

author =	{Alain Kerbrat and Slim {Ben Atallah}},
title =		{{Formal Specification of a Framework for Groupware 
		Development}},
booktitle =	{Proceedings of the 8th International Conference on Formal
		Description Techniques for Distributed Systems and 
		Communication Protocols (FORTE'95), Montreal, Quebec, Canada},
year =		{1995},

editor =	{Gregor v. Bochmann and Rachida Dssouli and Omar Rafiq},
pages =		{303--310},
publisher =	sv,
series =        {IFIP Advances in Information and Communication Technology},
month =		oct,

annote =	{}
}

@inproceedings{Krimm-Mounier-97,

author =        {Jean-Pierre Krimm and Laurent Mounier},
title =         {{Compositional State Space Generation from LOTOS Programs}},
booktitle =     {Proceedings of the 3rd International Workshop on Tools and
		Algorithms for the Construction and Analysis of Systems
		(TACAS'97), University of Twente, Enschede, The Netherlands},
year =          {1997},

editor =        {Ed Brinksma},
publisher =     sv,
series =	lncs,
volume =	{1217},
month =         apr,

note =          {Extended version with proofs available as Research 
		Report VERIMAG~RR97-01}
}

@inproceedings{Kriouile-Serwe-13,

author =	{Abderahman Kriouile and Wendelin Serwe},
title =		{{Formal Analysis of the ACE Specification for Cache Coherent
		Systems-on-Chip}},
booktitle =	{Proceedings of the 18th International Workshop on Formal
		Methods for Industrial Critical Systems (FMICS'13), Madrid,
		Spain},
year =		{2013},

editor =	{Charles Pecheur and Michael Dierkes},
publisher =	sv,
series =	lncs,
volume =	{8187},
pages =		{108--122},
month =		sep,


annote = 	{etude de cas avec CADP : ACE}
}

@inproceedings{Lang-02,

author =        {Fr\'ed\'eric Lang},
title =         {{Compositional Verification using SVL Scripts}},
booktitle =     {Proceedings of the 8th International Conference on Tools and 
                Algorithms for the Construction and Analysis of Systems 
                (TACAS'02), Grenoble, France},
year =          {2002},

editor =        {Joost-Pieter Katoen and Perdita Stevens},
publisher =     sv,
series =        lncs,
volume =        {2280},
pages =         {465--469},
month =         apr,

annote =        {Utilisation de SVL pour la verification compositionnelle}
}

@inproceedings{Lang-05,

author =	{Fr\'ed\'eric Lang},
title =		{{EXP.OPEN 2.0: A Flexible Tool Integrating Partial Order, 
		Compositional, and On-the-fly Verification Methods}},
booktitle =	{Proceedings of the 5th International Conference on Integrated 
		Formal Methods (IFM'05), Eindhoven, The Netherlands},
year =		{2005},

editor =	{Judi Romijn and Graeme Smith and Jaco {van de Pol}},
publisher =	sv,
series =	lncs,
volume =	{3771},
pages =		{70--88},
month =		nov,
note =		{Full version available as INRIA Research Report~RR-5673},

annote =	{Exp.Open 2.0}
}

@inproceedings{Lang-06,

author =	{Fr\'ed\'eric Lang},
title =		{{Refined Interfaces for Compositional Verification}},
booktitle =	{Proceedings of the 26th IFIP WG 6.1 International Conference
		on Formal Techniques for Networked and Distributed Systems
		(FORTE'06), Paris, France},
year =		{2006},

editor =	{Elie Najm and Jean-Fran\c{c}ois Pradat-Peyre and V\'eronique 
		{Vigui\'e Donzeau-Gouge}},
publisher =	sv,
series =	lncs,
volume =	{4229},
pages =		{159--174},
month =		sep,
note =		{Full version available as INRIA Research Report~RR-5996},

annote =	{Interfaces raffinees dans Exp.Open 2.0 et SVL}
}

@article{Lang-Salaun-Herilier-et-al-10,

author =	{Fr\'ed\'eric Lang and Gwen Sala\"un and R\'emi H\'erilier
		and Jeff Kramer and Jeff Magee},
title =		{{Translating FSP into LOTOS and Networks of Automata}},
journal =	{Formal Aspects of Computing},
year =		{2010},

publisher =	sv,
volume =	{22},
number =	{6},
pages =		{681--711},
month =		nov,

annote =	{Traducteur FSP2LOTOS - version journal etendue et revisee de 
		Salaun-Kramer-Lang-Magee-07}
}

@inproceedings{Lang-Mateescu-09,

author = 	{Fr\'ed\'eric Lang and Radu Mateescu},
title = 	{Partial Order Reductions using Compositional Confluence
		Detection},
booktitle = 	{Proceedings of the 16th International Symposium on Formal 
		Methods (FM'09), Eindhoven, The Netherlands},
year = 		{2009},
month = 	nov,
editor = 	{Jos Baeten and Ana Cavalcanti and Dennis Dams},
publisher = 	sv,
series = 	lncs,
volume = 	{5850},
pages = 	{157--172},

annote =	{}
}

@inproceedings{Lang-Mateescu-12,

author = 	{Fr\'ed\'eric Lang and Radu Mateescu},
title = 	{Partial Model Checking using Networks of Labelled Transition
		Systems and Boolean Equation Systems},
booktitle = 	{Proceedings of the 18th International Conference on Tools and
		Algorithms for the Construction and Analysis of Systems
		(TACAS'12), Talinn, Estonia},
year = 		{2012},
month = 	mar,
editor = 	{Cormac Flanagan and Barbara K\"onig},
publisher = 	sv,
series = 	lncs,
volume = 	{7214},
pages = 	{141--156},

annote =	{partial model-checking}
}

@article{Lang-Mateescu-13,

author =	{Fr\'ed\'eric Lang and Radu Mateescu},
title =		{{Partial Model Checking using Networks of Labelled Transition
		Systems and Boolean Equation Systems}},
journal =	{Logical Methods in Computer Science},
year =          {2013},

volume =	{9},
number =	{4},
pages =		{1--32},
month =         oct,
annote =        {partial model-checking, extended version of Lang-Mateescu-12}
}

@inproceedings{Lantreibecq-Serwe-11,

author =	{Etienne Lantreibecq and Wendelin Serwe},
title =		{{Model Checking and Co-simulation of a Dynamic Task Dispatcher
		Circuit Using CADP}},
booktitle =	{Proceedings of the 16th International Workshop on Formal
		Methods for Industrial Critical Systems (FMICS'11), Trento,
		Italy},
year =		{2011},

editor =	{Gwen Sala\"un and Bernhard Sch\"atz},
pages =		{180--195},
publisher =	sv,
series =	lncs,
volume =	{6959},
month =		aug,

annote = 	{etude de cas DTD}
}

@article{Lantreibecq-Serwe-14,

author =	{Etienne Lantreibecq and Wendelin Serwe},
title =		{{Formal Analysis of a Hardware Dynamic Task Dispatcher with
		CADP}},
journal = 	{Science of Computer Programming},
year = 		{2014},

volume =	{80},
number =	{Part A},
pages =		{130--149},
month =		feb,

annote = 	{etude de cas DTD}
}

@inproceedings{Leduc-87-b,

author =	{G. J. Leduc},
title =		{LOTOS, un outil utile ou un autre langage acad\'emique~?},
booktitle =	{Actes des Neuvi\`emes Journ\'ees Francophones sur
		l'Informatique -- Les r\'eseaux de communication -- Nouveaux
		outils et tendances actuelles (Li\`ege)},
year =		{1987},

month =		jan
}

@article{Logrippo-Faci-HajHussein-92,

author =	{L. Logrippo and M. Faci and M. Haj-Hussein},
title =		{An introduction to LOTOS: Learning by Examples},
journal =	isdn,
year =		{1992},

volume =	{23},
pages =		{325--342},
note =		{improved version available by ftp on lotos.csi.uottawa.ca},

annote =	{une introduction a LOTOS}
}

@inproceedings{Mateescu-96,

author =        {R. Mateescu},
title =		{Formal Description and Analysis of a Bounded Retransmission 
		Protocol},
booktitle =     {Proceedings of the COST 247 International Workshop on Applied 
		Formal Methods in System Design (Maribor, Slovenia)},
year =          {1996},

editor =	{Z. Brezo\v{c}nik and T. Kapus},
pages =         {98--113},
publisher =     {University of Maribor, Slovenia},
month =         jun,
note =		{Also available as INRIA Research Report~RR-2965},

annote =        {verification du BRP avec CADP + XTL}
}

@phdthesis{Mateescu-98-a,

author =	{Radu Mateescu},
school =	{Institut National Polytechnique de Grenoble},
title =		{V\'erification des propri\'et\'es temporelles des programmes 
		 parall\`eles},
type =		{{Th\`ese de Doctorat}}, 
year =		{1998},
month =		apr,

annote =        {XTL}
}

@inproceedings{Mateescu-98-b,

author =	{Radu Mateescu},
title =		{{Local Model-Checking of an Alternation-Free Value-Based Modal 
		Mu-Calculus}},
booktitle =	{Proceedings of the 2nd International Workshop on Verification,
		Model Checking and Abstract Interpretation (VMCAI'98), Pisa, 
		Italy},
year =		{1998},

editor =	{Annalisa Bossi and Agostino Cortesi and Francesca Levi},
publisher =	{University Ca' Foscari of Venice},
month =         sep,

annote =        {algo a la volee pour un mu-calcul d'alternance 1 avec valeurs}
}

@inproceedings{Mateescu-00-a,
 
author =        {Radu Mateescu},
title =         {Efficient Diagnostic Generation for Boolean Equation Systems},
booktitle =     {Proceedings of 6th International Conference on Tools and
		Algorithms for the Construction and Analysis of Systems
		(TACAS'00), Berlin, Germany},
year =          {2000},
 
editor =        {Susanne Graf and Michael Schwartzbach},
publisher =     sv,
series =        lncs,
volume =        {1785},
pages =         {251--265},
month =         mar,

note =		{Full version available as INRIA Research Report~RR-3861},
 
annote =        {generation d'exemples et contre-exemples dans EVALUATOR 3.0}
}

@inproceedings{Mateescu-02,
 
author =        {Radu Mateescu},
title =         {Local Model-Checking of Modal Mu-Calculus on Acyclic Labeled
		Transition Systems},
booktitle =     {Proceedings of the 8th International Conference on Tools and
		Algorithms for the Construction and Analysis of Systems
		(TACAS'02), Grenoble, France},
year =          {2002},
 
editor =        {Joost-Pieter Katoen and Perdita Stevens},
publisher =     sv,
series =        lncs,
volume =        {2280},
pages =         {281--295},
month =         apr,

note =		{Full version available as INRIA Research Report~RR-4430},

annote =        {Algorithmes optimises pour la verification de STE acycliques}
}

@inproceedings{Mateescu-03-a,

author =        {Radu Mateescu},
title =         {{A Generic On-the-Fly Solver for Alternation-Free Boolean
		Equation Systems}},
booktitle =     {Proceedings of the 9th International Conference on Tools and 
                Algorithms for the Construction and Analysis of Systems 
                (TACAS'03), Warsaw, Poland},
year =          {2003},

editor =        {Hubert Garavel and John Hatcliff},
publisher =     sv,
series =        lncs,
volume =        {2619},
pages =		{81--96},
month =         apr,
note =		{Full version available as INRIA Research Report~RR-4711},

annote =	{Bibliotheque CAESAR_SOLVE}
}

@article{Mateescu-03-b,

author =        {Radu Mateescu},
title =         {Logiques temporelles bas\'ees sur actions pour la
		v\'erification des syst\`emes asynchrones},
journal =       {Technique et Science Informatiques},
year =          {2003},

publisher =	{Lavoisier},
volume =        {22},
number =        {4},
pages =         {461--495},

note =		{Full version available as INRIA Research Report~RR-5032},

annote =        {synthese sur les logiques temporelles, les algorithmes de
		verification enumerative et les outils}
}

@inproceedings{Mateescu-03-c,

author =	{Radu Mateescu},
title =		{{On-the-Fly Verification using CADP}},
booktitle =	{Proceedings of the 8th International Workshop on Formal
		Methods for Industrial Critical Systems (FMICS'03),
		Trondheim, Norway},
year =		{2003},

editor =	{Thomas Arts and Wan Fokkink},
publisher =	{Elsevier},
volume =	{80},
series =        entcs,
month =		jun,

annote =	{CAESAR_SOLVE en bref}
}

@inproceedings{Mateescu-05,

author =	{Radu Mateescu},
title =		{{On-the-fly State Space Reductions for Weak Equivalences}},
booktitle =	{Proceedings of the 10th International Workshop on Formal
		Methods for Industrial Critical Systems (FMICS'05),
		Lisbon, Portugal},
year =		{2005},

editor =	{Tiziana Margaria and Mieke Massink},
organization =	{ERCIM},
publisher =	{ACM Computer Society Press},
pages =		{80--89},
month =		sep,

annote =	{reducteurs par tau-compression, tau-closure et tau-confluence}
}

@article{Mateescu-06-a,

author =	{Radu Mateescu},
title =		{{CAESAR\_SOLVE: A Generic Library for On-the-Fly Resolution
		of Alternation-Free Boolean Equation Systems}},
journal = 	{Springer International Journal on Software Tools for
		Technology Transfer (STTT)},
year = 		{2006},

editor =	{Hubert Garavel and John Hatcliff},
volume =	{8},
number =	{1},
pages =		{37--56},
month =		feb,
note =		{Full version available as INRIA Research Report RR-5948, July 2006},

annote = 	{description de CAESAR_SOLVE}
}

@inbook{Mateescu-06-b,

author =        {Radu Mateescu},
title =         {Mod\'elisation et analyse de syst\`emes asynchrones avec
		CADP},
booktitle =     {Syst\`emes temps re\'el 1 -- Techniques de description
		et de v\'erification},
year =          {2006},

series =	{Trait\'e IC2},
editor =        {Nicolas Navet},
chapter =       {5},
pages =         {151--180},
publisher =     {Lavoisier},
note =		{Full version available as INRIA Research Report RR~5953},

annote =        {tutoriel sur CADP base sur l'exemple de la table rotative}
}

@inbook{Mateescu-08,

author =        {Radu Mateescu},
title =         {Specification and Analysis of Asynchronous Systems using
		CADP},
booktitle =     {Modeling and Verification of Real-Time Systems -- Formalisms
		and Software Tools},
year =          {2008},

editor =        {Stephan Merz and Nicolas Navet},
chapter =       {5},
pages =         {141--170},
publisher =     {ISTE publishing / John Wiley},

annote =        {tutoriel sur CADP base sur l'exemple de la table rotative,
		version anglaise de Mateescu-06-b}
}

@inproceedings{Mateescu-Garavel-98,

author =	{Radu Mateescu and Hubert Garavel},
title =		{{XTL: A Meta-Language and Tool for Temporal Logic 
		Model-Checking}},
booktitle =	{Proceedings of the International Workshop on Software Tools 
		for Technology Transfer (STTT'98), Aalborg, Denmark},
year =		{1998},

editor =	{Tiziana Margaria},
pages =		{33--42},
organization =	{BRICS},
month =		jul,

annote = 	{}
}

@inproceedings{Mateescu-Monteiro-Dumas-deJong-08,

author =	{Radu Mateescu and {Pedro Tiago} Monteiro and Estelle Dumas and
		Hidde de Jong},
title = 	{{Computation Tree Regular Logic for Genetic Regulatory
		Networks}},
booktitle =	{Proceedings of the 6th International Symposium on Automated
		Technology for Verification and Analysis (ATVA'08), Seoul,
		South Korea},
year =		{2008},

editor =	{Sung Deok Cha and Jin-Young Choi and Moonzoo Kim and
		Insup Lee and Mahesh Viswanathan},
publisher =	sv,
series =	lncs,
volume =	{5311},
pages = 	{48--63},
month = 	oct,
note =		{Full version available as INRIA Research Report~RR-6521},

annote =	{definition de CTRL et traducteur Ctrl2Blk vers Evaluator}
}

@inproceedings{Mateescu-Oudot-08-a,

author =	{Radu Mateescu and Emilie Oudot},
title =		{{Bisimulator 2.0: An On-the-Fly Equivalence Checker based on
		Boolean Equation Systems}},
booktitle =	{Proceedings of the 6th ACM-IEEE International Conference on
		Formal Methods and Models for Codesign (MEMOCODE'08),
		Anaheim, CA, USA},
year =		{2008},

publisher =	{IEEE Computer Society Press},
pages =		{73--74},
month =		jun,

annote =	{papier court sur Bisimulator 2.0}
}

@inproceedings{Mateescu-Oudot-08-b,

author =	{Radu Mateescu and Emilie Oudot},
title =		{Improved On-the-Fly Equivalence Checking using Boolean
		Equation Systems},
booktitle =	{Proceedings of the 15th International SPIN Workshop on
		Model Checking of Software (SPIN'08), Los Angeles, USA},
year =		{2008},

editor =	{Klaus Havelund and Rupak Majumdar and Jens Palberg},
pages =		{196--213},
publisher =	sv,
series =	lncs,
volume =	{5156},
month =		aug,
note =		{Full version available as INRIA Research Report~RR-6777},

annote = 	{Nouveau codage des equivalences faibles et algorithme A8}
}

@inproceedings{Mateescu-Poizat-Salaun-07,

author =	{Radu Mateescu and Pascal Poizat and Gwen Sala\"un},
title =		{{Behavioral Adaptation of Component Compositions based
		on Process Algebra Encodings}},
booktitle =	{Proceedings of the 22nd IEEE/ACM International Conference
		on Automated Software Engineering (ASE'07), Atlanta,
		Georgia, USA},
year =		{2007},

editor =	{Alexander Egyed and Bernd Fischer},
publisher =	{ACM Press},
pages =		{385--388},
month =		nov,
note =		{Full version available as INRIA Research Report~RR-6362},

annote =	{Outils COMPOSITOR et SCRUTATOR pour la generation a la volee
		d'adaptateurs}
}

@inproceedings{Mateescu-Poizat-Salaun-08,

author =	{Radu Mateescu and Pascal Poizat and Gwen Sala\"{u}n},
title =		{Adaptation of Service Protocols using Process Algebra and
		On-the-Fly Reduction Techniques},
booktitle =	{Proceedings of the 6th International Conference on Service
		Oriented Computing {ICSOC}'08 (Sydney, Australia)},
year =		{2008},

editor =	{Athman Bouguettaya and Ingolf Krueger and Tiziana Margaria},

pages =		{84--99},
publisher =	sv,
series =	lncs,
volume =	{5364},
month =		dec,

annote = 	{Adaptation des protocoles avec communication de valeurs en
		utilisant LOTOS, Exp.Open, SVL, Compositor et Scrutator}
}

@inproceedings{Mateescu-Rampacek-08-a,

author =	{Radu Mateescu and Sylvain Rampacek},
title =		{Formal Modeling and Discrete-Time Analysis of BPEL Web
		Services},
booktitle =	{Proceedings of the 4th International Workshop on Enterprise
		and Organizational Modeling and Simulation {EOMAS}'08
		(Montpellier, France)},
year =		{2008},

editor =	{Joseph Barjis and Murali Mohan Narasipuram and Peter Rittgen},

pages =		{179--193},
publisher =	sv,
series =	{Lecture Notes in Business Information Processing},
volume =	{10},
month =		jun,

annote = 	{Etude de cas avec WSMOD et EVALUATOR 4}
}

@article{Mateescu-Rampacek-08-b,

author =	{Radu Mateescu and Sylvain Rampacek},
title =		{Formal Modelling and Discrete-Time Analysis of BPEL Web
		Services},
journal = 	{International Journal of Simulation and Process Modelling},
year = 		{2008},

volume =	{4},
number =	{3--4},
pages =		{183--194},

annote = 	{Etude de cas avec WSMOD et EVALUATOR 4}
}

@article{Mateescu-Requeno-18,
  author    = {Radu Mateescu and Jose Ignacio Requeno},
  title =     {{On-the-Fly Model Checking for Extended Action-Based
	       Probabilistic Operators}},
  journal =   {Springer International Journal on Software Tools for
               Technology Transfer (STTT)},
  volume    = {20},
  number    = {5},
  pages     = {563--587},
  year      = {2018},

annote = {Evaluator 5}
}

@inproceedings{Mateescu-Salaun-10,

author =	{Radu Mateescu and Gwen Sala\"un},
title =		{{Translating Pi-Calculus into LOTOS NT}},
booktitle =	{Proceedings of the 8th International Conference on Integrated
		Formal Methods (IFM'10), Nancy, France},
year =		{2010},

month =		oct,
series =	lncs,
editor =	{Dominique Mery and Stephan Merz},
publisher =	sv,
volume =	{6396},
pages =		{229--244},

annote =	{PIC2LNT}
}

@inproceedings{Mateescu-Serwe-10,

author =	{Radu Mateescu and Wendelin Serwe},
title =		{{A Study of Shared-Memory Mutual Exclusion Protocols using
		CADP}},
booktitle =	{Proceedings of the 15th International Workshop on Formal
		Methods for Industrial Critical Systems (FMICS'10),
		Antwerp, Belgium},
year =		{2010},

editor =	{Stefan Kowalewski and Marco Roveri},
publisher =	sv,
series =	lncs,
volume =	{6371},
pages =		{180--197},
month =		sep,
annote =	{papier de reference de la demo 41}
}

@article{Mateescu-Serwe-13,

author =	{Radu Mateescu and Wendelin Serwe},
title =		{{Model Checking and Performance Evaluation with CADP
		Illustrated on Shared-Memory Mutual Exclusion Protocols}},
journal = 	{Science of Computer Programming},
year = 		{2013},

volume =	{78},
number =	{7},
pages =		{843--861},
month =		jul,


annote = 	{}
}

@inproceedings{Mateescu-Sighireanu-00,

author =	{Radu Mateescu and Mihaela Sighireanu},
title =		{Efficient On-the-Fly Model-Checking for Regular
		Alternation-Free Mu-Calculus},
booktitle =	{Proceedings of the 5th International Workshop on Formal
		Methods for Industrial Critical Systems (FMICS'00), Berlin,
		Germany},
year =		{2000},

editor =	{Stefania Gnesi and Ina Schieferdecker and Axel Rennoch},
series =	{GMD Report 91},
address =	{Berlin},
pages =		{65--86},
month =		apr,

note = 		{Also available as INRIA Research Report~RR-3899},

annote =	{description d'EVALUATOR 3.0}
}

@article{Mateescu-Sighireanu-03,

author =	{Radu Mateescu and Mihaela Sighireanu},
title =		{{Efficient On-the-Fly Model-Checking for Regular
		Alternation-Free Mu-Calculus}},
journal = 	scp,
year = 		{2003},

volume =	{46},
number =	{3},
pages =		{255--281},
month =		mar,

annote = 	{description d'EVALUATOR 3.0}
}

@inproceedings{Mateescu-Thivolle-08,

author =	{Radu Mateescu and Damien Thivolle},
title =		{{A Model Checking Language for Concurrent Value-Passing
                 Systems}},
booktitle =	{Proceedings of the 15th International Symposium on Formal
		Methods (FM'08), Turku, Finland},
year =		{2008},

editor =	{Jorge Cuellar and Tom Maibaum and Kaisa Sere},
pages =		{148--164},
publisher =	sv,
series =	lncs,
volume =	{5014},
month =		may,

annote = 	{Description de MCL et EVALUATOR 4.0}
}

@inproceedings{Mateescu-Wijs-09-a,

author =	{Radu Mateescu and Anton Wijs},
title =		{{Hierarchical Adaptive State Space Caching based on Level
		Sampling}},
booktitle =	{Proceedings of the 15th International Conference on Tools
		and Algorithms for the Construction and Analysis of Systems
		(TACAS'09), York, UK},
year =		{2009},

editor =	{Stefan Kowalewski and Anna Philippou},
publisher =	sv,
series =	lncs,
volume =	{5505},
pages =		{215--229},
month =		mar,

annote = 	{Generation de LTS par BFS et DFS avec caches hierarchiques}
}

@techreport{Mateescu-Wijs-09-b,

author =	{Radu Mateescu and Anton Wijs},
title =		{Efficient On-the-Fly Computation of Weak Tau-Confluence},
institution =	{INRIA},
year = 		{2009},

type =		{Research Report},
number =	{RR-7000},
month =		jul,

annote = 	{tau-confluence faible detectee a la volee}
}

@inproceedings{Mateescu-Wijs-11,

author =	{Radu Mateescu and Anton Wijs},
title =		{Property-Dependent Reductions for the Modal Mu-Calculus},
booktitle =	{Proceedings of the 18th International SPIN Workshop on
		Model Checking Software (SPIN'11), Snowbird, Utah, USA},

year =		{2011},

editor =	{Alex Groce and Madanlal Musuvathi},
publisher =     sv,
series =        lncs,
volume =        {6823},
pages =         {2--19},
month =         jul,

note =          {Full version available as INRIA Research Report~RR-7690},


annote = 	{fragment du mu-calcul compatible avec la bisimulation de
		branchement sensible a la divergence}
}

@phdthesis{Mounier-92,

author =	{Laurent Mounier},
school =	{Universit\'e Joseph~Fourier (Grenoble)},
title =		{M\'ethodes de v\'erification de sp\'ecifications
		comportementales~: \'etude et mise en {\oe}uvre},
type =		{{Th\`ese de Doctorat}}, 
year =		{1992},
month =		jan,

annote =	{nouvel ALDEBARAN}
}

@techreport{Mounier-94,

author =	{Laurent Mounier},
title =		{{A LOTOS Specification of a Transit-Node}},
institution =	{VERIMAG},
year =		{1994},

type =		{Rapport SPECTRE},
number =	{94-8},
address =	{Grenoble},
month =		mar,
}

@techreport{Mounier-Bainbridge-91,

author =	{Simon Bainbridge and Laurent Mounier},
title = 	{{Specification and Verification of a Reliable Multicast 
		Protocol}},
institution =	{Hewlett-Packard Laboratories},
year =		{1991},

type =		{Technical Report},
number =	{HPL-91-163},
address =	{Bristol, U.K.},
month =		oct
}

@inproceedings{Pace-Lang-Mateescu-03,

author =    {Gordon Pace and Fr\'ed\'eric Lang and Radu Mateescu},
title =     {Calculating $\tau$-Confluence Compositionally},
booktitle = {Proceedings of the 15th International Conference on
            Computer Aided Verification (CAV'03), Boulder, Colorado, USA},
year =      {2003},

editor =    {Warren A. Hunt, Jr and Fabio Somenzi},
publisher = sv,
series =    lncs,
volume =    {2725},
pages =     {446--459},
month =     jul,
note =      {Full version available as INRIA Research Report~RR-4918},

anote =     {Presentation des outils tau_confluence et option -branching
            de exp.open}
}

@inproceedings{Pecheur-97,

author =	{Charles Pecheur},
title =		{Specification and Verification of the CO4 Distributed 
		Knowledge System Using LOTOS},
booktitle =	{Proceedings of the 12th IEEE International Conference on 
		Automated Software Engineering ASE-97 (Incline Village, 
		Nevada, USA)},
year =		{1997},

editor =	{Michael Lowry and Yves Ledru},
month =		nov,

note =          {Extended version available as INRIA Research Report~RR-3259}
}

@techreport{Pecheur-98,

author =	{Charles Pecheur},
title =		{Advanced Modelling and Verification Techniques Applied to
		a Cluster File System},
institution =	{INRIA},
year =		{1998},

type =		{Research Report},
number =	{RR-3416},
address =	{Grenoble},
month =		may,

annote =	{CFS}
}

@inproceedings{Pecheur-99,
 
author =        {Charles Pecheur},
title =         {{Advanced Modelling and Verification Techniques Applied to
		a Cluster File System}},
booktitle =     {Proceedings of the 14th IEEE International Conference on
		Automated Software Engineering (ASE'99) Cocoa Beach, Florida, 
		USA},
year =          {1999},
 
editor =        {Robert J. Hall and Ernst Tyugu},
publisher =   {IEEE Computer Society},
month =         oct,
 
note =          {Extended version available as INRIA Research Report~RR-3416},

annote =	{verification de CFS avec CADP et XTL}
}

@inproceedings{Ponsini-Serwe-08,

author =	{Olivier Ponsini and Wendelin Serwe},
title =		{A Schedulerless Semantics of {TLM} Models Written in {SystemC}
		via Translation into {LOTOS}},
booktitle =	{Proceedings of the 15th International Symposium on Formal
		Methods {FM}'08 (Turku, Finland)},
year =		{2008},

editor =	{Jorge Cuellar and Tom Maibaum and Kaisa Sere},
pages =		{278--293},
publisher =	sv,
series =	lncs,
volume =	{5014},
month =		may,

annote = 	{}
}

@inproceedings{Salaun-Serwe-05,

author =	{Gwen Sala\"un and Wendelin Serwe},
title =		{{Translating Hardware Process Algebras into Standard Process
		Algebras -- Illustration with CHP and LOTOS}},
booktitle =	{Proceedings of the 5th International Conference on Integrated
		Formal Methods (IFM'05), Eindhoven, The Netherlands},
year =		{2005},

editor =	{Judi Romijn and Graeme Smith and Jaco {van de Pol}},
publisher =	sv,
series =	lncs,
pages =		{287--306},
volume =	{3771},
month =		nov,
note =          {Full version available as INRIA Research Report~RR-5666},

annote =	{CHP, chp2lotos}
}

@inproceedings{Salaun-Serwe-Thonnart-Vivet-07,

author =	{Gwen Sala\"un and Wendelin Serwe and Yvain Thonnart and Pascal
		Vivet},
title =		{{Formal Verification of CHP Specifications with CADP --
		Illustration on an Asynchronous Network-on-Chip}},
booktitle =	{Proceedings of the 13th IEEE International Symposium on
		Asynchronous Circuits and Systems (ASYNC'07), Berkeley,
		California, USA},
year =		{2007},

editor =	{Peter Beerel and Marly Roncken and Mark Greenstreet and
		Montek Singh},
pages =		{73--82},
publisher =	{IEEE Computer Society Press},
month =		mar,

annote = 	{}
}

@article{SchnoEbelen-88-b,

author =	{Philippe Schn{o}{e}belen},
title =		{{Refined Compilation of Pattern-Matching for Functional
		Languages}},
journal =	{Science of Computer Programming},
year =		{1988},

volume =	{11},
pages =		{133--159}
}

@inproceedings{Sighireanu-Mateescu-97,

author =	{Mihaela Sighireanu and Radu Mateescu},
title =		{Validation of the Link Layer Protocol of the IEEE-1394 Serial
		 Bus (``FireWire''): an Experiment with E-LOTOS},
booktitle =	{Proceedings of the 2nd COST 247 International Workshop on
                Applied Formal Methods in System Design (Zagreb, Croatia)},
editor =	{Ignac Lovrek},
year =		{1997},
month =		jun,

note =          {Full version available as INRIA Research Report~RR-3172}
}

@techreport{Sighireanu-Turner-98,

author =	{Mihaela Sighireanu and {Kenneth J.} Turner},
title =		{{Requirement Capture, Formal Description and Verification of
		an Invoicing System}},
institution =	{INRIA},
year =		{1998},

type =		{Research Report},
number =	{RR-3575},
address =	{Grenoble},
month =		dec,

annote =		{etude de cas facturation}
}

@phdthesis{Sighireanu-99,

author =	{Mihaela Sighireanu},
school =	{Universit\'e Joseph Fourier (Grenoble)},
title =		{{Contribution \`a la d\'efinition et \`a l'impl\'ementation du 
		langage ``Extended LOTOS''}},
type =		{{Th\`ese de Doctorat}}, 
year =		{1999},
month =		jan,

annote =	{E-LOTOS et LOTOS NT}
}

@inbook{Tocher-89,

author =	{A. J. Tocher},
title =		{LOTOS and the Formal Specification of Communication 
		Standards},
editor =	{P. N. Scharbach},
booktitle =	{Formal Methods: Theory and Practice},
publisher =	{BSP Professional Books},
year =		{1989},

address =	{Oxford},

annote =	{introduction a LOTOS (exemple du transport)}
}

@inproceedings{Tronel-Lang-Garavel-03,

author =    {Fr\'ed\'eric Tronel and Fr\'ed\'eric Lang and Hubert Garavel},
title =     {{Compositional Verification Using CADP of the ScalAgent Deployment
            Protocol for Software Components}},
booktitle = {Proceedings of the 6th IFIP International Conference on Formal
            Methods for Open Object-based Distributed Systems (FMOODS'03),
            Paris, France},
year =      {2003},

editor =    {Elie Najm and Uwe Nestmann and Perdita Stevens},
publisher = sv,
series =    lncs,
volume =    {2884},
pages =     {244--260},
month =     nov,
note =      {Full version available as INRIA Research Report~RR-5012},

annote =     {Etude de cas Parfums}
}

@techreport{Tock-95,

author =	{Louis-Pascal Tock},
title =		{The BCG PostScript Format},
institution =	{INRIA Rh\^one-Alpes},
year =		{1995},

type =		{Rapport SPECTRE},
number =	{95-12},
address =	{Grenoble},
month =		oct,
annote =	{version 1.0}
}

@techreport{Turner-89,

author =	{Kenneth J. Turner},
title =		{The Formal Specification Language LOTOS: A Course for Users},
institution =	{Department of Computer Science and Mathematics, University of
		Stirling, Scotland},
year = 		{1989},

month =		aug,

annote = 	{see http://www.cs.stir.ac.uk/~kjt/research/publications.html}
}

@book{Turner-93,

editor =	{Kenneth J. Turner},
title =		{Using Formal Description Techniques -- An Introduction to 
		ESTELLE, LOTOS, and SDL},
publisher =	{Wiley},
year =		{1993},


annote =	{xxiv + 431 pages, 80 figures/tables, 29 specifications
		ISBN 0-471-93455-0}
}

@inproceedings{Zhang-Serwe-Wu-et-al-14,

author =	{Zhen Zhang and Wendelin Serwe and Jian Wu and Tomohiro Yoneda
		Hao Zheng and Chris Myers},
title =		{{Formal Analysis of a Fault-Tolerant Routing Algorithm for a
		Network-on-Chip}},
booktitle =	{Proceedings of the 19th International Workshop on Formal
		Methods for Industrial Critical Systems (FMICS'14), Florence,
		Italy},
year =		{2014},

editor =	{Fr\'{e}d\'{e}ric Lang and Francesco Flammini},
publisher =	sv,
series =	lncs,
volume =	{8718},
pages =		{48--62},
month =		sep,


annote = 	{etude de cas avec CADP : Utah/NoC}
}