We consider imperative programs that involve both randomization and pure nondeterminism. The central question is how to find a strategy resolving the pure nondeterminism such that the so-obtained determinized program satisfies a given quantitative specification, i.e., bounds on expected outcomes such as the expected final value of a program variable or the probability to terminate in a given set of states.

We show how memoryless and deterministic (MD) strategies can be obtained in a semi-automatic fashion using deductive verification. For loop-free programs, the MD strategies resulting from our weakest precondition-style framework are correct by construction. This extends to loopy programs, provided the loops are equipped with suitable loop invariants - just like in program verification.

We show how our technique relates to the well-studied problem of obtaining strategies in countably infinite Markov decision processes with reachability-reward objectives.

I will show the applicability of this approach by means of some case studies.

(This is based on joint work with Kevin Batz, Tom Biskup, and Tobias Winkler.)