Detail publikace

PAC Learning-Based Verification and Model Synthesis

CHEN, Y. HSIEH, C. LENGÁL, O. LII, T. TSAI, M. WANG, B. WANG, F.

Originální název

PAC Learning-Based Verification and Model Synthesis

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

model synthesis, PAC learning, finite automata, program verification

Autoři

CHEN, Y.; HSIEH, C.; LENGÁL, O.; LII, T.; TSAI, M.; WANG, B.; WANG, F.

Vydáno

16. 2. 2016

Nakladatel

Association for Computing Machinery

Místo

Austin, TX

ISBN

978-1-4503-3900-1

Kniha

Proceedings of the 38th International Conference on Software Engineering

Strany od

714

Strany do

724

Strany počet

11

URL

http://dx.doi.org/10.1145/2884781.2884860

BibTex

@inproceedings{BUT130941,
  author="Yu-Fang {Chen} and Chiao {Hsieh} and Ondřej {Lengál} and Tsung-Ju {Lii} and Ming-Hsien {Tsai} and Bow-Yaw {Wang} and Farn {Wang}",
  title="PAC Learning-Based Verification and Model Synthesis",
  booktitle="Proceedings of the 38th International Conference on Software Engineering",
  year="2016",
  pages="714--724",
  publisher="Association for Computing Machinery",
  address="Austin, TX",
  doi="10.1145/2884781.2884860",
  isbn="978-1-4503-3900-1",
  url="http://dx.doi.org/10.1145/2884781.2884860"
}