PAC Learning-Based Verification and Model Synthesis

Result code in 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>

Result on the web

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

Result language

angličtina

Original language name

PAC Learning-Based Verification and Model Synthesis

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

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

Project

<a href="/en/project/GA16-17538S" target="_blank" >GA16-17538S: Relaxed equivalence checking for approximate computing</a><br>

Continuities

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

Publication year

2016

Confidentiality

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

Article name in the collection

Proceedings of the 38th International Conference on Software Engineering

ISBN

978-1-4503-3900-1

ISSN

—

e-ISSN

—

Number of pages

11

Pages from-to

714-724

Publisher name

Association for Computing Machinery

Place of publication

Austin, TX

Event location

Austin, TX

Event date

May 14, 2016

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000406138600063