Geração de casos de teste usando Bounded Model Checking

Abstract

Testcase generation consists in generating inputs for an algorithm that are able to explore all paths of a program, maximizing its coverage. Usually, fuzzing techniques are used because of its great performace and low cost. However, formal techniques such as Symbolic Execution are gaining notority in this domain, one of those is Bounded Model Checking (BMC). BMC is a verification technique that encodes a property in paths of transition system up to a bound k to one single logic formula such that if the system contains a flaw the formula will generate a proof. This proof contain information for the testcase generation. The difficult of using BMC for testcase is at the time/space complexity and at the optimizations trying to workaround this issue. Incremental BMC is a strategy that increases the k limit until the violation is found or the system is completely verified. The issue is that at each increment every path is verified again, which add time and memory consuption to solve the current instance. To solve those issue this work proposes two main contributions: (1) algorithm for testcase generation using proofs; and (2) a caching system that uses small instances by: (A) direct use; and (B) indirect use of other systems. Those contributions were implemented into the Efficient SMT-based Bounded Model Checker (ESBMC), being tested over Continuos Integration and over public benchmarks of C programs, obtaining the first place at TestComp’21 in the Cover-error category and reducing the time of the CI.