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

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...

Full description

Saved in:
Bibliographic Details
Published in:arXiv.org 2023-01
Main Authors: Wu, Tong, Manino, Edoardo, Aljaafari, Fatimah, Petoumenos, Pavlos, Cordeiro, Lucas C
Format: Article
Language:English
Subjects:
Concurrency
Configurations
Decision trees
Feature extraction
Machine learning
Verification
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:2331-8422