PAC Learning-Based Verification and Model Synthesis

TL;DR

This paper presents a PAC learning-based approach for verifying and synthesizing models of sequential programs, offering probabilistic correctness guarantees and demonstrating promising preliminary results that can outperform existing verifiers.

Contribution

It introduces a novel PAC learning framework for program verification and model synthesis, addressing undecidability issues with probabilistic guarantees.

Findings

Preliminary experiments show promising verification performance.

The method can sometimes outperform mature software verifiers.

Provides probabilistic correctness guarantees for models.

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.