PAC Learning-Based Verification and Model Synthesis

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F16%3APU121597" target="_blank" >RIV/00216305:26230/16:PU121597 - isvavai.cz</a>

Výsledek na webu

<a href="http://dx.doi.org/10.1145/2884781.2884860" target="_blank" >http://dx.doi.org/10.1145/2884781.2884860</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1145/2884781.2884860" target="_blank" >10.1145/2884781.2884860</a>

Jazyk výsledku

angličtina

Název v původním jazyce

PAC Learning-Based Verification and Model Synthesis

Popis výsledku v původním jazyce

We introduce a novel technique for verification and model synthesis of sequential programs. Our technique is based on learning an approximate regular model of the set of feasible paths in a program, and testing whether this model contains an incorrect behavior. Exact learning algorithms require checking equivalence between the model and the program, which is a difficult problem, in general undecidable. Our learning procedure is therefore based on the framework of probably approximately correct (PAC) learning, which uses sampling instead, and provides correctness guarantees expressed using the terms error probability and confidence. Besides the verification result, our procedure also outputs the model with the said correctness guarantees. Obtained preliminary experiments show encouraging results, in some cases even outperforming mature software verifiers.

Název v anglickém jazyce

PAC Learning-Based Verification and Model Synthesis

Popis výsledku anglicky

We introduce a novel technique for verification and model synthesis of sequential programs. Our technique is based on learning an approximate regular model of the set of feasible paths in a program, and testing whether this model contains an incorrect behavior. Exact learning algorithms require checking equivalence between the model and the program, which is a difficult problem, in general undecidable. Our learning procedure is therefore based on the framework of probably approximately correct (PAC) learning, which uses sampling instead, and provides correctness guarantees expressed using the terms error probability and confidence. Besides the verification result, our procedure also outputs the model with the said correctness guarantees. Obtained preliminary experiments show encouraging results, in some cases even outperforming mature software verifiers.

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

<a href="/cs/project/GA16-17538S" target="_blank" >GA16-17538S: Přibližná ekvivalence pro aproximativní počítání</a><br>

Návaznosti

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

Rok uplatnění

2016

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 38th International Conference on Software Engineering

ISBN

978-1-4503-3900-1

ISSN

—

e-ISSN

—

Počet stran výsledku

11

Strana od-do

714-724

Název nakladatele

Association for Computing Machinery

Místo vydání

Austin, TX

Místo konání akce

Austin, TX

Datum konání akce

14. 5. 2016

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

WRD - Celosvětová akce

Kód UT WoS článku

000406138600063