Publication Details

PAC Learning-Based Verification and Model Synthesis

CHEN Yu-Fang, HSIEH Chiao, LENGÁL Ondřej, LII Tsung-Ju, TSAI Ming-Hsien, WANG Bow-Yaw and WANG Farn. PAC Learning-Based Verification and Model Synthesis. In: Proceedings of the 38th International Conference on Software Engineering. Austin, TX: Association for Computing Machinery, 2016, pp. 714-724. ISBN 978-1-4503-3900-1. Available from: http://dx.doi.org/10.1145/2884781.2884860
Czech title
Verifikace a syntéza modelu založené na PAC učení
Type
conference paper
Language
english
Authors
Chen Yu-Fang (ASIN)
Hsieh Chiao (ASIN)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Lii Tsung-Ju (NTU)
Tsai Ming-Hsien (ASIN)
Wang Bow-Yaw (ASIN)
Wang Farn (NTU)
URL
Keywords

model synthesis, PAC learning, finite automata, program verification

Abstract

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.

Published
2016
Pages
714-724
Proceedings
Proceedings of the 38th International Conference on Software Engineering
Conference
38th International Conference on Software Engineering, Austin, TX, US
ISBN
978-1-4503-3900-1
Publisher
Association for Computing Machinery
Place
Austin, TX, US
DOI
UT WoS
000406138600063
EID Scopus
BibTeX
@INPROCEEDINGS{FITPUB11087,
   author = "Yu-Fang Chen and Chiao Hsieh and Ond\v{r}ej Leng\'{a}l and Tsung-Ju Lii and Ming-Hsien Tsai and Bow-Yaw Wang and Farn Wang",
   title = "PAC Learning-Based Verification and Model Synthesis",
   pages = "714--724",
   booktitle = "Proceedings of the 38th International Conference on Software Engineering",
   year = 2016,
   location = "Austin, TX, US",
   publisher = "Association for Computing Machinery",
   ISBN = "978-1-4503-3900-1",
   doi = "10.1145/2884781.2884860",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11087"
}
Back to top