# Counterexample-Driven Synthesis for Probabilistic Program Sketches

## TL;DR

This paper introduces a counterexample-guided synthesis method for probabilistic programs, enabling automatic generation of finite-state models by efficiently exploring large design spaces with minimal verification queries.

## Contribution

It presents a novel approach combining CEGIS with model checking and SMT solving for probabilistic program synthesis, improving scalability and automation.

## Key findings

- Can explore millions of candidate designs with few thousand queries
- Effective in practical case studies involving complex probabilistic programs
- Demonstrates scalability and efficiency of the proposed synthesis method

## Abstract

Probabilistic programs are key to deal with uncertainty in e.g. controller synthesis. They are typically small but intricate. Their development is complex and error prone requiring quantitative reasoning over a myriad of alternative designs. To mitigate this complexity, we adopt counterexample-guided inductive synthesis (CEGIS) to automatically synthesise finite-state probabilistic programs. Our approach leverages efficient model checking, modern SMT solving, and counterexample generation at program level. Experiments on practically relevant case studies show that design spaces with millions of candidate designs can be fully explored using a few thousand verification queries.