Přístupnostní navigace
E-application
Search Search Close
Publication detail
ČEŠKA, M. HENSE, C. JUNGES, S. KATOEN, J.
Original Title
Counterexample-Driven Synthesis for Probabilistic Program Sketches
Type
conference paper
Language
English
Original 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 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.
Keywords
probabilistic programs, synthesis, counter-examples, SMT solving
Authors
ČEŠKA, M.; HENSE, C.; JUNGES, S.; KATOEN, J.
Released
17. 6. 2019
Publisher
Springer International Publishing
Location
Porto
ISBN
978-3-030-30941-1
Book
Proceedings of the 23rd International Symposium on Formal Methods.
Edition
Lecture Notes of Computer Science
Pages from
101
Pages to
120
Pages count
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" }