Counterexample-Driven Synthesis for Probabilistic Program Sketches

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F19%3APU134955" target="_blank" >RIV/00216305:26230/19:PU134955 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1007/978-3-030-30942-8_8" target="_blank" >http://dx.doi.org/10.1007/978-3-030-30942-8_8</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-030-30942-8_8" target="_blank" >10.1007/978-3-030-30942-8_8</a>

Jazyk výsledku

angličtina

Název v původním jazyce

Counterexample-Driven Synthesis for Probabilistic Program Sketches

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Counterexample-Driven Synthesis for Probabilistic Program Sketches

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.

Návaznosti

P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)

Rok uplatnění

2019

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Proceedings of the 23rd International Symposium on Formal Methods.

ISBN

978-3-030-30941-1

ISSN

—

e-ISSN

—

Počet stran výsledku

19

Strana od-do

101-120

Název nakladatele

Springer International Publishing

Místo vydání

Porto

Místo konání akce

Porto

Datum konání akce

17. 6. 2019

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—