PAC Learning-Based Verification and Model Synthesis

2015/11/03 by Yu-Fang Chen, Yu‐Fang Chen, Chen, Yu-Fang +12 · 2 citations
Computer Science · #Formal Methods in Verification #Machine Learning and Algorithms #Software Testing and Debugging Techniques #cs.LG #cs.LO #cs.SE

paper · pdf · doi:10.48550/arxiv.1511.00754

11 pages

arxiv created 2015/11/03 · arxiv updated 2015/11/04

Abstract

We introduce a novel technique for verification and model synthesis of sequential programs. Our technique is based on learning a 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.

Cited by

• Reachability of Linear Uncertain Systems: Sampling Based Approaches
• Data-Driven Probabilistic Evaluation of Logic Properties with PAC-Confidence on Mealy Machines

Related

• Model Learning: A Survey on Foundation, Tools and Applications
• Models That Prove Their Own Correctness
• Interpolation and SAT-Based Model Checking Revisited: Adoption to Software Verification
• Extract, model, refine: improved modelling of program verification tools through data enrichment
• Toward Trustworthy Neural Program Synthesis