LF-checker: Machine Learning Acceleration of Bounded Model Checking for Concurrency Verification (Competition Contribution)
This work addresses efficiency in concurrency verification for software developers and verification engineers, but it is incremental as it builds on existing bounded model checking methods.
The paper tackles the problem of optimizing bounded model checking for concurrency verification by introducing LF-checker, a metaverifier tool that uses machine learning to predict optimal configurations, resulting in better performance than the default settings of the ESBMC verification engine.
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.