persee.bib

@COMMENT{{{This file has been generated by bib2bib 1.75}}
@COMMENT{{{Command line: bib2bib -ob persee.bib abbrevs-lsv.bib persee-src.bib}}

@INPROCEEDINGS{BLP-cav06,
  TITLE = {{FAST} {E}xtended {R}elease},
  AUTHOR = {Bardin, S. and Leroux, J. and Point, G.},
  BOOKTITLE = {{P}roceedings of the 18th {I}nternational {C}onference on {C}omputer {A}ided {V}erification ({CAV}'06), Seattle, Washington, USA, Aug. 2006},
  PAGES = {63-66},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {4144},
  YEAR = {2006}
}

@INPROCEEDINGS{L-ATVA04,
  AUTHOR = {Leroux, J.},
  TITLE = {Disjunctive invariants for numerical systems},
  BOOKTITLE = {Proc. 2nd Int. Symp. Automated Technology for Verification and Analysis (ATVA'2004), Taipei, Taiwan, Nov. 2004},
  YEAR = {2004},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 3299,
  PAGES = {99--107}
}

@INPROCEEDINGS{L-LICS05,
  AUTHOR = {Leroux, J.},
  TITLE = {A polynomial-time Presburger criterion and synthesis for number decision diagrams},
  BOOKTITLE = {Proc. 20th Annual IEEE Symposium on Logic in Computer Science (LICS'05),  Chicago, USA June 2005},
  YEAR = {2005},
  PUBLISHER = {IEEE Comp.\ Soc.\ Press},
  PAGES = {147--156}
}

@INPROCEEDINGS{Leroux:2005:ATVA,
  AUTHOR = {Leroux, J. and Sutre, G.},
  TITLE = {Flat counter automata almost everywhere!},
  BOOKTITLE = {Proc.\ 3rd Int.\ Symp.\ Automated Technology for Verification and Analysis
		  (ATVA'05), Taipei, Taiwan, Oct.\ 2005},
  VOLUME = {3707},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer},
  PAGES = {489--503},
  YEAR = {2005}
}

@INPROCEEDINGS{FGRV-express04,
  AUTHOR = {Finkel, A. and Geeraerts, G. and
                   Raskin, {J-F} and Van{ }Begin, L.},
  BOOKTITLE = {{P}roceedings of the 11th {I}nternational {W}orkshop
                   on {E}xpressiveness in {C}oncurrency ({EXPRESS}'04)},
  MONTH = APR,
  NUMBER = {2},
  PAGES = {87-101},
  PUBLISHER = {Elsevier Science Publishers},
  SERIES = {Electronic Notes in Theoretical Computer Science},
  TITLE = {On the Omega-Language Expressive Power of Extended
                   {P}etri Nets},
  VOLUME = {128},
  YEAR = {2005},
  NMONTH = {4},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGRV-express04.pdf}
}

@PHDTHESIS{THESE-bertrand06,
  AUTHOR = {Bertrand, N.},
  MONTH = SEP,
  SCHOOL = {Laboratoire Sp{\'e}cification et V{\'e}rification,
                   ENS Cachan, France},
  TYPE = {Th{\`e}se de doctorat},
  TITLE = {Mod{\`e}les stochastiques pour les pertes de messages
                   dans les protocoles asynchrones et techniques de
                   v{\'e}rification automatique},
  YEAR = {2006},
  NMONTH = {9},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/these-bertrand.pdf}
}

@INPROCEEDINGS{touili2007,
  AUTHOR = {T. Touili and M. Sighireanu},
  BOOKTITLE = {Proc.\ 8th Int.\ Workshop on Verification of Infinite
                   State Systems (INFINITY 2006)},
  NOTE = {To appear},
  PUBLISHER = {Elsevier Science},
  URL = {http://www.liafa.jussieu.fr/~touili/express06.ps.gz},
  SERIES = {Electronic Notes in Theor.\ Comp.\ Sci.},
  TITLE = {Bounded Communication Reachability Analysis of
                   Process Rewrite Systems with Ordered Parallelism},
  YEAR = {2007}
}

@INPROCEEDINGS{touili-vissas05,
  AUTHOR = {T. Touili},
  BOOKTITLE = {Proc.\ NATO Advanced Research Workshop on
                   Verification of Infinite State Systems with
                   Applications to Security (VISSAS 2005)},
  PAGES = {213--227},
  PUBLISHER = {IOS Press},
  URL = {http://www.liafa.jussieu.fr/~touili/vissas.ps.gz},
  TITLE = {Dealing with Communication for Dynamic Multithreaded
                   Recursive Programs},
  YEAR = {2006}
}

@INPROCEEDINGS{meyer04,
  AUTHOR = {A. Meyer},
  BOOKTITLE = {Proc.\ 7th Int.\ Conf.\ Foundations of Software
                   Science and Computation Structures (FOSSACS 2004)},
  MONTH = APR,
  PAGES = {378--392},
  PUBLISHER = {Springer},
  URL = {http://www.liafa.jussieu.fr/~ameyer/binaires/fossacs04.pdf},
  SERIES = {Lecture Notes in Computer Science},
  TITLE = {On Term Rewriting Systems Having a Rational
                   Derivation},
  VOLUME = {2987},
  YEAR = {2004}
}

@INPROCEEDINGS{leroux2005,
  AUTHOR = {J. Leroux},
  BOOKTITLE = {Proc.\ 20th IEEE Symp.\ Logic in Computer Science
                   (LICS 2005)},
  MONTH = JUN,
  PAGES = {147--156},
  PUBLISHER = {IEEE Comp.\ Soc.\ Press},
  TITLE = {A Polynomial Time {Presburger} Criterion and
                   Synthesis for Number Decision Diagrams},
  URL = {http://www.irisa.fr/vertecs/Equipe/Leroux/papiers/papier.lics05.ps},
  YEAR = {2005}
}

@INPROCEEDINGS{Ler-atva04,
  AUTHOR = {J. Leroux},
  BOOKTITLE = {Proc.\ 2nd Int.\ Symp.\ Automated Technology for
                   Verification and Analysis (ATVA 2004)},
  MONTH = NOV,
  PAGES = {93--107},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  TITLE = {Disjunctive Invariants for Numerical Systems},
  VOLUME = {3299},
  YEAR = {2004}
}

@INPROCEEDINGS{ChakiCKRT06,
  AUTHOR = {S. Chaki and E. M. Clarke and N. Kidd and Th. W. Reps and
                   T. Touili},
  BOOKTITLE = {Proc.\ 12th Int.\ Conf.\ Tools and Algorithms for the
                   Construction and Analysis of Systems (TACAS 2006)},
  MONTH = MAR,
  URL = {http://www.liafa.jussieu.fr/~touili/tacas06.ps.gz},
  PAGES = {334--349},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  TITLE = {Verifying Concurrent Message-Passing {C} Programs
                   with Recursive Calls},
  VOLUME = {3920},
  YEAR = {2006}
}

@INPROCEEDINGS{CCGOSTV05,
  AUTHOR = {S. Chaki and E. M. Clarke and O. Grumberg and
                   J. Ouaknine and N. Sharygina and T. Touili and
                   H. Veith},
  BOOKTITLE = {Proc.\ 5th Int.\ Conf.\ Integrated Formal Methods
                   (IFM 2005)},
  PAGES = {53--69},
  MONTH = NOV,
  PUBLISHER = {Springer},
  URL = {http://www.liafa.jussieu.fr/~touili/seaw.ps.gz},
  SERIES = {Lecture Notes in Computer Science},
  TITLE = {State/Event Software Verification for Branching-Time
                   Specifications},
  VOLUME = {3771},
  YEAR = {2005}
}

@INPROCEEDINGS{bouajjani-rta05,
  AUTHOR = {A. Bouajjani and T. Touili},
  BOOKTITLE = {Proc.\ 16th Int.\ Conf.\ Term Rewriting and
                   Applications (RTA 2005)},
  PAGES = {484--499},
  MONTH = APR,
  PUBLISHER = {Springer},
  URL = {http://www.liafa.jussieu.fr/~touili/rta05.ps.gz},
  SERIES = {Lecture Notes in Computer Science},
  TITLE = {On Computing Reachability Sets of Process Rewrite
                   Systems},
  VOLUME = {3467},
  YEAR = {2005}
}

@INPROCEEDINGS{BST-express-2006,
  AUTHOR = {A. Bouajjani and J. Strej{\v{c}}ek and T. Touili},
  BOOKTITLE = {Proc.\ 13th Int.\ Workshop on Expressiveness in
                   Concurrency (EXPRESS 2006)},
  NOTE = {To appear},
  PUBLISHER = {Elsevier Science},
  SERIES = {Electronic Notes in Theor.\ Comp.\ Sci.},
  TITLE = {On symbolic verification of weakly extended {PAD}},
  YEAR = {2007},
  URL = {http://www.liafa.jussieu.fr/~touili/express06.ps.gz}
}

@INPROCEEDINGS{bouajjani-vissas05,
  AUTHOR = {A. Bouajjani},
  BOOKTITLE = {Proc.\ NATO Advanced Research Workshop on
                   Verification of Infinite State Systems with
                   Applications to Security (VISSAS 2005)},
  PAGES = {17--22},
  PUBLISHER = {IOS Press},
  TITLE = {Regular Model Checking for Programs with Dynamic
                   Memory},
  YEAR = {2006}
}

@INPROCEEDINGS{bouajjani-concur05,
  AUTHOR = {A. Bouajjani and M. M{\"u}ller-Olm and T. Touili},
  BOOKTITLE = {Proc.\ 16th Int.\ Conf.\ Concurrency Theory (CONCUR
                   2005)},
  MONTH = AUG,
  URL = {http://www.liafa.jussieu.fr/~abou/concur05-long-version.ps.gz},
  PAGES = {474--487},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  TITLE = {Regular Symbolic Analysis of Dynamic Networks of
                   Pushdown Systems},
  VOLUME = {3653},
  YEAR = {2005}
}

@INPROCEEDINGS{BHRV05,
  AUTHOR = {A. Bouajjani and P. Habermehl and A. Rogalewicz and
                   T. Vojnar},
  BOOKTITLE = {Proc.\ 7th Int.\ Workshop on Verification of Infinite
                   State Systems (INFINITY 2005)},
  MONTH = FEB,
  URL = {http://www.liafa.jussieu.fr/~haberm/Publications/bhrvinfinity05.ps.gz},
  PAGES = {37--48},
  PUBLISHER = {Elsevier Science},
  SERIES = {Electronic Notes in Theor.\ Comp.\ Sci.},
  TITLE = {Abstract Regular Tree Model Checking},
  VOLUME = {149(1)},
  YEAR = {2006}
}

@INPROCEEDINGS{BHMV-tacas05,
  AUTHOR = {A. Bouajjani and P. Habermehl and P. Moro and
                   T. Vojnar},
  BOOKTITLE = {Proc.\ 11th Int.\ Conf.\ Tools and Algorithms for the
                   Construction and Analysis of Systems (TACAS 2005)},
  MONTH = APR,
  PAGES = {13--39},
  SERIES = {Lecture Notes in Computer Science},
  URL = {http://www.liafa.jussieu.fr/~haberm/Publications/bhmvtacas05.ps.gz},
  TITLE = {Verifying Programs with Dynamic 1-Selector-Linked
                   Structures in Regular Model Checking},
  VOLUME = {3440},
  YEAR = {2005}
}

@INPROCEEDINGS{BouajjaniESS05,
  AUTHOR = {A. Bouajjani and J. Esparza and S. Schwoon and
                   J. Strejcek},
  BOOKTITLE = {Proc.\ 25th Conf.\ Found.\ of Software Technology and
                   Theor.\ Comp.\ Sci.\ (FST\&TCS 2005)},
  PAGES = {348--359},
  URL = {http://www.liafa.jussieu.fr/~abou/adpn-fsttcs05.ps.gz},
  MONTH = DEC,
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  TITLE = {Reachability Analysis of Multithreaded Software with
                   Asynchronous Communication},
  VOLUME = {3821},
  YEAR = {2005}
}

@INPROCEEDINGS{BouajjaniE-rta06,
  AUTHOR = {A. Bouajjani and J. Esparza},
  BOOKTITLE = {Proc.\ 17th Int.\ Conf.\ Term Rewriting and
                   Applications (RTA 2006)},
  PAGES = {136--150},
  MONTH = AUG,
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  TITLE = {Rewriting Models of Boolean Programs},
  VOLUME = {4098},
  URL = {http://www.liafa.jussieu.fr/~abou/rta06.pdf},
  YEAR = {2006}
}

@INPROCEEDINGS{bouajjani2006,
  AUTHOR = {A. Bouajjani and M. Bozga and P. Habermehl and
                   R. Iosif and P. Moro and T. Vojnar},
  BOOKTITLE = {Proc.\ 18th Int.\ Conf.\ Computer Aided Verification
                   (CAV 2006)},
  PAGES = {517--531},
  PUBLISHER = {Springer},
  MONTH = AUG,
  URL = {http://www.liafa.jussieu.fr/~abou/lp2c-long.pdf},
  SERIES = {Lecture Notes in Computer Science},
  TITLE = {Programs with Lists are Counter Automata},
  VOLUME = {4144},
  YEAR = {2006}
}

@INPROCEEDINGS{BH:CAV:2006,
  AUTHOR = {Boigelot, B. and Herbreteau, F.},
  TITLE = {The Power of Hybrid Acceleration},
  BOOKTITLE = {Proc. of the 18th Int. Conf. on Computer Aided Verification (CAV06)},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {4144},
  PAGES = {438--451},
  MONTH = AUG,
  YEAR = {2006},
  PUBLISHER = {Springer},
  URL = {http://www.labri.fr/~herbrete/publications/cav06/BH-cav06.pdf}
}

@INPROCEEDINGS{DDFG:ATVA:2006,
  AUTHOR = {Demri, S. and Finkel, A. and
                   Goranko, V. and van{ }Drimmelen, G.},
  BOOKTITLE = {{P}roceedings of the 4th {I}nternational {S}ymposium
                   on {A}utomated {T}echnology for {V}erification and
                   {A}nalysis ({ATVA}'06)},
  MONTH = OCT,
  PAGES = {493-507},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  TITLE = {Towards a model-checker for counter systems},
  VOLUME = {4218},
  YEAR = {2006},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DDFG-atva06.pdf}
}

@ARTICLE{CF:IC:2005,
  AUTHOR = {C{\'e}c{\'e}, G. and Finkel, A.},
  JOURNAL = {Information and Computation},
  MONTH = NOV,
  NUMBER = {2},
  PAGES = {166-190},
  TITLE = {Verification of Programs with Half-Duplex
                   Communication},
  VOLUME = {202},
  YEAR = {2005},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/CF-icomp05.pdf}
}

@ARTICLE{FL:IPL:2005,
  AUTHOR = {Finkel, A. and Leroux, J.},
  JOURNAL = {Information Processing Letters},
  MONTH = OCT,
  NUMBER = {1},
  PAGES = {30-35},
  TITLE = {The Convex Hull of a Regular Set of Integer Vectors
                   is Polyhedral and Effectively Computable},
  VOLUME = {96},
  YEAR = {2005},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FL-ipl05.pdf}
}

@ARTICLE{FMP:IC:2004,
  AUTHOR = {Finkel, A. and McKenzie, P. and
                   Picaronny, C.},
  JOURNAL = {Information and Computation},
  MONTH = NOV,
  NUMBER = {1-2},
  PAGES = {1--29},
  TITLE = {A Well-Structured Framework for Analysing {P}etri
                   Nets Extensions},
  VOLUME = {195},
  YEAR = {2004},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FMP-wstsPN-icomp.ps}
}

@ARTICLE{FGRV:TCS:2005,
  AUTHOR = {Finkel, A. and Geeraerts, G. and
                   Raskin, {J.-F.} and Van{ }Begin, L.},
  JOURNAL = {Theoretical Computer Science},
  MONTH = MAY,
  NUMBER = {3},
  PAGES = {374-386},
  TITLE = {On the \(\omega\)-Language Expressive Power of
                   Extended {P}etri Nets},
  VOLUME = {356},
  YEAR = {2006},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FGRV-TCS04.pdf}
}

@INPROCEEDINGS{DFV:AVOCS:2004,
  AUTHOR = {Darlot, {\relax Ch.} and Finkel, A. and
                   Van{ }Begin, L.},
  BOOKTITLE = {{P}roceedings of the 4th {I}nternational {W}orkshop
                   on {A}utomated {V}erification of {C}ritical {S}ystems
                   ({AVoCS}'04)},
  MONTH = MAY,
  NUMBER = {6},
  PAGES = {87-103},
  SERIES = {Electronic Notes in Theor.\ Comp.\ Sci.},
  TITLE = {About {F}ast and {TReX} accelerations},
  VOLUME = {128},
  YEAR = {2005},
  PUBLISHER = {Elsevier Science},
  NMONTH = {5},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/DFV-avocs04.pdf}
}

@PHDTHESIS{Bardin:THESE:2005,
  AUTHOR = {Bardin, S.},
  MONTH = OCT,
  SCHOOL = {Laboratoire Sp{\'e}cification et V{\'e}rification,
                   ENS Cachan, France},
  TYPE = {Th{\`e}se de doctorat},
  TITLE = {Vers un model checking avec acc{\'e}l{\'e}ration
                   plate de syst{\`e}mes h{\'e}t{\'e}rog{\`e}nes},
  YEAR = {2005},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/bardin-THESE.pdf}
}

@ARTICLE{KS:TCS:2006,
  AUTHOR = {Ku{\v c}era, A. and
                   Schnoebelen, {\relax Ph.}},
  JOURNAL = {Theoretical Computer Science},
  MONTH = AUG,
  NUMBER = {2-3},
  PAGES = {315-333},
  TITLE = {A General Approach to Comparing Infinite-State
                   Systems with Their Finite-State Specifications},
  VOLUME = {358},
  YEAR = {2006},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/KucSch-TCS.pdf}
}

@ARTICLE{BBS:ACMTCL:2006,
  AUTHOR = {Baier, {\relax Ch.} and Bertrand, N. and
                   Schnoebelen, {\relax Ph.}},
  JOURNAL = {ACM Transactions on Computational Logic},
  NOTE = {To appear},
  PUBLISHER = {ACM Press},
  TITLE = {Verifying nondeterministic probabilistic channel
                   systems against \(\omega\)-regular linear-time
                   properties},
  YEAR = {2007},
  URL = {http://arxiv.org/abs/cs.LO/0511023}
}

@INPROCEEDINGS{BBS:LPAR:2006,
  AUTHOR = {Baier, {\relax Ch.} and Bertrand, N. and
                   Schnoebelen, {\relax Ph.}},
  BOOKTITLE = {{P}roceedings of the 13th {I}nternational
                   {C}onference on {L}ogic for {P}rogramming,
                   {A}rtificial {I}ntelligence, and {R}easoning
                   ({LPAR}'06)},
  MONTH = NOV,
  PAGES = {347-361},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Artificial Intelligence},
  TITLE = {On Computing Fixpoints in Well-Structured Regular
                   Model Checking, with Applications to Lossy Channel
                   Systems},
  VOLUME = {4246},
  YEAR = {2006},
  NMONTH = {11},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-lpar06.pdf}
}

@INPROCEEDINGS{BBS:FORTE:2006,
  AUTHOR = {Baier, {\relax Ch.} and Bertrand, N. and
                   Schnoebelen, {\relax Ph.}},
  BOOKTITLE = {{P}roceedings of 26th {IFIP} {WG6.1} {I}nternational
                   {C}onference on {F}ormal {T}echniques for {N}etworked
                   and {D}istributed {S}ystems ({FORTE}'06)},
  MONTH = SEP,
  PUBLISHER = {Springer},
  PAGES = {212-227},
  VOLUME = {4229},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-forte06.pdf},
  SERIES = {Lecture Notes in Computer Science},
  TITLE = {Symbolic verification of communicating systems with
                   probabilistic message losses: liveness and fairness},
  YEAR = {2006},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BBS-forte06.pdf}
}

@ARTICLE{ABRS:IC:2005,
  AUTHOR = {Abdulla, {P. A.} and Bertrand, N. and Rabinovich, A. and Schnoebelen, {\relax Ph.}},
  JOURNAL = {Information and Computation},
  MONTH = NOV,
  NUMBER = {2},
  PAGES = {141-165},
  PUBLISHER = {Elsevier Science Publishers},
  TITLE = {Verification of Probabilistic Systems with Faulty
                   Communication},
  VOLUME = {202},
  YEAR = {2005},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/InfComp-ABRS.pdf}
}

@ARTICLE{BBS:IPL:2005,
  AUTHOR = {Baier, {\relax Ch.} and Bertrand, N. and Schnoebelen, {\relax Ph.}},
  JOURNAL = {Information Processing Letters},
  MONTH = JAN,
  NUMBER = {2},
  PAGES = {58-63},
  PUBLISHER = {Elsevier Science Publishers},
  TITLE = {A note on the attractor-property of infinite-state {M}arkov chains},
  VOLUME = {97},
  YEAR = {2006},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/IPL-BBS.pdf}
}

@INPROCEEDINGS{BS:EXPRESS:2005,
  AUTHOR = {Bertrand, N. and
                   Schnoebelen, {\relax Ph.}},
  BOOKTITLE = {{P}roceedings of the 12th {I}nternational {W}orkshop
                   on {E}xpressiveness in {C}oncurrency ({EXPRESS} 2005)},
  MONTH = JUL,
  NUMBER = {3},
  PAGES = {59-69},
  SERIES = {Electronic Notes in Theor.\ Comp.\ Sci.},
  PUBLISHER = {Elsevier Science},
  TITLE = {A short visit to the {STS} hierarchy},
  VOLUME = {154},
  YEAR = {2006},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BS05-express.pdf}
}

@INPROCEEDINGS{BFLS:ATVA:2005,
  AUTHOR = {Bardin, S. and Finkel, A. and Leroux, J. and Schnoebelen, {\relax Ph.}},
  BOOKTITLE = {{P}roceedings of the 3rd {I}nternational {S}ymposium
                   on {A}utomated {T}echnology for {V}erification and
                   {A}nalysis ({ATVA}'05)},
  MONTH = OCT,
  PAGES = {474-488},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  TITLE = {Flat acceleration in symbolic model checking},
  VOLUME = {3707},
  YEAR = {2005},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLS05-atva.pdf}
}

@ARTICLE{LS:IC:2005,
  AUTHOR = {Lugiez, D. and Schnoebelen, {\relax Ph.}},
  JOURNAL = {Information and Computation},
  MONTH = NOV,
  NUMBER = {1},
  PAGES = {75-113},
  PUBLISHER = {Elsevier Science Publishers},
  TITLE = {Decidable first-order transition logics for
                   {PA}-processes},
  VOLUME = {203},
  YEAR = {2005},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/InfComp-C2707.pdf}
}

@INPROCEEDINGS{BF:ATVA:2004,
  AUTHOR = {Bardin, S. and Finkel, A.},
  BOOKTITLE = {Proc.\ 2nd Int.\ Symp.\ Automated Technology for Verification and Analysis (ATVA 2004)},
  MONTH = OCT,
  PAGES = {248-262},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  TITLE = {Composition of accelerations to verify infinite heterogeneous 
systems},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/BF-atva04.ps.gz},
  VOLUME = {3299},
  YEAR = {2004}
}

@INPROCEEDINGS{GV:TMMC:2004,
  AUTHOR = {Griffault, A. and Vincent, A.},
  TITLE = {The Mec~5 model-checker},
  BOOKTITLE = {Proc.\ 16th Int.\ Conf.\ Computer Aided Verification
		  (CAV 2004)},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer},
  VOLUME = {3114},
  PAGES = {488--491},
  MONTH = JUL,
  YEAR = {2004},
  PS = {http://www.labri.fr/Perso/~vincent/Research/GV-TMMC-2004.ps}
}

@INCOLLECTION{Kordon:2004:BOOK,
  AUTHOR = {Bréant, F. and Couvreur, {J.-M.} and Gilliers, F. and Kordon, F. and Mounier, I. and Paviot-Adet, E. and Poitrenaud, D. and Regep, D. and Sutre, G.},
  TITLE = {Modeling and verifying behavioral aspects},
  BOOKTITLE = {Formal Methods for Embedded Distributed Systems · How to master the complexity},
  CHAPTER = {6},
  PUBLISHER = {Kluwer Academic},
  PAGES = {171--211},
  YEAR = {2004}
}

@INPROCEEDINGS{C:Couvreur:2002:ICATPN,
  AUTHOR = {Couvreur, {J.-M.} and Encrenaz, E.  and
                 Paviot-Adet, E. and Poitrenaud, D.  and
                 Wacrenier, {P.-A.}},
  TITLE = {Data Decision Diagrams for {Petri} Net Analysis.},
  BOOKTITLE = {Proc.\ 23rd Int.\ Conf.\ Applications and Theory of Petri Nets,  (ICATPN'2002)},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {2360},
  MONTH = OCT,
  PAGES = {101--120},
  PUBLISHER = {Springer},
  YEAR = {2002}
}

@INPROCEEDINGS{C:Couvreur:2005:ICATPN,
  AUTHOR = {Barkaoui, K. and Couvreur, {J.-M.} and Klai, K.},
  TITLE = {On the equivalence between liveness and deadlock-freeness in {Petri} nets},
  BOOKTITLE = {Proc. 26th Int. Conf Applications and Theory of Petri Nets,  (ICATPN'2005)},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 3536,
  MONTH = NOV,
  PAGES = {90--107},
  PUBLISHER = {Springer},
  YEAR = {2005}
}

@INPROCEEDINGS{C:Couvreur:2004:CIAA,
  AUTHOR = {Couvreur, {J.-M.}},
  TITLE = {A {BDD}-like Implementation of an Automata Package},
  BOOKTITLE = {Proc. 9th Int. Conf. Implementation and Application of Automata (CIAA'2004)},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {3317},
  PAGES = {310-311},
  PUBLISHER = {Springer},
  MONTH = DEC,
  YEAR = {2005}
}

@INPROCEEDINGS{BerSch-avis2004,
  AUTHOR = {N. Bertrand and {\relax Ph.} Schnoebelen},
  TITLE = {Verifying Nondeterministic Channel Systems With Probabilistic
                  Message Losses},
  BOOKTITLE = {Proc.\ 3rd Int.\ Workshop on Automated Verification of
                  Infinite-State Systems (AVIS 2004)},
  ADDRESS = {Barcelona, Spain},
  MONTH = APR,
  YEAR = 2004,
  EDITOR = {Bharadwaj, Ramesh},
  PDF = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/BerSch-avis04.pdf}
}

@INPROCEEDINGS{NowakDJJ:towsvp,
  AUTHOR = {S. Bardin and A. Finkel and D. Nowak},
  TITLE = {Toward symbolic verification of programs handling pointers},
  BOOKTITLE = {Proc.\ 3rd Int.\ Workshop on Automated Verification of
                  Infinite-State Systems (AVIS 2004)},
  MONTH = APR,
  YEAR = 2004,
  ADDRESS = {Barcelona, Spain},
  EDITOR = {Bharadwaj, Ramesh},
  PS = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/BFN-avis2004.ps}
}

@INPROCEEDINGS{Leroux:2004:CONCUR,
  AUTHOR = {Leroux, J. and Sutre, G.},
  TITLE = {On Flatness for 2-dimensional Vector Addition Systems with States},
  BOOKTITLE = {Proc.\ 15th Int.\ Conf.\ Concurrency Theory
		  (CONCUR 2004)},
  VOLUME = {3170},
  SERIES = {Lecture Notes in Computer Science},
  MONTH = AUG,
  PUBLISHER = {Springer},
  PAGES = {402--416},
  YEAR = {2004},
  PS = {http://www.labri.fr/~sutre/Publications/Documents/Leroux:2004:CONCUR-Long.ps.gz}
}

@INPROCEEDINGS{Adelaide:2004:BioCONCUR,
  AUTHOR = {Ad{\'e}la{\"\i}de, M. and Sutre, G.},
  TITLE = {Parametric Analysis and Abstraction of Genetic
                     Regulatory Networks},
  BOOKTITLE = {Proc.\ 2nd Workshop on Concurrent Models in Molecular Biology (BioCONCUR'04)},
  NOTE = {To appear},
  SERIES = {Electronic Notes in Theor.\ Comp.\ Sci.},
  PUBLISHER = {Elsevier Science},
  YEAR = {2007},
  PS = {http://www.labri.fr/~sutre/Publications/Documents/Adelaide:2004:BioCONCUR.ps.gz}
}

@INPROCEEDINGS{Henzinger:2002:POPL,
  AUTHOR = {Henzinger, {T. A.} and Jhala, R. and Majumdar, R. and
                     Sutre, G.},
  TITLE = {Lazy Abstraction},
  BOOKTITLE = {Proc.\ 29th ACM Symp.\ Principles of Programming
		  Languages (POPL 2002)},
  MONTH = JAN,
  PUBLISHER = {ACM Press},
  PAGES = {58--70},
  YEAR = {2002},
  PS = {http://www.labri.fr/~sutre/Publications/Documents/Henzinger:2002:POPL.ps.gz}
}

@INPROCEEDINGS{BerSch-fossacs2003,
  AUTHOR = {Bertrand, N. and Schnoebelen, {\relax Ph.}},
  BOOKTITLE = {Proc.\ 6th Int.\ Conf.\ Foundations of Software Science and
		  Computation Structures (FOSSACS 2003)},
  TITLE = {Model Checking Lossy Channels Systems Is Probably Decidable},
  VOLUME = {2620},
  PUBLISHER = {Springer},
  MONTH = APR,
  PAGES = {120--135},
  YEAR = {2003},
  SERIES = {Lecture Notes in Computer Science},
  PS = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/BerSch-fossacs2003.ps}
}

@INPROCEEDINGS{KucSch2004,
  AUTHOR = {Ku{\v{c}}era, A. and Schnoebelen, {\relax Ph.}},
  BOOKTITLE = {Proc.\ 15th Int.\ Conf.\ Concurrency Theory
		  (CONCUR 2004)},
  TITLE = {A General Approach to Comparing Infinite-State Systems with Their Finite-State Specifications},
  VOLUME = {3170},
  MONTH = AUG,
  PUBLISHER = {Springer},
  PAGES = {371--386},
  YEAR = {2004},
  SERIES = {Lecture Notes in Computer Science},
  PDF = {http://www.fi.muni.cz/informatics/reports/files/2004/FIMU-RS-2004-05.pdf}
}

@INCOLLECTION{Sch-voss,
  AUTHOR = {Schnoebelen, {\relax Ph.}},
  BOOKTITLE = {Validation of Stochastic Systems -- A Guide to Current Research},
  TITLE = {The Verification of Probabilistic Lossy Channel Systems},
  VOLUME = {2925},
  PUBLISHER = {Springer},
  PAGES = {445--465},
  YEAR = {2004},
  MONTH = AUG,
  SERIES = {Lecture Notes in Computer Science},
  PS = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/Sch-voss.ps}
}

@INPROCEEDINGS{FAST-cav03,
  AUTHOR = {S. Bardin and A. Finkel and J. Leroux and L.
                 Petrucci},
  TITLE = {{FAST}: {F}ast {A}cceleration of {S}ymbolic
                 {T}ransition systems},
  BOOKTITLE = {Proc.\ 15th Int.\ Conf.\ Computer Aided Verification
		  (CAV 2003)},
  VOLUME = {2725},
  MONTH = JUL,
  PAGES = {118--121},
  SERIES = {Lecture Notes in Computer Science},
  YEAR = {2003},
  PUBLISHER = {Springer},
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FAST-cav03.ps}
}

@ARTICLE{FPS-ICOMP,
  AUTHOR = {A. Finkel and S. {Purushothaman Iyer} and G. Sutre},
  TITLE = {Well-Abstracted Transition Systems: Application to
                 {FIFO} Automata},
  MONTH = FEB,
  JOURNAL = {Information and Computation},
  VOLUME = {181},
  NUMBER = {1},
  PAGES = {1--31},
  YEAR = {2003},
  PS = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/FPS-ICOMP.ps},
  WWWPUBLIC = {public ccsb}
}

@MISC{THESE-LEROUX-2003,
  AUTHOR = {J. Leroux},
  TITLE = {Algorithmique de la v{\'e}rification des syst{\`e}mes {\`a}
                 compteurs. {A}pproximation et acc{\'e}l{\'e}ration.
                 {I}mpl{\'e}mentation de l'outil {FAST}},
  YEAR = {2003},
  MONTH = DEC,
  HOWPUBLISHED = {Th{\`e}se ENS de Cachan},
  PS = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/Leroux-these.ps}
}

@INPROCEEDINGS{BDF-afadl2004,
  AUTHOR = {S. Bardin and {\relax Ch}. Darlot and A. Finkel},
  TITLE = {{FAST}~: un model-checker pour syst{\`e}mes {\`a}
                 compteurs},
  EDITOR = {J. Julliand},
  BOOKTITLE = {Actes du 6\`eme atelier Approches Formelles dans
                  l'Assistance au Développement de Logiciels (AFADL 2004),
                  Besan\c{c}on, France},
  PAGES = {377--380},
  YEAR = {2004},
  MONTH = JUN,
  PS = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/BDF-afadl04.ps}
}

@INPROCEEDINGS{BFL-tacas04,
  AUTHOR = {S. Bardin and A. Finkel and J. Leroux},
  TITLE = {{FAST}er acceleration of counter automata in
                 practice},
  BOOKTITLE = {Proc.\ 10th Int.\ Conf.\ Tools and Algorithms for the
		  Construction and Analysis of Systems (TACAS 2004)},
  VOLUME = {2988},
  MONTH = APR,
  PAGES = {576--590},
  SERIES = {Lecture Notes in Computer Science},
  YEAR = {2004},
  PUBLISHER = {Springer},
  PS = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/BFL-tacas04.ps}
}

@INPROCEEDINGS{BP-pnml2004,
  AUTHOR = {S. Bardin and L. Petrucci},
  TITLE = {From {PNML} to counter systems for accelerating
                 {P}etri {N}ets with {FAST}},
  EDITOR = {Kindler, Ekkart},
  MONTH = JUN,
  PAGES = {26-40},
  BOOKTITLE = {Proc.\ Workshop on Interchange Format for Petri Nets,
                 Bologna, Italy},
  YEAR = {2004},
  PS = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/BP-pnml04.ps}
}

@INPROCEEDINGS{FL-cav04,
  AUTHOR = {A. Finkel and J. Leroux},
  TITLE = {Image computation in infinite state model checking},
  BOOKTITLE = {Proc.\ 16th Int.\ Conf.\ Computer Aided Verification
		  (CAV 2004)},
  VOLUME = 3114,
  MONTH = JUL,
  SERIES = {Lecture Notes in Computer Science},
  YEAR = {2004},
  PUBLISHER = {Springer},
  PAGES = {361-371},
  PS = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/FL-cav04.ps}
}

@INPROCEEDINGS{FL-spin04,
  AUTHOR = {A. Finkel and J. Leroux},
  TITLE = {Polynomial Time Image Computation With
                 Interval-definable Counters Systems},
  BOOKTITLE = {Proc.\ 11th Int.\ {SPIN} Workshop on Model Checking Software},
  MONTH = APR,
  VOLUME = {2989},
  PAGES = {182--197},
  SERIES = {Lecture Notes in Computer Science},
  YEAR = {2004},
  PUBLISHER = {Springer},
  PS = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/FL-spin04.ps}
}

@INPROCEEDINGS{Ler-inf03,
  PAGES = {89-104},
  VOLUME = {98},
  NMONTH = {8},
  AUTHOR = {J. Leroux},
  TITLE = {The affine hull of a binary automaton is computable in
                 polynomial time},
  BOOKTITLE = {Proc.\ 5th Int.\ Workshop on Verification of Infinite
		  State Systems (INFINITY 2003)},
  SERIES = {Electronic Notes in Theor.\ Comp.\ Sci.},
  MONTH = AUG,
  YEAR = {2004},
  PUBLISHER = {Elsevier Science},
  PS = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/Ler-inf03.ps}
}

@ARTICLE{BH99,
  AUTHOR = {A. Bouajjani and P. Habermehl},
  TITLE = {{Symbolic Reachability Analysis of Fifo-Channel Systems
with Nonregular Sets of Configurations}},
  JOURNAL = {Theoretical Computer Science},
  VOLUME = {221},
  MONTH = JUN,
  NUMBER = {1-2},
  PAGES = {211--250},
  YEAR = {1999},
  URL = {http://www.liafa.jussieu.fr/~abou/cqdd-tcs.ps.gz}
}

@INPROCEEDINGS{BM99,
  AUTHOR = {A. Bouajjani and R. Mayr},
  TITLE = {{Model Checking Lossy Vector Addition Systems}},
  BOOKTITLE = {Proc.\ 16th Ann.\ Symp.\ Theoretical Aspects of Computer
		  Science (STACS '99)},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {1563},
  MONTH = MAR,
  PAGES = {323-333},
  PUBLISHER = {Springer},
  YEAR = {1999},
  URL = {http://www.liafa.jussieu.fr/~abou/lvass-stacs99.ps.gz}
}

@INPROCEEDINGS{DT99,
  AUTHOR = {{\relax P.A.} Abdulla and A. Annichini and S. Bensalem and A. Bouajjani and
P. Habermehl, Y. Lakhnech},
  TITLE = {{Verification of Infinite-State Systems by Combining Abstraction and
Reachability Analysis}},
  BOOKTITLE = {Proc.\ 11th Int.\ Conf.\ Computer Aided Verification
		  (CAV '99), Trento, Italy, July 1999},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {1633},
  YEAR = 1999,
  URL = {http://www.liafa.jussieu.fr/~abou/abst+symb-cav99.ps.gz}
}

@INPROCEEDINGS{CJ99,
  AUTHOR = {H. Comon and Y. Jurski},
  TITLE = {{Timed Automata and the Theory of Real Numbers}},
  BOOKTITLE = {Proc.\ 10th Int.\ Conf.\ Concurrency Theory
		  (CONCUR '99), Eindhoven, The Netherlands, Aug.\ 1999},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {1664},
  YEAR = 1999,
  URL = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/ComJur-concur99.ps}
}

@INPROCEEDINGS{BJNT00,
  AUTHOR = {A. Bouajjani and B. Jonsson and M. Nilsson and T. Touili},
  TITLE = {Regular Model Checking},
  BOOKTITLE = {Proc.\ 12th Int.\ Conf.\ Computer Aided Verification
		  (CAV 2000)},
  SERIES = {Lecture Notes in Computer Science},
  NUMBER = {1855},
  MONTH = JUL,
  PAGES = {403-418},
  YEAR = {2000},
  URL = {http://www.liafa.jussieu.fr/~abou/rmc-cav00.ps.gz}
}

@INPROCEEDINGS{AAB00,
  AUTHOR = {A. Annichini and E. Asarin and A. Bouajjani},
  TITLE = {{Symbolic Techniques for Parametric Reasoning about Counter and
                Clock Systems}},
  BOOKTITLE = {Proc.\ 12th Int.\ Conf.\ Computer Aided Verification
		  (CAV 2000)},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {1855},
  PAGES = {419--434},
  MONTH = JUL,
  YEAR = 2000,
  URL = {http://www.liafa.jussieu.fr/~abou/pdbm-cav00.ps.gz}
}

@INPROCEEDINGS{Bou01,
  AUTHOR = {A. Bouajjani},
  TITLE = {{Languages, Rewriting systems, and Verification of Infinte-State Systems}},
  NOTE = {invited paper},
  BOOKTITLE = {Proc.\ 28th Int.\ Coll.\ Automata, Languages, and
		  Programming (ICALP 2001)},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {2076},
  PUBLISHER = {Springer},
  MONTH = JUL,
  YEAR = 2001,
  URL = {http://www.liafa.jussieu.fr/~abou/rew-icalp01.ps.gz}
}

@INPROCEEDINGS{ABB01,
  AUTHOR = {{\relax P.A.} Abdulla and L. Boasson and A. Bouajjani},
  TITLE = {Effective Lossy Queue Languages},
  BOOKTITLE = {Proc.\ 28th Int.\ Coll.\ Automata, Languages, and
		  Programming (ICALP 2001)},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {2076},
  PAGES = {639--651},
  MONTH = JUL,
  YEAR = 2001,
  URL = {http://www.liafa.jussieu.fr/~abou/cflcs-icalp01.ps.gz}
}

@INPROCEEDINGS{Tou01,
  AUTHOR = {Touili, T.},
  TITLE = {Regular Model-Checking using Widening Techniques},
  BOOKTITLE = {Proc.\ Workshop on Verification of Parametrized Systems
                   (VEPAS'01)},
  SERIES = {Electronic Notes in Theor.\ Comp.\ Sci.},
  PUBLISHER = {Elsevier Science},
  VOLUME = 50,
  NUMBER = 4,
  MONTH = AUG,
  PAGES = {342-356},
  YEAR = 2001
}

@INPROCEEDINGS{ABLS01,
  AUTHOR = {A Annichini and A. Bouajjani and Y. Lakhnech and
                M. Sighireanu},
  TITLE = {{Analysis of Fair Extended Automata}},
  BOOKTITLE = {Proc.\ 8th Int.\ Symp.\ Static Analysis (SAS 2001)},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {2126},
  PAGES = {335--355},
  MONTH = JUL,
  YEAR = 2001,
  URL = {http://www.liafa.jussieu.fr/~abou/fpea-sas01.ps.gz}
}

@INPROCEEDINGS{ABS01,
  AUTHOR = {A. Annichini and A. Bouajjani and M. Sighireanu},
  TITLE = {{TReX: A Tool for Reachability Analysis of Complex Systems}},
  BOOKTITLE = {Proc.\ 13th Int.\ Conf.\ Computer Aided Verification
		  (CAV 2001)},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  PAGES = {368--372},
  VOLUME = {2102},
  MONTH = JUL,
  YEAR = 2001,
  URL = {http://www.liafa.jussieu.fr/~abou/trex-cav01.ps.gz}
}

@INPROCEEDINGS{Collomb-Sighireanu-01,
  AUTHOR = {Collomb-Annichini, A.  and Sighireanu, M.},
  TITLE = {{Parameterized Reachability Analysis of the IEEE 1394 Root
                 Contention Protocol using TReX}},
  BOOKTITLE = {Proc.\ Workshop on Real-Time Tools (RTTOOLS'01), Aalborg,
                     August 2001},
  YEAR = {2001},
  EDITOR = {Pettersson, P. and Yovine, S.},
  ORGANIZATION = {Uppsala University},
  PUBLISHER = {Department of Information Technology},
  NOTE = {Appears as technical report 2001-014}
}

@INPROCEEDINGS{BM02,
  AUTHOR = {A. Bouajjani and A. Merceron},
  TITLE = {{Parametric Verification of a Group Membership Algorithm}},
  BOOKTITLE = {Proc.\ 7th Int.\ Symp.\ on Formal Techniques in Real-Time
                    and Fault Tolerant Systems (FTRTFT'02)},
  PUBLISHER = {Springer},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {2469},
  PAGES = {311--330},
  MONTH = SEP,
  YEAR = 2002,
  URL = {http://www.liafa.jussieu.fr/~abou/bm-ftrtft02.ps.gz}
}

@INPROCEEDINGS{BT02,
  AUTHOR = {A. Bouajjani and T. Touili},
  TITLE = {{Extrapolating Tree Transformations}},
  BOOKTITLE = {Proc.\ 14th Int.\ Conf.\ Computer Aided Verification
		  (CAV 2002)},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {2404},
  PUBLISHER = {Springer},
  PAGES = {539--554},
  MONTH = JUL,
  YEAR = 2002,
  URL = {http://www.liafa.jussieu.fr/~abou/bt-cav02.ps.gz}
}

@ARTICLE{BouaHaberMayr03,
  AUTHOR = {Bouajjani, A. and Habermehl, P. and Mayr, R.},
  TITLE = {{Automatic verification of recursive procedures with one integer
              parameter}},
  JOURNAL = {Theoretical Computer Science},
  YEAR = 2003,
  VOLUME = 295,
  NUMBER = {1--3},
  MONTH = FEB,
  PAGES = {85--106},
  URL = {http://www.liafa.jussieu.fr/~abou/bpaZ-complete.ps.gz}
}

@INPROCEEDINGS{BT03,
  AUTHOR = {A. Bouajjani and T. Touili},
  TITLE = {{Reachability Analysis of Process Rewrite Systems}},
  BOOKTITLE = {Proc.\ 23rd Conf.\ Found.\ of Software Technology and
		  Theor.\ Comp.\ Sci.\ (FST\&TCS 2003)},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {2914},
  PAGES = {74-87},
  MONTH = DEC,
  YEAR = 2003,
  URL = {http://www.liafa.jussieu.fr/~abou/fsttcs03.ps.gz}
}

@ARTICLE{BET03b,
  AUTHOR = {A. Bouajjani and J. Esparza and T. Touili},
  TITLE = {{A Generic Approach to the Static Analysis of Concurrent 
Programs with Procedures}},
  JOURNAL = {Int.\ J.\ of Foundations Computer Science},
  PUBLISHER = {World Scientific},
  YEAR = 2003,
  VOLUME = 14,
  NUMBER = 4,
  MONTH = AUG,
  PAGES = {551--582},
  URL = {http://www.liafa.jussieu.fr/~abou/cpda-journal.ps.gz}
}

@INPROCEEDINGS{Boyer-Sighireanu-03,
  AUTHOR = {Boyer, M. and Sighireanu, M.},
  TITLE = {{Synthesis and Verification of Constraints in the PGM protocol}},
  BOOKTITLE = {Proc.\ 12th Int.\ Symposium of Formal Methods Europe
		   (FME '03)},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {2805},
  PAGES = {264-281},
  PUBLISHER = {Springer},
  MONTH = SEP,
  YEAR = 2003
}

@ARTICLE{ACBJ04,
  AUTHOR = {P. A. Abdulla and A. Collomb-Annichini and A. Bouajjani and B. Jonsson},
  TITLE = {{Using Forward Reachability Analysis for Verification of Lossy Channel Systems}},
  JOURNAL = {Formal Methods in System Design},
  PUBLISHER = {Kluwer Academic},
  VOLUME = 25,
  NUMBER = 1,
  MONTH = JUL,
  PAGES = {39--65},
  YEAR = 2004,
  URL = {http://www.liafa.jussieu.fr/~abou/sre-fmsd04.ps.gz}
}

@INPROCEEDINGS{BHV04,
  AUTHOR = {A. Bouajjani and P. Habermehl and T. Vojnar},
  TITLE = {{Abstract Regular Model Checking}},
  BOOKTITLE = {Proc.\ 16th Int.\ Conf.\ Computer Aided Verification
		  (CAV 2004)},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = 3114,
  PAGES = {372-386},
  MONTH = JUL,
  YEAR = 2004,
  URL = {http://www.liafa.jussieu.fr/~abou/cav04-armc.ps.gz}
}

@INPROCEEDINGS{HV04,
  AUTHOR = {P. Habermehl and T. Vojnar},
  TITLE = {{Regular Model Checking Using Inference of Regular Languages}},
  BOOKTITLE = {Proc.\ 6th Int.\ Workshop on Verification of Infinite
		  State Systems (INFINITY 2004)},
  URL = {http://www.liafa.jussieu.fr/~haberm/Publications/infinity04inf.ps.gz},
  SERIES = {Electronic Notes in Theor.\ Comp.\ Sci.},
  MONTH = DEC,
  PUBLISHER = {Elsevier Science},
  VOLUME = {138(3)},
  PAGES = {21--36},
  YEAR = 2005
}

@INPROCEEDINGS{BLW04,
  AUTHOR = {A. Bouajjani and A. Legay and P. Wolper},
  TITLE = {{Handling Liveness Properties in 
              ($\omega$-)Regular Model Checking}},
  BOOKTITLE = {Proc.\ 6th Int.\ Workshop on Verification of Infinite
		  State Systems (INFINITY 2004)},
  SERIES = {Electronic Notes in Theor.\ Comp.\ Sci.},
  MONTH = DEC,
  PUBLISHER = {Elsevier Science},
  VOLUME = {138(3)},
  PAGES = {101--115},
  YEAR = 2005,
  URL = {http://www.liafa.jussieu.fr/~abou/rmc-live-infinity04.pdf.gz}
}

@INPROCEEDINGS{BET04,
  AUTHOR = {A. Bouajjani and J. Esparza and T. Touili},
  TITLE = {{Reachability Analysis of Synchronized PA Systems}},
  BOOKTITLE = {Proc.\ 6th Int.\ Workshop on Verification of Infinite
		  State Systems (INFINITY 2004)},
  SERIES = {Electronic Notes in Theor.\ Comp.\ Sci.},
  MONTH = DEC,
  PUBLISHER = {Elsevier Science},
  VOLUME = {138(3)},
  YEAR = 2005,
  PAGES = {153--178},
  URL = {http://www.liafa.jussieu.fr/~abou/spa-infinity04.ps.gz}
}

@INPROCEEDINGS{BM04,
  AUTHOR = {A. Bouajjani and A. Meyer},
  TITLE = {{Symbolic Reachability Analysis of Higher-Order Context-Free Processes}},
  BOOKTITLE = {Proc.\ 24th Conf.\ Found.\ of Software Technology and
                  Theor.\ Comp.\ Sci.\ (FST\&TCS 2004)},
  SERIES = {Lecture Notes in Computer Science},
  PUBLISHER = {Springer},
  VOLUME = 3328,
  PAGES = {135--147},
  MONTH = DEC,
  YEAR = 2004,
  URL = {http://www.liafa.jussieu.fr/~abou/hcfp-fsttcs04.ps.gz}
}

@INPROCEEDINGS{BHJ:CAV03,
  AUTHOR = {Boigelot,B. and Herbreteau,F. and Jodogne,S.},
  TITLE = {Hybrid Acceleration Using Real Vector Automata},
  BOOKTITLE = {Proc.\ 15th Int.\ Conf.\ Computer Aided Verification
		  (CAV 2003)},
  SERIES = {Lecture Notes in Computer Science},
  VOLUME = {2725},
  PAGES = {193--205},
  PUBLISHER = {Springer},
  MONTH = JUL,
  YEAR = {2003},
  URL = {http://www.labri.fr/Perso/~herbrete/publications/cav03/BHJ-cav03.ps.gz}
}


This file has been generated by bibtex2html 1.75

Valid HTML 4.01! Valid CSS!