An evolutionary approach for Bounded Model Checking

The Bounded Model Checking problem can be efficiently reduced to a propositional satisfiability problem, and therefore be solved by SAT solvers. In this work, we introduce an evolutionary algorithm that makes use of the multilevel paradigm for the boundary model checking problem. The multilevel paradigm refers to the process of dividing large and difficult problems into smaller ones, which are hopefully much easier to solve, and then work backward towards the solution of the original problem, using a solution from a previous level as a starting solution at the next level. Results on real model checking industrial instances are presented.