Get our free extension to see links to code for papers anywhere online!

Chrome logo Add to Chrome

Firefox logo Add to Firefox


Counterexample-Driven Synthesis for Probabilistic Program Sketches

Apr 28, 2019
Milan Češka, Christian Hensel, Sebastian Junges, Joost-Pieter Katoen



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.

* Extended version 


Share this with someone who'll enjoy it:

   Access Paper Source



Share this with someone who'll enjoy it: