Detail publikace

Counterexample-Driven Synthesis for Probabilistic Program Sketches

ČEŠKA, M. HENSE, C. JUNGES, S. KATOEN, J.

Originální název

Counterexample-Driven Synthesis for Probabilistic Program Sketches

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální abstrakt

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 nite-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.

Klíčová slova

probabilistic programs, synthesis, counter-examples, SMT solving

Autoři

ČEŠKA, M.; HENSE, C.; JUNGES, S.; KATOEN, J.

Vydáno

17. 6. 2019

Nakladatel

Springer International Publishing

Místo

Porto

ISBN

978-3-030-30941-1

Kniha

Proceedings of the 23rd International Symposium on Formal Methods.

Edice

Lecture Notes of Computer Science

Strany od

101

Strany do

120

Strany počet

19

BibTex

@inproceedings{BUT161455,
  author="ČEŠKA, M. and HENSE, C. and JUNGES, S. and KATOEN, J.",
  title="Counterexample-Driven Synthesis for Probabilistic Program Sketches",
  booktitle="Proceedings of the 23rd International Symposium on Formal Methods.",
  year="2019",
  series="Lecture Notes of Computer Science",
  pages="101--120",
  publisher="Springer International Publishing",
  address="Porto",
  doi="10.1007/978-3-030-30942-8\{_}8",
  isbn="978-3-030-30941-1"
}