Computing Expected Runtimes for Constant Probability Programs. - Jürgen Giesl; Peter Giesl; Marcel Hark (CADE, 2019)

Aiming Low Is Harder - Inductive Proof Rules for Lower Bounds on Weakest Preexpectations in Probabilistic Program Verification. - Marcel Hark; Benjamin Lucien Kaminski; Jürgen Giesl; Joost-Pieter Katoen (CoRR, 2019)

On the Decidability of Termination for Polynomial Loops. - Florian Frohn; Marcel Hark; Jürgen Giesl (CoRR, 2019)

Polynomial Loops: Beyond Termination. - Marcel Hark; Florian Frohn; Jürgen Giesl (LPAR, 2020)

Termination of Polynomial Loops. - Florian Frohn; Marcel Hark; Jürgen Giesl (SAS, 2020)

Aiming low is harder: induction for lower bounds in probabilistic program verification. - Marcel Hark; Benjamin Lucien Kaminski; Jürgen Giesl; Joost-Pieter Katoen (Proc. ACM Program. Lang., 2020)

Inferring Expected Runtimes of Probabilistic Integer Programs Using Expected Sizes. - Fabian Meyer; Marcel Hark; Jürgen Giesl (TACAS (1), 2021)

Towards complete methods for automatic complexity and termination analysis of (probabilistic) programs. - Marcel Hark (2021)

Improving Automatic Complexity Analysis of Integer Programs. - Jürgen Giesl; Nils Lommen; Marcel Hark; Fabian Meyer (The Logic of Software. A Tasting Menu of Formal Methods, 2022)

Termination of triangular polynomial loops. - Marcel Hark; Florian Frohn; Jürgen Giesl (Formal Methods Syst. Des., 2025)