Skip to content

Advanced Methods for Synthesis of Probabilistic Programs

License

Notifications You must be signed in to change notification settings

xstupi00/Master-s-Thesis

Repository files navigation

Master's Thesis


Diplomová práce


Author: Stupinský Šimon, Bc. xstupi00@stud.fit.vutbr.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.