Satisfiability (SAT) based bounded model checkers

摘要

Systems and methods that use a solver to find bugs in a target model of a computing system having one or more finite computation paths are provided. The bugs on computation paths of less than a predetermined length are detected by translating the target model to include a state variable AF for one or more states of the target model, wherein AF(S) represents value of the state variable AF at state S; and solving the translated version of the target model that satisfies predetermined constrains.