Bibliography

[1]

Michele Chiari, Dino Mandrioli, and Matteo Pradella. Model-checking structured context-free languages. In CAV '21, volume 12760 of LNCS, 387–410. Springer, 2021. doi:10.1007/978-3-030-81688-9_18.

[2]

Michele Chiari, Dino Mandrioli, and Matteo Pradella. A first-order complete temporal logic for structured context-free languages. Log. Methods Comput. Sci., 2022. doi:10.46298/LMCS-18(3:11)2022.

[3]

D. Mandrioli and M. Pradella. Generalizing input-driven languages: theoretical and practical benefits. Computer Science Review, 27:61–87, 2018. doi:10.1016/j.cosrev.2017.12.001.

[4]

R. Alur, K. Etessami, and P. Madhusudan. A temporal logic of nested calls and returns. In TACAS 2004, 467–481. Springer, 2004. doi:10.1007/978-3-540-24730-2_35.

[5]

R. Alur, M. Arenas, P. Barceló, K. Etessami, N. Immerman, and L. Libkin. First-order and temporal logics for nested words. LMCS, 2008. doi:10.2168/LMCS-4(4:11)2008.

[6]

R. Alur and P. Madhusudan. Adding nesting structure to words. JACM, 2009. doi:10.1145/1516512.1516518.

[7]

Michele Chiari, Luca Geatti, Nicola Gigante, and Matteo Pradella. Smt-based symbolic model-checking for operator precedence languages. In CAV '24, volume 14681 of LNCS, 387–408. Springer, 2024. doi:10.1007/978-3-031-65627-9_19.

[8]

Francesco Pontiggia, Ezio Bartocci, and Michele Chiari. Model checking probabilistic operator precedence automata. CoRR, 2024. URL: https://doi.org/10.48550/arXiv.2404.03515.

[9]

Kousha Etessami and Mihalis Yannakakis. Recursive markov chains, stochastic grammars, and monotone systems of nonlinear equations. J. ACM, 56(1):1:1–1:66, 2009. URL: https://doi.org/10.1145/1462153.1462154, doi:10.1145/1462153.1462154.

[10]

Microsoft Research. Z3. URL: https://github.com/Z3Prover/z3.

[11]

Tobias Winkler and Joost-Pieter Katoen. Certificates for probabilistic pushdown automata via optimistic value iteration. In TACAS'23, volume 13994 of LNCS, 391–409. Springer, 2023. doi:10.1007/978-3-031-30820-8_24.

[12]

Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. MIT Press, 2008. ISBN 978-0-262-02649-9. URL: https://mitpress.mit.edu/9780262026499/principles-of-model-checking/.

[13]

T. Jensen, D. Le Metayer, and T. Thorn. Verification of control flow based security properties. In Proc. '99 IEEE Symp. on Security and Privacy, 89–103. 1999. doi:10.1109/SECPRI.1999.766902.

[14]

Herb Sutter. Exception-safe generic containers. C++ Report, 1997. URL: https://ptgmedia.pearsoncmg.com/imprint_downloads/informit/aw/meyerscddemo/DEMO/MAGAZINE/SU_FRAME.HTM.

[15]

D. Abrahams. Exception-Safety in Generic Components. In Generic Programming, 69–79. Springer, 2000. doi:10.1007/3-540-39953-4_6.

[16]

Francesco Pontiggia, Ezio Bartocci, and Michele Chiari. POPACheck: A model checker for probabilistic pushdown automata. In CAV (2) 2025, volume 15932 of LNCS, 105–121. Springer, 2025. doi:10.1007/978-3-031-98679-6\_5.

[17]

Dominik Wojtczak and Kousha Etessami. PReMo: an analyzer for probabilistic recursive models. In TACAS'07, volume 4424 of LNCS, 66–71. Springer, 2007. doi:10.1007/978-3-540-71209-1_7.

[18]

Dominik Wojtczak. Recursive probabilistic models: efficient analysis and implementation. PhD thesis, University of Edinburgh, UK, 2009. URL: https://hdl.handle.net/1842/3217.