Abstract ESBMC, a bounded model checking (BMC) verifier based on SMT solving, has demonstrated its effectiveness in bug detection in recent software verification competitions. We extend its capabilities to enable branch coverage analysis and test suite generation. Our contributions are twofold: (1) we define a branch coverage property and instrument the control flow graph (CFG) to compute branch coverage using SMT solving, and (2) we propose an incremental multi-property reasoning algorithm for efficient and sound test case generation. ESBMC is ranked 7th in the category of Test-Comp 2025.

Bounded model checking (BMC) and fuzzing techniques are among the most effective methods for detecting errors and security vulnerabilities in software. However, there are still shortcomings in detecting these errors due to the inability of existing methods to cover large areas in target code. We proposeFuSeBMCv4, a test generator that synthesizes seeds with useful properties, that we refer to assmart seeds, to improve the performance of its hybrid fuzzer thereby achieving high C program coverage.FuSeBMCworks by first analyzing and incrementally injecting goal labels into the given C program to guide BMC and Evolutionary Fuzzing engines. After that, the engines are employed for an initial period to produce the so–called smart seeds. Finally, the engines are run again, with these smart seeds as starting seeds, in an attempt to achieve maximum code coverage/find bugs. During seed generation and normal running, theTracersubsystem aids coordination between the engines. This subsystem conducts additional coverage analysis and updates a shared memory with information on goals covered so far. Furthermore, theTracerevaluates test-cases dynamically to convert cases into seeds for subsequent test fuzzing. Thus, the BMC engine can provide the seed that allows the fuzzing engine to bypass complex mathematical guards (e.g., input validation). As a result, we received three awards for participation in the fourth international competition in software testing (Test-Comp 2022), outperforming all state-of-the-art tools in every category, including the coverage category.

Abstract The cooperative verification of Bounded Model Checking and Fuzzing has proved to be one of the most effective techniques when testing C programs. FuSeBMC is a test-generation tool that employs BMC and Fuzzing to produce test cases. In Test-Comp 2023, we present an interval approach to FuSeBMC_IA, improving the test generator to use interval methods and abstract interpretation (via Frama-C) to strengthen our instrumentation and fuzzing. Here, an abstract interpretation engine instruments the program as follows. It analyzes different program branches, combines the conditions of each branch, and produces a Constraint Satisfaction Problem (CSP), which is solved using Constraint Programming (CP) by interval manipulation techniques called Contractor Programming. This process has a set of invariants for each branch, which are introduced back into the program as constraints. Experimental results show improvements in reducing CPU time (37%) and memory (13%), while retaining a high score.

Abstract FuSeBMC is a test generator for finding security vulnerabilities in C programs. In Test-Comp 2021, we described a previous version that incrementally injected labels to guide Bounded Model Checking (BMC) and Evolutionary Fuzzing engines to produce test cases for code coverage and bug finding. This paper introduces an improved version of FuSeBMC that utilizes both engines to produce smart seeds. First, the engines run with a short time limit on a lightly instrumented version of the program to produce the seeds. The BMC engine is particularly useful in producing seeds that can pass through complex mathematical guards. Then, FuSeBMC runs its engines with extended time limits using the smart seeds created in the previous round. FuSeBMC manages this process in two main ways. Firstly, it uses shared memory to record the labels covered by each test case. Secondly, it evaluates test cases, and those of high impact are turned into seeds for subsequent test fuzzing. In this year’s competition, we participate in the Cover-Error, Cover-Branches, and Overall categories. The Test-Comp 2022 results show that we significantly increased our code coverage score from last year, outperforming all tools in all categories.

Abstract We describe and evaluate a novel white-box fuzzer for C programs named , which combines fuzzing and symbolic execution, and applies Bounded Model Checking (BMC) to find security vulnerabilities in C programs. explores and analyzes C programs (1) to find execution paths that lead to property violations and (2) to incrementally inject labels to guide the fuzzer and the BMC engine to produce test-cases for code coverage. successfully participates in Test-Comp’21 and achieves first place in the category and second place in the category.