@inproceedings(AADP13,
 author       = {P.~A. Abdulla and M.~Faouzi Atig and G.~Delzanno and A.~Podelski},
 year         = {2013},
 title        = {Push-Down Automata with Gap-Order Constraints},
 booktitle    = {{FSEN} 2013},
 pages        = {199--216},
 doi          = {10.1007/978-3-642-40213-5\_13},
)
@inproceedings(ACJT96,
 author       = {P.~A. Abdulla and K.~Cerans and B.~Jonsson and Y.-K. Tsay},
 year         = {1996},
 title        = {General Decidability Theorems for Infinite-State Systems},
 booktitle    = {LICS'96},
 pages        = {313--321},
 doi          = {10.1109/LICS.1996.561359},
)
@article(ADV11,
 author       = {P.~A. Abdulla and G.~Delzanno and L.~Van Begin},
 year         = {2011},
 title        = {A classification of the expressive power of well-structured transition systems},
 journal      = {Inf. Comput.},
 volume       = {209},
 number       = {3},
 pages        = {248--279},
 doi          = {10.1016/j.ic.2010.11.003},
)
@article(AJ01,
 author       = {P.~A. Abdulla and B.~Jonsson},
 year         = {2001},
 title        = {Ensuring completeness of symbolic verification methods for infinite-state systems},
 journal      = {Theor. Comput. Sci.},
 volume       = {256},
 number       = {1-2},
 pages        = {145--167},
 doi          = {10.1016/S0304-3975(00)00105-5},
)
@inproceedings(AN00,
 author       = {P.~A. Abdulla and A.~Nyl{\'e}n},
 year         = {2000},
 title        = {Better is Better than Well: On Efficient Verification of Infinite-State Systems},
 booktitle    = {LICS'00},
 publisher    = {IEEE Computer Society},
 pages        = {132--140},
 doi          = {10.1109/LICS.2000.855762},
)
@article(BDFZ09,
 author       = {M.~Bartoletti and P.~Degano and G.~L. Ferrari and R.~Zunino},
 year         = {2009},
 title        = {Local policies for resource usage analysis},
 journal      = {{ACM} TOPLAS},
 volume       = {31},
 number       = {6},
 doi          = {10.1145/1552309.1552313},
)
@misc(BozPhD,
 author       = {M.~Bozzano},
 title        = {{A Logic-Based Approach to Model Checking of Parameterized and Infinite-State Systems}, {PhD Thesis}, {DISI}, {University of Genova}, {June 2002}},
)
@inproceedings(CO13,
 author       = {X.~Cai and M.~Ogawa},
 year         = {2013},
 title        = {Well-Structured Pushdown Systems},
 booktitle    = {CONCUR 2013},
 pages        = {121--136},
 doi          = {10.1007/978-3-642-40184-8\_10},
)
@inproceedings(CO14,
 author       = {X.~Cai and M.~Ogawa},
 year         = {2014},
 title        = {Well-Structured Pushdown System: Case of Dense Timed Pushdown Automata},
 booktitle    = {FLOPS 2014},
 pages        = {336--352},
 doi          = {10.1007/978-3-319-07151-0\_21},
)
@article(ChadhaV09,
 author       = {R.~Chadha and M.~Viswanathan},
 year         = {2009},
 title        = {Deciding branching time properties for asynchronous programs},
 journal      = {Theor. Comput. Sci.},
 volume       = {410},
 number       = {42},
 pages        = {4169--4179},
 doi          = {10.1016/j.tcs.2009.01.021},
)
@article(DelzannoMSR,
 author       = {G.~Delzanno},
 year         = {2007},
 title        = {Constraint-based automatic verification of abstract models of multithreaded programs},
 journal      = {{TPLP}},
 volume       = {7},
 number       = {1-2},
 pages        = {67--91},
 doi          = {10.1017/S1471068406002821},
)
@inproceedings(Delzanno15,
 author       = {G.~Delzanno},
 year         = {2015},
 title        = {Data Tracking in Parameterized Verification},
 booktitle    = {TGC 2015},
)
@article(DR13,
 author       = {G.~Delzanno and F.~Rosa{-}Velardo},
 year         = {2013},
 title        = {On the coverability and reachability languages of monotonic extensions of {P}etri {N}ets},
 journal      = {Theor. Comput. Sci.},
 volume       = {467},
 pages        = {12--29},
 doi          = {10.1016/j.tcs.2012.09.021},
)
@article(FS01,
 author       = {A.~Finkel and Ph. Schnoebelen},
 year         = {2001},
 title        = {Well-structured transition systems everywhere!},
 journal      = {Theor. Comput. Sci.},
 volume       = {256},
 number       = {1-2},
 pages        = {63--92},
 doi          = {10.1016/S0304-3975(00)00102-X},
)
@inproceedings(LNORW08,
 author       = {R.~Lazic and T.~C. Newcomb and J.~Ouaknine and A.~W. Roscoe and J.~Worrell},
 year         = {2007},
 title        = {Nets with Tokens Which Carry Data},
 booktitle    = {ICATPN 2007},
 pages        = {301--320},
 doi          = {10.1007/978-3-540-73094-1\_19},
)
@inproceedings(MMW13,
 author       = {R.~Majumdar and R.~Meyer and Z.~Wang},
 year         = {2013},
 title        = {Provenance Verification},
 booktitle    = {RP '13},
 pages        = {21--22},
 doi          = {10.1007/978-3-642-41036-9\_3},
)
@inproceedings(Velardo,
 author       = {F.~Rosa{-}Velardo and D.~de~Frutos{-}Escrig},
 year         = {2009},
 title        = {Decidability Results for Restricted Models of Petri Nets with Name Creation and Replication},
 booktitle    = {Petri Nets},
 pages        = {63--82},
 doi          = {10.1007/978-3-642-02424-5\_6},
)
@inproceedings(T11,
 author       = {N.~Tzevelekos},
 year         = {2011},
 title        = {Fresh-register automata},
 booktitle    = {POPL 2011},
 pages        = {295--306},
 doi          = {10.1145/1926385.1926420},
)
@inproceedings(TG13,
 author       = {N.~Tzevelekos and R.~Grigore},
 year         = {2013},
 title        = {History-Register Automata},
 booktitle    = {FOSSACS 2013},
 pages        = {17--33},
 doi          = {10.1007/978-3-642-37075-5\_2},
)