@inproceedings{DBLP:conf/atva/JensenSSSVD21,
  author       = {Peter Gj{\o}l Jensen and
                  Stefan Schmid and
                  Morten Konggaard Schou and
                  Jir{\'{\i}} Srba and
                  Juan Vanerio and
                  Ingo van Duijn},
  editor       = {Zhe Hou and
                  Vijay Ganesh},
  title        = {Faster Pushdown Reachability Analysis with Applications in Network
                  Verification},
  booktitle    = {Automated Technology for Verification and Analysis - 19th International
                  Symposium, {ATVA} 2021, Gold Coast, QLD, Australia, October 18-22,
                  2021, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {12971},
  pages        = {170--186},
  publisher    = {Springer},
  year         = {2021},
  url          = {https://doi.org/10.1007/978-3-030-88885-5\_12},
  doi          = {10.1007/978-3-030-88885-5\_12},
  timestamp    = {Tue, 21 Mar 2023 20:59:41 +0100},
  biburl       = {https://dblp.org/rec/conf/atva/JensenSSSVD21.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@phdthesis{schwoon2002model,
  author    = {Stefan Schwoon},
title     = {Model checking pushdown systems},
school    = {Technical University Munich, Germany},
year      = {2002},
note       = {\url{https://d-nb.info/96638976X/34}},
}

@inproceedings{DBLP:conf/fmcad/SchlichtkrullSST22,
  author       = {Anders Schlichtkrull and
                  Morten Konggaard Schou and
                  Jir{\'{\i}} Srba and
                  Dmitriy Traytel},
  editor       = {Alberto Griggio and
                  Neha Rungta},
  title        = {Differential Testing of Pushdown Reachability with a Formally Verified
                  Oracle},
  booktitle    = {22nd Formal Methods in Computer-Aided Design, {FMCAD} 2022, Trento,
                  Italy, October 17-21, 2022},
  pages        = {369--379},
  publisher    = {{IEEE}},
  year         = {2022},
  url          = {https://doi.org/10.34727/2022/isbn.978-3-85448-053-2\_44},
  doi          = {10.34727/2022/isbn.978-3-85448-053-2\_44},
  timestamp    = {Tue, 21 Mar 2023 21:02:10 +0100},
  biburl       = {https://dblp.org/rec/conf/fmcad/SchlichtkrullSST22.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

@article{buchi1964regular,
  title={Regular canonical systems},
  author={B{\"u}chi, J Richard},
  journal={Archiv f{\"u}r mathematische Logik und Grundlagenforschung},
  volume={6},
  number={3-4},
  pages={91--111},
  year={1964},
  publisher={Springer},
  doi={https://doi.org/10.1007/BF01969548}
}

@inproceedings{esparza1999automata,
  author    = {Javier Esparza and
Jens Knoop},
editor    = {Wolfgang Thomas},
title     = {An Automata-Theoretic Approach to Interprocedural Data-Flow Analysis},
booktitle = {FoSSaCS 1999},
series    = {LNCS},
volume    = {1578},
pages     = {14--30},
publisher = {Springer},
year      = {1999},
doi       = {10.1007/3-540-49019-1\_2},
}

@inproceedings{conway2005incremental,
  author    = {Christopher L. Conway and
Kedar S. Namjoshi and
Dennis Dams and
Stephen A. Edwards},
editor    = {Kousha Etessami and
Sriram K. Rajamani},
title     = {Incremental Algorithms for Inter-procedural Analysis of Safety Properties},
booktitle = {{CAV} 2005},
series    = {LNCS},
volume    = {3576},
pages     = {449--461},
publisher = {Springer},
year      = {2005},
doi       = {10.1007/11513988\_45},
}

@inproceedings{esparza2001bdd,
  author    = {Javier Esparza and
Stefan Schwoon},
editor    = {G{\'{e}}rard Berry and
Hubert Comon and
Alain Finkel},
title     = {A BDD-Based Model Checker for Recursive Programs},
booktitle = {CAV 2001},
series    = {LNCS},
volume    = {2102},
pages     = {324--336},
publisher = {Springer},
year      = {2001},
doi       = {10.1007/3-540-44585-4\_30},
}

@inproceedings{moped,
  title={Moped},
  author={Stefan Schwoon},
  note={\url{http://www2.informatik.uni-stuttgart.de/fmi/szs/tools/moped/}},
  year={2002},
}

@inproceedings{jmoped,
author    = {Dejvuth Suwimonteerabuth and
Stefan Schwoon and
Javier Esparza},
editor    = {Nicolas Halbwachs and
Lenore D. Zuck},
title     = {{jMoped}: {A} {J}ava Bytecode Checker Based on {Moped}},
booktitle = {{TACAS} 2005},
series    = {LNCS},
volume    = {3440},
pages     = {541--545},
publisher = {Springer},
year      = {2005},
doi       = {10.1007/978-3-540-31980-1\_35},
}

@inproceedings{bouajjani1997reachability,
  author    = {Ahmed Bouajjani and
Javier Esparza and
Oded Maler},
editor    = {Antoni W. Mazurkiewicz and
J{\'{o}}zef Winkowski},
title     = {Reachability Analysis of Pushdown Automata: Application to Model-Checking},
booktitle = {{CONCUR} 1997},
series    = {LNCS},
volume    = {1243},
pages     = {135--150},
publisher = {Springer},
year      = {1997},
doi       = {10.1007/3-540-63141-0\_10},
}

@inproceedings{JKMSST:coNEXT:18,
  author    = {Jesper Stenbjerg Jensen and
Troels Beck Kr{\o}gh and
Jonas Sand Madsen and
Stefan Schmid and
Jir{\'{\i}} Srba and
Marc Tom Thorgersen},
editor    = {Xenofontas A. Dimitropoulos and
Alberto Dainotti and
Laurent Vanbever and
Theophilus Benson},
title     = {P-{Rex}: fast verification of {MPLS} networks with multiple link failures},
booktitle = {CoNEXT 2018},
pages     = {217--227},
publisher = {{ACM}},
year      = {2018},
doi       = {10.1145/3281411.3281432},
}

@inproceedings{jensen2020aalwines,
  author    = {Peter Gj{\o}l Jensen and
Dan Kristiansen and
Stefan Schmid and
Morten Konggaard Schou and
Bernhard Clemens Schrenk and
Jir{\'{\i}} Srba},
editor    = {Dongsu Han and
Anja Feldmann},
title     = {{AalWiNes}: a fast and quantitative what-if analysis tool for {MPLS}
networks},
booktitle = {CoNEXT 2020},
pages     = {474--481},
publisher = {{ACM}},
year      = {2020},
doi       = {10.1145/3386367.3431308},
}

@article{DJJKMSST:TON:21,
author ={I. van Duijn and P.G. Jensen and J.S. Jensen and T.B. Kr{\o}gh and J.S. Madsen and S. Schmid and J. Srba and M.T. Thorgersen},
title ={Automata-Theoretic Approach to Verification of {MPLS} Networks under Link Failures},
journal ={IEEE/ACM Transactions on Networking},
year ={2021},
volume ={},
number ={},
publisher ={IEEE},
pages ={1--16},
pdf ={http://www.cs.aau.dk/~srba/files/DJJKMSST:TON:21.pdf},
ee ={https://ieeexplore.ieee.org/document/9619760},
doi ={10.1109/TNET.2021.3126572},
}

@misc{Lammich-DPN,
  author={Peter Lammich},
  title={Formalization of Dynamic Pushdown Networks in {I}sabelle/{HOL}},
  year={2009},
  note={\url{https://www21.in.tum.de/~lammich/isabelle/dpn-document.pdf}}
}

@inproceedings{DBLP:conf/cav/LammichMW09,
    author    = {Peter Lammich and
    Markus M{\"{u}}ller{-}Olm and
    Alexander Wenner},
    editor    = {Ahmed Bouajjani and
    Oded Maler},
    title     = {Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints},
    booktitle = {{CAV} 2009},
    series    = {LNCS},
    volume    = {5643},
    pages     = {525--539},
    publisher = {Springer},
    year      = {2009},
    doi       = {10.1007/978-3-642-02658-4\_39}
}

