@inproceedings{10.1007/978-3-030-99253-8_23,
    Abstract = {Probabilistic pushdown automata (pPDA) are a standard operational model for programming languages involving discrete random choices, procedures, and returns. Temporal properties are useful for gaining insight into the chronological order of events during program execution. Existing approaches in the literature have focused mostly on {\$}{\$}{\backslash}omega {\$}{\$}$\omega$-regular and LTL properties. In this paper, we study the model checking problem of pPDA against {\$}{\$}{\backslash}omega {\$}{\$}$\omega$-visibly pushdown languages that can be described by specification logics such as CaRet and are strictly more expressive than {\$}{\$}{\backslash}omega {\$}{\$}$\omega$-regular properties. With these logical formulae, it is possible to specify properties that explicitly take the structured computations arising from procedural programs into account. For example, CaRet is able to match procedure calls with their corresponding future returns, and thus allows to express fundamental program properties like total and partial correctness.},
    Address = {Cham},
    Author = {Winkler, Tobias and Gehnen, Christina and Katoen, Joost-Pieter},
    BookTitle = {Foundations of Software Science and Computation Structures},
    Editor = {Bouyer, Patricia and Schr{\"o}der, Lutz},
    File = {Model Checking Temporal Properties of Recursive Probabilistic Programs - 978-3-030-99253-8\_23 - a.pdf},
    ISBN = {978-3-030-99253-8},
    Pages = {449--469},
    Publisher = {Springer International Publishing},
    Title = {Model Checking Temporal Properties of Recursive Probabilistic Programs},
    Year = {2022},
    date-added = {2023-01-27 08:37:30 +0100},
    date-modified = {2023-01-27 08:37:30 +0100},
    doi = {10.1007/978-3-030-99253-8_23}
}

@inproceedings{10.1007/978-3-030-99253-8_23, Abstract = {Probabilistic pushdown automata (pPDA) are a standard operational model for programming languages involving discrete random choices, procedures, and returns. Temporal properties are useful for gaining insight into the chronological order of events during program execution. Existing approaches in the literature have focused mostly on {\$}{\$}{\backslash}omega {\$}{\$}$\omega$-regular and LTL properties. In this paper, we study the model checking problem of pPDA against {\$}{\$}{\backslash}omega {\$}{\$}$\omega$-visibly pushdown languages that can be described by specification logics such as CaRet and are strictly more expressive than {\$}{\$}{\backslash}omega {\$}{\$}$\omega$-regular properties. With these logical formulae, it is possible to specify properties that explicitly take the structured computations arising from procedural programs into account. For example, CaRet is able to match procedure calls with their corresponding future returns, and thus allows to express fundamental program properties like total and partial correctness.}, Address = {Cham}, Author = {Winkler, Tobias and Gehnen, Christina and Katoen, Joost-Pieter}, BookTitle = {Foundations of Software Science and Computation Structures}, Editor = {Bouyer, Patricia and Schr{\"o}der, Lutz}, File = {Model Checking Temporal Properties of Recursive Probabilistic Programs - 978-3-030-99253-8_23 - a.pdf}, ISBN = {978-3-030-99253-8}, Pages = {449--469}, Publisher = {Springer International Publishing}, Title = {Model Checking Temporal Properties of Recursive Probabilistic Programs}, Year = {2022}, date-added = {2023-01-27 08:37:30 +0100}, date-modified = {2023-01-27 08:37:30 +0100}, doi = {10.1007/978-3-030-99253-8_23} }