Abstract
Probabilistic programs are typically rather small, but intricate to get correct. Whereas the main control flow is often in place, completing the bits and pieces to obtain a full-fledged program is non-trivial. This talk addresses program sketching: given a partial probabilistic program, i.e., a program with "holes", fill these "holes" such that the resulting program satisfies the specification.
I will outline two approaches: counterexample-guided abstraction refinement (CEGAR) and counterexample-guided inductive synthesis (CEGIS). The CEGAR approach iteratively partitions the design space starting from an abstraction of this space and refines this by a light-weight analysis of verification results. The CEGIS technique exploits critical subsystems as counterexamples to prune all programs behaving incorrectly on that input.
We show how these techniques can be used to sketch probabilistic programs, as well as to synthesise randomised distributed algorithms and controllers for POMDPs.
This is joint work with Sebastian Junges (Berkeley), Milan Ceska and Roman Andriushchenko (Brno).