@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