Real-Time Interaction with a Humanoid Avatar in an Immersive Table Tennis Simulation. - Stephan Rusdorf; Guido Brunnett; Mario Lorenz 003; Tobias Winkler 001 (IEEE Trans. Vis. Comput. Graph., 2007)

Stochastic Games with Lexicographic Reachability-Safety Objectives. - Krishnendu Chatterjee; Joost-Pieter Katoen; Maximilian Weininger; Tobias Winkler 001 (CAV (2), 2020)

Approximating Values of Generalized-Reachability Stochastic Games. - Pranav Ashok; Krishnendu Chatterjee; Jan Kretínský; Maximilian Weininger; Tobias Winkler 001 (LICS, 2020)

Generating Functions for Probabilistic Programs. - Lutz Klinkenberg; Kevin Batz; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Joshua Moerman; Tobias Winkler 001 (LOPSTR, 2020)

Stochastic Games with Disjunctions of Multiple Objectives (Technical Report). - Tobias Winkler 001; Maximilian Weininger (CoRR, 2021)

Stochastic Games with Disjunctions of Multiple Objectives. - Tobias Winkler 001; Maximilian Weininger (GandALF, 2021)

The complexity of reachability in parametric Markov decision processes. - Sebastian Junges; Joost-Pieter Katoen; Guillermo A. Pérez 001; Tobias Winkler 001 (J. Comput. Syst. Sci., 2021)

Does a Program Yield the Right Distribution? - Verifying Probabilistic Programs via Generating Functions. - Mingshuai Chen; Joost-Pieter Katoen; Lutz Klinkenberg; Tobias Winkler 001 (CAV (1), 2022)

Out of Control: Reducing Probabilistic Models by Control-State Elimination. - Tobias Winkler 001; Johannes Lehmann 001; Joost-Pieter Katoen (VMCAI, 2022)

Weighted Programming. - Kevin Batz; Adrian Gallus; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Tobias Winkler 001 (CoRR, 2022)

Weighted programming: a programming paradigm for specifying mathematical models. - Kevin Batz; Adrian Gallus; Benjamin Lucien Kaminski; Joost-Pieter Katoen; Tobias Winkler 001 (Proc. ACM Program. Lang., 2022)

Prodigy - Artifact Evaluation at CAV 2022. - Mingshuai Chen; Joost-Pieter Katoen; Lutz Klinkenberg; Tobias Winkler 001 (Zenodo, 2022)

On Certificates, Expected Runtimes, and Termination in Probabilistic Pushdown Automata. - Tobias Winkler 001; Joost-Pieter Katoen (LICS, 2023)

Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration. - Tobias Winkler 001; Joost-Pieter Katoen (TACAS (2), 2023)

Exact Probabilistic Inference Using Generating Functions. - Lutz Klinkenberg; Tobias Winkler 001; Mingshuai Chen; Joost-Pieter Katoen (CoRR, 2023)

Model Checking Temporal Properties of Recursive Probabilistic Programs. - Tobias Winkler 001; Christina Gehnen; Joost-Pieter Katoen (Log. Methods Comput. Sci., 2023)

ARTIFACT EVALUATION FOR TACAS '23 SUBMISSION 103: "Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration". - Tobias Winkler 001; Joost-Pieter Katoen (Zenodo, 2023)

Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains (Artifact). - Hannah Mertens; Joost-Pieter Katoen; Tim Quatmann; Tobias Winkler 001 (Zenodo, 2023)

J-P: MDP. FP. PP - Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs. - Kevin Batz; Benjamin Lucien Kaminski; Christoph Matheja; Tobias Winkler 001 (Principles of Verification (1), 2024)

Markov Decision Processes with Sure Parity and Multiple Reachability Objectives. - Raphaël Berthon; Joost-Pieter Katoen; Tobias Winkler 001 (RP, 2024)

Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains. - Hannah Mertens; Joost-Pieter Katoen; Tim Quatmann; Tobias Winkler 001 (TACAS (2), 2024)

J-P: MDP. FP. PP.: Characterizing Total Expected Rewards in Markov Decision Processes as Least Fixed Points with an Application to Operational Semantics of Probabilistic Programs (Technical Report). - Kevin Batz; Benjamin Lucien Kaminski; Christoph Matheja; Tobias Winkler 001 (CoRR, 2024)

Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs. - Kevin Batz; Tom Jannik Biskup; Joost-Pieter Katoen; Tobias Winkler 001 (Proc. ACM Program. Lang., 2024)

Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate (Artifact). - Hannah Mertens; Tim Quatmann; Joost-Pieter Katoen; Tobias Winkler 001 (Zenodo, 2024)

Stochastic games with lexicographic objectives. - Krishnendu Chatterjee; Joost-Pieter Katoen; Stefanie Mohr; Maximilian Weininger; Tobias Winkler 001 (Formal Methods Syst. Des., 2024)

Efficient Probabilistic Model Checking for Relational Reachability. - Lina Gerlach; Tobias Winkler 001; Erika Ábrahám; Borzoo Bonakdarpour; Sebastian Junges (CAV (1), 2025)

Fixed Point Certificates for Reachability and Expected Rewards in MDPs. - Krishnendu Chatterjee; Tim Quatmann; Maximilian Schäffeler; Maximilian Weininger; Tobias Winkler 001; Daniel Zilken (TACAS (2), 2025)

Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back. - Kevin Batz; Joost-Pieter Katoen; Francesca Randone; Tobias Winkler 001 (Proc. ACM Program. Lang., 2025)

Artifact: Fixed Point Certificates for Reachability and Expected Rewards in MDPs. - Krishnendu Chatterjee; Tim Quatmann; Maximilian Schäffeler; Maximilian Weininger; Tobias Winkler 001; Daniel Zillken (Zenodo, 2025)

Efficient Probabilistic Model Checking for Relational Reachability (Extended Version). - Lina Gerlach; Tobias Winkler 001; Erika Ábrahám; Borzoo Bonakdarpour; Sebastian Junges (CoRR, 2025)