FuSeBMC AI: Acceleration of Hybrid Approach through Machine Learning

TL;DR

FuSeBMC-AI addresses the challenge of selecting optimal configuration flags for a hybrid verification pipeline that combines fuzzing and bounded model checking by learning from program features. It extends FuSeBMC with a feature-based ML framework (SVM and neural networks) to predict flag settings, training on SV-Comp/Test-Comp benchmarks and evaluating over 384 flag combinations per program. The work demonstrates notable resource reductions and targeted improvements in several categories (e.g., up to $86\%$ in ControlFlow, $84\%$ in Termination-Main ControlFlow) while acknowledging dataset limitations as a key constraint. The approach offers a scalable, data-driven method to tune verification engines, with publicly available tooling and data to support replication and extension in practice.

Abstract

We present FuSeBMC-AI, a test generation tool grounded in machine learning techniques. FuSeBMC-AI extracts various features from the program and employs support vector machine and neural network models to predict a hybrid approach optimal configuration. FuSeBMC-AI utilizes Bounded Model Checking and Fuzzing as back-end verification engines. FuSeBMC-AI outperforms the default configuration of the underlying verification engine in certain cases while concurrently diminishing resource consumption.

Figures (1)

• Figure 1: The major components of the FuSeBMC-AI test generator and how they interact.