Publication Details

Counterexample-Driven Synthesis for Probabilistic Program Sketches

ČEŠKA Milan, HENSE Christian, JUNGES Sebastian and KATOEN Joost-Pieter. Counterexample-Driven Synthesis for Probabilistic Program Sketches. In: Proceedings of the 23rd International Symposium on Formal Methods.. Lecture Notes of Computer Science. Porto: Springer International Publishing, 2019, pp. 101-120. ISBN 978-3-030-30941-1.
Czech title
Syntéza pravděpodobnostních programů
Type
conference paper
Language
english
Authors
Češka Milan, RNDr., Ph.D. (DITS FIT BUT)
Hense Christian (RWTH Aachen University)
Junges Sebastian (RWTH Aachen University)
Katoen Joost-Pieter (RWTH)
Keywords

probabilistic programs, synthesis, counter-examples, SMT solving

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.

Published
2019
Pages
101-120
Proceedings
Proceedings of the 23rd International Symposium on Formal Methods.
Series
Lecture Notes of Computer Science
Conference
23rd International Symposium on Formal Methods,, Porto, PT
ISBN
978-3-030-30941-1
Publisher
Springer International Publishing
Place
Porto, PT
DOI
EID Scopus
BibTeX
@INPROCEEDINGS{FITPUB12010,
   author = "Milan \v{C}e\v{s}ka and Christian Hense and Sebastian Junges and Joost-Pieter Katoen",
   title = "Counterexample-Driven Synthesis for Probabilistic Program Sketches",
   pages = "101--120",
   booktitle = "Proceedings of the 23rd International Symposium on Formal Methods.",
   series = "Lecture Notes of Computer Science",
   year = 2019,
   location = "Porto, PT",
   publisher = "Springer International Publishing",
   ISBN = "978-3-030-30941-1",
   doi = "10.1007/978-3-030-30942-8\_8",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/12010"
}
Back to top