Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs

Explore a 17-minute conference talk from POPL 2024 that delves into programmatic strategy synthesis for resolving nondeterminism in probabilistic programs. Learn how researchers from RWTH Aachen University develop a semi-automatic approach using deductive verification techniques to find memoryless and deterministic strategies that satisfy quantitative specifications in programs involving both randomization and pure nondeterminism. Discover the application of weakest precondition-style frameworks for loop-free programs and the use of loop invariants for programs with loops. Gain insights into the relationship between this technique and strategy obtainment in countably infinite Markov decision processes with reachability-reward objectives. Examine case studies demonstrating the practical application of this innovative approach to program verification and strategy synthesis.