@inproceedings(DBLP:conf/atva/AbdullaACJ09,
 author       = {Parosh Aziz Abdulla and Muhsin Atto and Jonathan Cederberg and Ran Ji},
 year         = {2009},
 title        = {Automated Analysis of Data-Dependent Programs with Dynamic Memory},
 editor       = {Zhiming Liu and Anders P. Ravn},
 booktitle    = {Automated Technology for Verification and Analysis, 7th International Symposium, {ATVA} 2009, Macao, China, October 14-16, 2009. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {5799},
 publisher    = {Springer},
 pages        = {197--212},
 url          = {https://doi.org/10.1007/978-3-642-04761-9\_16},
)
@article(DBLP:journals/iandc/AbdullaCJT00,
 author       = {Parosh Aziz Abdulla and Karlis Cerans and Bengt Jonsson and Yih{-}Kuen Tsay},
 year         = {2000},
 title        = {Algorithmic Analysis of Programs with Well Quasi-ordered Domains},
 journal      = {Inf. Comput.},
 volume       = {160},
 number       = {1-2},
 pages        = {109--127},
 doi          = {10.1006/inco.1999.2843},
)
@article(DBLP:journals/ijfcs/AbdullaDHR09,
 author       = {Parosh Aziz Abdulla and Giorgio Delzanno and Noomene Ben Henda and Ahmed Rezine},
 year         = {2009},
 title        = {Monotonic Abstraction: on Efficient Verification of Parameterized Systems},
 journal      = {Int. J. Found. Comput. Sci.},
 volume       = {20},
 number       = {5},
 pages        = {779--801},
 url          = {https://doi.org/10.1142/S0129054109006887},
)
@inproceedings(BFLS-avis06,
 author       = {S{\'e}bastien Bardin and Alain Finkel and {\'E}tienne Lozes and Arnaud Sangnier},
 year         = {2006},
 title        = {From Pointer Systems to Counter Systems Using Shape Analysis},
 editor       = {Ramesh Bharadwaj},
 booktitle    = {{P}roceedings of the 5th {I}nternational {W}orkshop on {A}utomated {V}erification of {I}nfinite-{S}tate {S}ystems ({AVIS}'06)},
 address      = {Vienna, Austria},
 url          = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/BFLS-AVIS-06.pdf},
)
@inproceedings(BFG-fsttcs17,
 author       = {Michael Blondin and Alain Finkel and Goubault{-}Larrecq, Jean},
 year         = {2017},
 title        = {Forward Analysis for {WSTS}, {Part III}: {Karp-Miller} Trees},
 editor       = {Satya Lokam and R. Ramanujam},
 booktitle    = {{P}roceedings of the 37th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'17)},
 series       = {Leibniz International Proceedings in Informatics},
 volume       = {93},
 publisher    = {Leibniz-Zentrum f{\"u}r Informatik},
 address      = {Kanpur, India},
 pages        = {16:1--16:15},
 doi          = {10.4230/LIPIcs.FSTTCS.2017.16},
 url          = {https://hal.archives-ouvertes.fr/hal-01736704/},
)
@article(DBLP:journals/jacm/BrandZ83,
 author       = {Daniel Brand and Pitro Zafiropulo},
 year         = {1983},
 title        = {On Communicating Finite-State Machines},
 journal      = {J. {ACM}},
 volume       = {30},
 number       = {2},
 pages        = {323--342},
 url          = {https://doi.org/10.1145/322374.322380},
)
@inproceedings(DBLP:conf/popl/CousotC77,
 author       = {Patrick Cousot and Radhia Cousot},
 year         = {1977},
 title        = {Abstract Interpretation: {A} Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints},
 editor       = {Robert M. Graham and Michael A. Harrison and Ravi Sethi},
 booktitle    = {Conference Record of the Fourth {ACM} Symposium on Principles of Programming Languages, Los Angeles, California, USA, January 1977},
 publisher    = {{ACM}},
 pages        = {238--252},
 url          = {https://doi.org/10.1145/512950.512973},
)
@inproceedings(DBLP:conf/rp/DelzannoS14,
 author       = {Giorgio Delzanno and Jan St{\"{u}}ckrath},
 year         = {2014},
 title        = {Parameterized Verification of Graph Transformation Systems with Whole Neighbourhood Operations},
 editor       = {Jo{\"{e}}l Ouaknine and Igor Potapov and James Worrell},
 booktitle    = {Reachability Problems - 8th International Workshop, {RP} 2014, Oxford, UK, September 22-24, 2014. Proceedings},
 series       = {Lecture Notes in Computer Science},
 volume       = {8762},
 publisher    = {Springer},
 pages        = {72--84},
 url          = {https://doi.org/10.1007/978-3-319-11439-2\_6},
)
@article(DBLP:journals/corr/abs-1911-05430,
 author       = {Emanuele D'Osualdo and Felix Stutz},
 year         = {2019},
 title        = {Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions},
 journal      = {CoRR},
 volume       = {abs/1911.05430},
 url          = {http://arxiv.org/abs/1911.05430},
)
@inproceedings(F-icalp87,
 author       = {Alain Finkel},
 year         = {1987},
 title        = {A generalization of the procedure of {K}arp and {M}iller to well structured transition system},
 editor       = {Thomas Ottmann},
 booktitle    = {{P}roceedings of the 14th {I}nternational {C}olloquium on {A}utomata, {L}anguages and {P}rogramming ({ICALP}'87)},
 series       = {Lecture Notes in Computer Science},
 volume       = {267},
 publisher    = {Springer-Verlag},
 address      = {Karlsruhe, Germany},
 pages        = {499--508},
 doi          = {10.1007/3-540-18088-5\_43},
 url          = {http://www.lsv.fr/Publis/PAPERS/PDF/F-icalp87.pdf},
)
@inproceedings(DBLP:conf/stacs/FinkelG09,
 author       = {Alain Finkel and Goubault{-}Larrecq, Jean},
 year         = {2009},
 title        = {Forward Analysis for WSTS, Part {I:} Completions},
 editor       = {Susanne Albers and Jean{-}Yves Marion},
 booktitle    = {26th International Symposium on Theoretical Aspects of Computer Science, {STACS} 2009, February 26-28, 2009, Freiburg, Germany, Proceedings},
 series       = {LIPIcs},
 volume       = {3},
 publisher    = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany},
 pages        = {433--444},
 url          = {https://doi.org/10.4230/LIPIcs.STACS.2009.1844},
)
@inproceedings(finkel98,
 author       = {Alain Finkel and {\relax Ph}ilippe Schnoebelen},
 year         = {1998},
 title        = {Fundamental Structures in Well-Structured Infinite Transition Systems},
 editor       = {Claudio L. Lucchesi and Arnaldo V. Moura},
 booktitle    = {{P}roceedings of the 3rd {L}atin {A}merican {S}ymposium on {T}heoretical {I}nformatics ({LATIN}'98)},
 series       = {Lecture Notes in Computer Science},
 volume       = {1380},
 publisher    = {Springer},
 address      = {Campinas, Brasil},
 pages        = {102--118},
 doi          = {10.1007/BFb0054314},
 url          = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PS/FinSch-latin98.ps},
)
@article(finkel98b,
 author       = {Alain Finkel and {\relax Ph}ilippe Schnoebelen},
 year         = {2001},
 title        = {Well-Structured Transition Systems Everywhere!},
 journal      = {Theoretical Computer Science},
 volume       = {256},
 number       = {1-2},
 pages        = {63--92},
 doi          = {10.1016/S0304-3975(00)00102-X},
 url          = {http://www.lsv.ens-cachan.fr/Publis/PAPERS/PDF/FinSch-TCS99.pdf},
)
@inproceedings(GF-fsttcs19,
 author       = {Ekanshdeep Gupta and Alain Finkel},
 year         = {2019},
 title        = {The well structured problem for Presburger counter machines},
 editor       = {Arkadev Chattopadhyay and Paul Gastin},
 booktitle    = {{P}roceedings of the 39th {C}onference on {F}oundations of {S}oftware {T}echnology and {T}heoretical {C}omputer {S}cience ({FSTTCS}'19)},
 series       = {Leibniz International Proceedings in Informatics},
 publisher    = {Leibniz-Zentrum f{\"u}r Informatik},
 address      = {Bombay, India},
 pages        = {41:1--41:15},
 doi          = {10.4230/LIPIcs.FSTTCS.2019.41},
 url          = {https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=11603},
)
@article(DBLP:journals/tcs/VauquelinF80,
 author       = {Bernard Vauquelin and Franchi{-}Zannettacci, Paul},
 year         = {1980},
 title        = {Automates a File},
 journal      = {Theor. Comput. Sci.},
 volume       = {11},
 pages        = {221--225},
 url          = {https://doi.org/10.1016/0304-3975(80)90047-X},
)