LF-checker: Machine Learning Acceleration of Bounded Model Checking for Concurrency Verification (Competition Contribution)

TL;DR

LF-checker leverages machine learning to optimize bounded model checking configurations, significantly improving concurrency verification efficiency by predicting optimal settings with a decision tree, outperforming default configurations.

Contribution

Introduces LF-checker, a machine learning-based tool that predicts optimal verification configurations for concurrency verification, enhancing efficiency over default settings.

Findings

LF-checker outperforms default verification configurations.

Machine learning improves verification speed and accuracy.

Specialized in concurrency verification using ESBMC.

Abstract

We describe and evaluate LF-checker, a metaverifier tool based on machine learning. It extracts multiple features of the program under test and predicts the optimal configuration (flags) of a bounded model checker with a decision tree. Our current work is specialised in concurrency verification and employs ESBMC as a back-end verification engine. In the paper, we demonstrate that LF-checker achieves better results than the default configuration of the underlying verification engine.