@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.