Master's Thesis

Advanced Methods for Synthesis of Probabilistic Programs

---

Diplomová práce

Pokročilé metody pro syntézu pravděpodobnostních programů

---

Author: Stupinský Šimon, Bc. xstupi00@stud.fit.vutbr.cz

Supervisor: RNDr. Češka Milan, Ph.D. (UITS FIT VUT) ceskam@fit.vut.cz

Reviewer: Mgr. Holík Lukáš, Ph.D. (UITS FIT VUT) holik@fit.vut.cz

Specification:

1. Study the current methods for automated design and synthesis of probabilistic programs including methods based on MDP abstraction and counter-example guided inductive synthesis.
2. Evaluate these methods on practically relevant case-studies and identify their limitations.
3. Design possible improvements and extensions of the methods including the support of optimal synthesis and synthesis for multi-property specifications.
4. Implement the improvements and extensions within an existing probabilistic model-checker (e.g. STORM or PRISM).
5. Carry out a detailed evaluation of the implemented methods including an extension of the existing benchmarks.

Category: Formal Verification

Literature:

1. Milan Češka, Nils Jansen, Sebastian Junges, and Joost-Pieter Katoen. Shepherding hordes of Markov chains. In Proc. of TACAS'19. Springer, 2019.
2. Milan Češka, Christian Hensel, Sebastian Junges, and Joost-Pieter Katoen. Counterexample-Driven Synthesis for Probabilistic Program Sketches. In Proc. of FM'19. Springer, 2019.

Implementation

The implementation is in the repository randriu/synthesis.