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.
@article{arxiv.2301.09142,
title = {LF-checker: Machine Learning Acceleration of Bounded Model Checking for Concurrency Verification (Competition Contribution)},
author = {Tong Wu and Edoardo Manino and Fatimah Aljaafari and Pavlos Petoumenos and Lucas C. Cordeiro},
journal= {arXiv preprint arXiv:2301.09142},
year = {2023}
}