@inproceedings{Alechina::Demri::deRijke01,
  address = {Rome, Italy},
  month = sep,
  year = 2001,
  volume = 45,
  series = {CEUR Workshop Proceedings},
  publisher = {RWTH Aachen, Germany},
  editor = {Lenzerini, Maurizio and Nardi, Daniele and Nutt, Werner
            and Suciu, Dan},
  acronym = {{KRDB}'01},
  booktitle = {{P}roceedings of the 8th {I}nternational 
               {W}orkshop on {K}nowledge {R}epresentation meets
               {D}atabases
               ({KRDB}'01)},
  author = {Alechina, Natasha and Demri, St{\'e}phane and 
                  de Rijke, Maarten},
  title = {Path Constraints from a Modal Logic Point of View
                 (Extended Abstract)},
  missingpages = {},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ADdR-krdb01.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/ADdR-krdb01.ps}
}
@inproceedings{BB-wadt2001,
  address = {Genova, Italy},
  month = apr,
  year = 2001,
  volume = 2267,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Cerioli, Maura and Reggio, Gianna},
  acronym = {{WADT}'01},
  booktitle = {{R}ecent {T}rends in {A}lgebraic {D}evelopment {T}echniques~---
               {S}elected {P}apers of the 15th {I}nternational {W}orkshop
               on {A}lgebraic {D}evelopment {T}echniques
               ({WADT}'01)},
  author = {Bidoit, Michel and Boisseau, Alexandre},
  title = {Algebraic Abstractions},
  pages = {21-47},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BB-wadt2001.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BB-wadt2001.ps}
}
@article{BBFM-DISTCOMP,
  publisher = {Springer},
  journal = {Distributed Computing},
  author = {Beauquier, Joffroy and B{\'e}rard, B{\'e}atrice and 
                 Fribourg, Laurent and Magniette, Fr{\'e}d{\'e}ric},
  title = {Proving Convergence of Self-Stabilizing Systems Using
                 First-Order Rewriting and Regular Languages},
  volume = {14},
  number = {2},
  pages = {83-95},
  year = {2001},
  missingmonth = {},
  missingnmonth = {},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBFM-DISCOMP2000.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BBFM-DISCOMP2000.ps},
  doi = {10.1007/PL00008931}
}
@proceedings{BCF-lncs2102,
  title = {{P}roceedings of the 13th
           {I}nternational {C}onference on 
           {C}omputer {A}ided {V}erification
           ({CAV}'01)},
  booktitle = {{P}roceedings of the 13th
               {I}nternational {C}onference on 
               {C}omputer {A}ided {V}erification
               ({CAV}'01)},
  editor = {Berry, G{\'e}rard and Comon, Hubert and Finkel, Alain},
  publisher = {Springer},
  volume = {2102},
  series = {Lecture Notes in Computer Science},
  year = {2001},
  month = jul,
  address = {Paris, France},
  isbn = {3-540-42345-1},
  url = {http://www.springer.com/978-3-540-42345-1},
  olderurl = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-42345-1}
}
@inproceedings{BPT-concur-2001,
  address = {Aalborg, Denmark},
  month = aug,
  year = 2001,
  volume = 2154,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Larsen, Kim G. and Nielsen, Modens},
  acronym = {{CONCUR}'01},
  booktitle = {{P}roceedings of the 12th 
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'01)},
  author = {Bouyer, Patricia and Petit, Antoine and 
                  Th{\'e}rien, Denis},
  title = {An Algebraic Characterization of Data and Timed
                 Languages},
  pages = {248-261},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BPT-concur2001.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BPT-concur2001.ps},
  abstract = {Algebra offers an elegant and 
	powerful approach to understand regular
	languages and finite automata. Such framework 
	has been notoriously
	lacking for timed languages and timed automata. 
	We introduce the
	notion of monoid recognizability for data 
	languages, which include
	timed languages as special case, in a way that 
	respects the spirit of
	the classical situation. We study closure 
	properties and hierarchies
	in this model, and prove that emptiness is 
	decidable under natural
	hypotheses. Our class of recognizable languages 
	properly includes many
	families of deterministic timed languages that 
	have been proposed
	until now, and the same holds for 
	non-deterministic versions.}
}
@inproceedings{BT-afadl2001,
  address = {Nancy, France},
  month = jun,
  year = 2001,
  editor = {Souqui{\`e}res, Jeanine},
  acronym = {{AFADL}'01},
  booktitle = {{A}ctes du 4{\`e}me {A}telier sur les {A}pproches {F}ormelles
               dans l'{A}ssistance au {D}{\'e}veloppement de {L}ogiciels
               ({AFADL}'01)},
  author = {Blanc, Benjamin and Tort, Fran{\c{c}}oise},
  title = {Co-d\'eveloppement de sp\'ecifications alg\'ebriques},
  pages = {141-156},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BT-afadl01.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BT-afadl01.ps}
}
@misc{CASL-tut-2001,
  author = {Bidoit, Michel and Mosses, Peter D.},
  title = {A Gentle Introduction to {CASL}~v1.0.1},
  year = {2001},
  month = apr,
  howpublished = {Invited tutorial, CoFI Workshop at the 4th European Joint Conferences on
                 Theory and Practice of Software (ETAPS 2001), Genova,
                 Italy},
  url = {http://www.lsv.ens-cachan.fr/~bidoit/CASL/}
}
@techreport{CCR-vulcain-final,
  author = {Canet, G{\'e}raud and Couffin, S. and Rossi, O.},
  title = {Validation dans le cadre de l'utilisation des {SFC},
                 {LD} et~{ST}},
  year = {2001},
  month = may,
  type = {Final Report},
  institution = {t{\^a}ches~4, 5 et~6, projet VULCAIN},
  missinghowpublished = {Rapport final des t{\^a}ches~4, 5 et~6
                 du projet {VULCAIN}},
  note = {393 pages}
}
@proceedings{CMR-lncs2002,
  title = {{R}evised {L}ectures of the
           {I}nternational {S}ummer {S}chool on {C}onstraints
           in {C}omputational {L}ogics
           ({CCL}'99)},
  booktitle = {{R}evised {L}ectures of the
               {I}nternational {S}ummer {S}chool on {C}onstraints
               in {C}omputational {L}ogics
               ({CCL}'99)},
  editor = {Comon, Hubert and March{\'e}, Claude and Treinen, Ralf},
  publisher = {Springer},
  volume = {2002},
  series = {Lecture Notes in Computer Science},
  year = {2001},
  address = {Gif-sur-Yvette, France},
  isbn = {3-540-41950-0},
  url = {http://www.springer.com/978-3-540-41950-0},
  olderurl = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-41950-0}
}
@techreport{Calife-4.4,
  author = {B{\'e}rard, B{\'e}atrice and Bouyer, Patricia and 
                  Petit, Antoine},
  title = {Mod{\'e}lisation du protocole~{PGM} et de certaines de ses
                 propri{\'e}t{\'e}s en {UPPAAL}},
  year = {2001},
  month = nov,
  type = {Contract Report},
  number = {4.4},
  institution = {projet RNRT Calife},
  note = {18 pages}
}
@inproceedings{DFN-concur-2001,
  address = {Aalborg, Denmark},
  month = aug,
  year = 2001,
  volume = 2154,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Larsen, Kim G. and Nielsen, Modens},
  acronym = {{CONCUR}'01},
  booktitle = {{P}roceedings of the 12th 
               {I}nternational {C}onference on
               {C}oncurrency {T}heory
               ({CONCUR}'01)},
  author = {Duflot, Marie and Fribourg, Laurent and Nilsson, Ulf},
  title = {Unavoidable Configurations of Parameterized Rings of
                 Processes},
  pages = {472-486},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFN-concur2001.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFN-concur2001.ps}
}
@inproceedings{DFP-disc2001,
  address = {Lisbon, Portugal},
  month = oct,
  year = 2001,
  volume = 2180,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Welch, Jennifer L.},
  acronym = {{DISC}'01},
  booktitle = {{P}roceedings of the 15th {I}nternational
               {S}ymposium on {D}istributed {C}omputing
               ({DISC}'01)},
  author = {Duflot, Marie and Fribourg, Laurent and Picaronny, Claudine},
  title = {Randomized Finite-State Distributed Algorithms as
                 {M}arkov Chains},
  pages = {240-254},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFP-disc2001.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/DFP-disc2001.ps}
}
@techreport{EVA-TR1,
  author = {Jacquemard, Florent and Le{ }M{\'e}tayer, Daniel},
  title = {Langage de sp{\'e}cification de protocoles
                 cryptographiques de {EVA}: syntaxe concr{\`e}te},
  year = {2001},
  month = nov,
  type = {Technical Report},
  number = 1,
  institution = {projet RNTL~EVA},
  note = {25 pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EVA-TR1.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EVA-TR1.pdf}
}
@techreport{EVA-TR4,
  author = {Bolignano, Dominique and Fiorenza, Francesca and 
                 Jacquemard, Florent and Le{ }M{\'e}tayer, Daniel},
  title = {{EVA} test base},
  year = {2001},
  month = nov,
  type = {Technical Report},
  number = 4,
  institution = {projet RNTL~EVA},
  note = {55 pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EVA-TR4.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EVA-TR4.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/EVA-TR4.ps}
}
@proceedings{Fri-lncs2142,
  title = {{P}roceedings of the 15th {I}nternational
           {W}orkshop on {C}omputer {S}cience {L}ogic
           ({CSL}'01)},
  booktitle = {{P}roceedings of the 15th {I}nternational
               {W}orkshop on {C}omputer {S}cience {L}ogic
               ({CSL}'01)},
  editor = {Fribourg, Laurent},
  publisher = {Springer},
  volume = {2142},
  series = {Lecture Notes in Computer Science},
  year = {2001},
  month = sep,
  address = {Paris, France},
  isbn = {3-540-42554-3},
  url = {http://www.springer.com/978-3-540-42554-3},
  olderurl = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-42554-3}
}
@article{GB-LP-JSTTT00,
  publisher = {Springer},
  journal = {International Journal on Software Tools 
             for Technology Transfer},
  author = {Berthelot, G{\'e}rard and Petrucci, Laure},
  title = {Specification and Validation of a Concurrent System:
                 {A}n Educational Project},
  volume = {3},
  number = {4},
  pages = {372-381},
  year = {2001},
  month = sep,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GB-LP-STTT01.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/GB-LP-STTT01.ps},
  doi = {10.1007/s100090100064}
}
@inproceedings{GL:WFRR,
  address = {Paris, France},
  month = sep,
  year = 2001,
  volume = 2142,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Fribourg, Laurent},
  acronym = {{CSL}'01},
  booktitle = {{P}roceedings of the 15th {I}nternational
               {W}orkshop on {C}omputer {S}cience {L}ogic
               ({CSL}'01)},
  author = {Goubault{-}Larrecq, Jean},
  title = {Well-Founded Recursive Relations},
  pages = {484-497},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Gou-csl2001.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Gou-csl2001.ps}
}
@techreport{JGL:eva:propal,
  author = {Goubault{-}Larrecq, Jean},
  title = {Une proposition de langage de description de
                 protocoles cryptographiques},
  year = {2001},
  month = jul,
  type = {Contract Report},
  number = 2,
  institution = {projet RNTL~EVA},
  note = {12 pages},
  missingcomprehension = {Je ne comprends pas pourquoi cette entree est en RC et pas en wwwpublic, 
                  alors que d'autres contrats EVA sont en TR et wwwpublic public}
}
@techreport{JGL:eva:sem,
  author = {Goubault{-}Larrecq, Jean},
  title = {Les syntaxes et la s{\'e}mantique du langage de
                 sp{\'e}cification~{EVA}},
  year = {2001},
  month = nov,
  type = {Contract Report},
  number = 3,
  institution = {projet RNTL~EVA},
  note = {32 pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EVA-TR3.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/EVA-TR3.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/EVA-TR4.ps}
}
@techreport{LSV:01:13,
  author = {Comon, Hubert and Cortier, V{\'e}ronique},
  title = {Tree Automata with One Memory, Set Constraints and
                 Cryptographic Protocols},
  type = {Research Report},
  number = {LSV-01-13},
  year = {2001},
  month = dec,
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  note = {98 pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2001-13.rr.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
		  rr-lsv-2001-13.rr.ps}
}
@techreport{LSV:01:9,
  author = {Goubault{-}Larrecq, Jean},
  title = {Higher-Order Automata, Pushdown Systems, and Set
                 Constraints},
  type = {Research Report},
  number = {LSV-01-9},
  year = {2001},
  month = nov,
  institution = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  note = {15 pages},
  url = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/rr-lsv-2001-9.rr.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/RAPPORTS_LSV/PS/
		  rr-lsv-2001-9.rr.ps}
}
@techreport{PKDAB-DSTO-01,
  author = {Petrucci, Laure and Kristensen, Lars M. and Dauchy, Pierre 
                 and Aziz, M. and Billington, Jonathan},
  missingauthor = {},
  title = {Modelling and analysis of airborne mission systems},
  year = {2001},
  month = dec,
  type = {Progress Report},
  number = 1,
  institution = {{DSTO/UniSA} contract},
  note = {54 pages}
}
@inproceedings{RGL:TAinCoq,
  address = {Edinburgh, Scotland, UK},
  month = sep,
  year = 2001,
  volume = 2152,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Boulton, Richard J. and Jackson, Paul B.},
  acronym = {{TPHOLs}'01},
  booktitle = {{P}roceedings of the 14th {I}nternational
               {C}onference on {T}heorem {P}roving in
               {H}igher {O}rder {L}ogics
               ({TPHOLs}'01)},
  author = {Rival, Xavier and Goubault{-}Larrecq, Jean},
  title = {Experiments with Finite Tree Automata in {C}oq},
  pages = {362-377},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RivGou-tphol01.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RivGou-tphol01.ps}
}
@inproceedings{RGL:log-art,
  address = {Cape Breton, Nova Scotia, Canada},
  month = jun,
  year = 2001,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{CSFW}'01},
  booktitle = {{P}roceedings of the 
               14th {IEEE} {C}omputer {S}ecurity {F}oundations
               {W}orkshop ({CSFW}'01)},
  author = {Roger, Muriel and Goubault{-}Larrecq, Jean},
  title = {Log Auditing through Model Checking},
  pages = {220-236},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RogGou-csfw01.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/RogGou-csfw01.ps}
}
@inproceedings{Sch-tacs2001,
  address = {Sendai, Japan},
  month = oct,
  year = 2001,
  volume = 2215,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Kobayashi, Naoki and Pierce, Benjamin C.},
  acronym = {{TACS}'01},
  booktitle = {{P}roceedings of the 4th {I}nternational
               {W}orkshop on {T}heoretical {A}spects of
               {C}omputer {S}oftware
               ({TACS}'01)},
  author = {Schnoebelen, {\relax Ph}ilippe},
  title = {Bisimulation and Other Undecidable Equivalences for
                 Lossy Channel Systems},
  pages = {385-399},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-tacs2001.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/Sch-tacs2001.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Sch-tacs2001.ps},
  abstract = {Lossy channel systems are systems of 
	finite state automata that communicate via unreliable 
	unbounded fifo channels. Today the main open question 
	in the theory of lossy channel systems is whether 
	bisimulation is decidable. \par
	We show that bisimulation, simulation, and in fact 
	all relations between bisimulation and trace 
	inclusion are undecidable for lossy channel systems 
	(and for lossy vector addition systems).}
}
@phdthesis{THESE-CANET-2001,
  author = {Canet, G{\'e}raud},
  title = {V{\'e}rification des programmes {\'e}crits dans les langages
                 de programmation~{IL} et~{ST} d{\'e}finis par la norme
                 {IEC}~61131-3},
  year = {2001},
  month = dec,
  type = {Th{\`e}se de doctorat},
  school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Canet-these.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Canet-these.ps}
}
@phdthesis{THESE-NARBONI-2001,
  author = {Narboni, Guy A.},
  title = {Un cas remarquable de syst{\`e}mes lin{\'e}aires: les
                 syst{\`e}mes monotones. {R}{\'e}solution et application {\`a} la
                 v{\'e}rification formelle de programmes},
  year = {2001},
  month = dec,
  school = {Laboratoire Sp{\'e}cification et V{\'e}rification,
               ENS Cachan, France},
  type = {Th{\`e}se de doctorat},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Narboni-these.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Narboni-these.ps}
}
@misc{ap-express01,
  author = {Petit, Antoine},
  title = {About Extensions of Timed Automata},
  howpublished = {Invited talk, 8th {I}nternational {W}orkshop on {E}xpressiveness in
                 {C}oncurrency ({EXPRESS}'01), {A}alborg, {D}enmark},
  year = 2001,
  month = aug
}
@inproceedings{bhk-fossacs2001,
  address = {Genova, Italy},
  month = apr,
  year = 2001,
  volume = 2030,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Honsell, Furio and Miculan, Marino},
  acronym = {{FoSSaCS}'01},
  booktitle = {{P}roceedings of the 4th {I}nternational 
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'01)},
  author = {Bidoit, Michel and Hennicker, Rolf and Kurz, Alexander},
  title = {On the Duality between Observability and
                 Reachability},
  pages = {72-87},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHK-fossacs2001.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BHK-fossacs2001.ps}
}
@inproceedings{ccm-icalp2001,
  address = {Heraklion, Crete, Grece},
  month = jul,
  year = 2001,
  volume = 2076,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Orejas, Fernando and Spirakis, Paul G. and
            van Leeuwen, Jan},
  acronym = {{ICALP}'01},
  booktitle = {{P}roceedings of the 28th {I}nternational 
               {C}olloquium on {A}utomata, {L}anguages and 
               {P}rogramming
               ({ICALP}'01)},
  author = {Comon, Hubert and Cortier, V{\'e}ronique and Mitchell, John},
  title = {Tree Automata with One Memory, Set Constraints and
                 Ping-Pong Protocols},
  pages = {682-693},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CCM-icalp2001.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CCM-icalp2001.ps}
}
@inproceedings{cgn-focs2001,
  address = {Las Vegas, Nevada, USA},
  month = oct,
  year = 2001,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{FOCS}'01},
  booktitle = {{P}roceedings of the 42nd {S}ymposium
               on {F}oundations of {C}omputer {S}cience
              ({FOCS}'01)},
  author = {Comon, Hubert and Godoy, Guillem and Nieuwenhuis, Robert},
  title = {The Confluence of Ground Term Rewrite Systems is
                 Decidable in Polynomial Time},
  pages = {298-307},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CGN-focs2001.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CGN-focs2001.ps}
}
@inproceedings{cmr-csfw2001,
  address = {Cape Breton, Nova Scotia, Canada},
  month = jun,
  year = 2001,
  publisher = {{IEEE} Computer Society Press},
  acronym = {{CSFW}'01},
  booktitle = {{P}roceedings of the 
               14th {IEEE} {C}omputer {S}ecurity {F}oundations
               {W}orkshop ({CSFW}'01)},
  author = {Cortier, V{\'e}ronique and Millen, Jonathan K. and 
                  Rue{\ss}, Harald},
  title = {Proving Secrecy is Easy Enough},
  pages = {97-110},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CMR-csfw2001.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/CMR-csfw2001.ps}
}
@inproceedings{comon01ccl,
  address = {Gif-sur-Yvette, France},
  year = 2001,
  volume = 2002,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Comon, Hubert and March{\'e}, {\relax Cl}aude
            and Treinen, Ralf},
  acronym = {{CCL}'99},
  booktitle = {{R}evised {L}ectures of the
               {I}nternational {S}ummer {S}chool on {C}onstraints
               in {C}omputational {L}ogics
               ({CCL}'99)},
  author = {Comon, Hubert and Kirchner, Claude},
  title = {Constraint Solving on Terms},
  pages = {47-103}
}
@incollection{comon99hb,
  author = {Comon, Hubert},
  title = {Inductionless Induction},
  editor = {Robinson, Alan and Voronkov, Andrei},
  booktitle = {Handbook of Automated Reasoning},
  volume = {1},
  chapter = {14},
  pages = {913-962},
  year = {2001},
  missingmonth = {},
  missingnmonth = {},
  publisher = {Elsevier Science Publishers},
  isbn = {0-444-82949-0},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HC-hb.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/HC-hb.ps}
}
@mastersthesis{corbineau-dea,
  author = {Corbineau, Pierre},
  title = {Autour de la cl{\^o}ture de congruence avec {C}oq},
  year = {2001},
  month = sep,
  school = {{DEA} Programmation, Paris, France},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Corbineau-dea2001.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Corbineau-dea2001.ps}
}
@article{finkel98b,
  publisher = {Elsevier Science Publishers},
  journal = {Theoretical Computer Science},
  author = {Finkel, Alain and Schnoebelen, {\relax Ph}ilippe},
  title = {Well-Structured Transition Systems Everywhere!},
  volume = {256},
  number = {1-2},
  pages = {63-92},
  year = {2001},
  month = apr,
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FinSch-TCS99.pdf},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FinSch-TCS99.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinSch-TCS99.ps},
  doi = {10.1016/S0304-3975(00)00102-X},
  abstract = {Well-structured transition systems 
	(WSTS's) are a general class of infinite state 
	systems for which decidability results rely on the 
	existence of a well-quasi-ordering between states 
	that is compatible with the transitions.\par
	In this article, we provide an extensive treatment 
	of the WSTS idea and show several new results.  
	Our improved definitions allow many examples of 
	classical systems to be seen as instances of 
	WSTS's.}
}
@mastersthesis{hornus-dea,
  author = {Hornus, Samuel},
  title = {Requ{\^e}tes en logique temporelle},
  year = {2001},
  month = sep,
  school = {{DEA} Algorithmique, Paris, France},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Hornus-dea2001.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/Hornus-dea2001.ps}
}
@inproceedings{lms-fossacs2001,
  address = {Genova, Italy},
  month = apr,
  year = 2001,
  volume = 2030,
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  editor = {Honsell, Furio and Miculan, Marino},
  acronym = {{FoSSaCS}'01},
  booktitle = {{P}roceedings of the 4th {I}nternational 
               {C}onference on {F}oundations of {S}oftware {S}cience
               and {C}omputation {S}tructures
               ({FoSSaCS}'01)},
  author = {Laroussinie, Fran{\c{c}}ois and Markey, Nicolas and 
                 Schnoebelen, {\relax Ph}ilippe},
  title = {Model checking {CTL}{\(^+\)} and {FCTL} is~hard},
  pages = {318-331},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-fossacs2001.pdf},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/LMS-fossacs2001.ps},
  pdf = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/LMS-fossacs2001.pdf},
  abstract = {Among the branching-time temporal logics used for the 
	specification and verification of systems, CTL\(^+\), FCTL and ECTL\(^+\) 
	are the
	most notable logics for which the precise computational complexity of
	model checking is not known. We answer this longstanding open 
	problem and show that model checking these (and some related) logics is
	\(\Delta_2^p\)-complete.}
}
@book{lsvmcbook01,
  author = {B{\'e}rard, B{\'e}atrice and Bidoit, Michel and Finkel, Alain 
                 and Laroussinie, Fran{\c{c}}ois and 
                 Petit, Antoine and Petrucci, Laure and 
                 Schnoebelen, {\relax Ph}ilippe},
  title = {Systems and Software Verification. {M}odel-Checking
                 Techniques and Tools},
  year = {2001},
  missingmonth = {},
  missingnmonth = {},
  publisher = {Springer},
  isbn = {3-540-41523-8},
  url = {http://www.springer.com/978-3-540-41523-8},
  olderurl = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-41523-8}
}
@phdthesis{phs-hab-01,
  author = {Schnoebelen, {\relax Ph}ilippe},
  title = {Sp{\'e}cification et v{\'e}rification des syst{\`e}mes
                 concurrents},
  year = {2001},
  month = oct,
  type = {M{\'e}moire d'habilitation},
  school = {Universit{\'e} Paris~7, Paris, France},
  url = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/phs-habile.ps},
  ps = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/phs-habile.ps}
}
@mastersthesis{pichon-dea,
  author = {Pichon, {\'E}ric},
  title = {Preuves observationnelles},
  year = {2001},
  month = sep,
  school = {{DEA} Programmation, Paris, France}
}
@book{scopos13-2001,
  author = {Badouel, {\'E}ric and Boucheron, St{\'e}phane and 
                 Dicky, Anne and Petit, Antoine
                 and Santha, Miklos and Weil, Pascal and Zeitoun, Marc},
  title = {Probl\`{e}mes d'informatique fondamentale},
  publisher = {Springer},
  volume = {13},
  series = {Scopos},
  year = {2001},
  missingmonth = {},
  missingnmonth = {},
  isbn = {3-540-42341-9},
  url = {http://www.springer.com/978-3-540-42341-9},
  olderurl = {http://www.springer.de/cgi-bin/search_book.pl?isbn=3-540-42341-9}
}
@comment{{B-arxiv16,
  author =		Bollig, Benedikt, 
  affiliation = 	aff-LSVmexico,
  title =    		One-Counter Automata with Counter Visibility, 
  institution = 	Computing Research Repository, 
  number =    		1602.05940, 
  month = 		feb, 
  nmonth =     		2,
  year = 		2016, 
  type = 		RR, 
  axeLSV = 		mexico,
  NOcontrat = 		"",
  
  url =			http://arxiv.org/abs/1602.05940, 
  PDF =			"http://www.lsv.fr/Publis/PAPERS/PDF/B-arxiv16.pdf",
  lsvdate-new =  	20160222,
  lsvdate-upd =  	20160222,
  lsvdate-pub =  	20160222,
  lsv-category = 	"rapl",
  wwwpublic =    	"public and ccsb",
  note = 		18~pages, 

  abstract = "In a one-counter automaton (OCA), one can read a letter
    from some finite alphabet, increment and decrement the counter by
    one, or test it for zero. It is well-known that universality and
    language inclusion for OCAs are undecidable. We consider here OCAs
    with counter visibility: Whenever the automaton produces a letter,
    it outputs the current counter value along with~it. Hence, its
    language is now a set of words over an infinite alphabet. We show
    that universality and inclusion for that model are in PSPACE, thus
    no harder than the corresponding problems for finite automata, which
    can actually be considered as a special case. In fact, we show that
    OCAs with counter visibility are effectively determinizable and
    closed under all boolean operations. As~a~strict generalization, we
    subsequently extend our model by registers. The general nonemptiness
    problem being undecidable, we impose a bound on the number of
    register comparisons and show that the corresponding nonemptiness
    problem is NP-complete.",
}}

This file was generated by bibtex2html 1.98.