Satisfiability (SAT) Based Bounded Model Checkers

A computer-implemented method for determining whether a computing system satisfies a temporal logic property by exploring the underlying state space, the method comprising:

• translating a target model for the computing system 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, having one or more finite paths, that satisfies predetermined constrains defined as:
• AF(S0)→Bad(S0)
• AF(Si)→(AF(Si−1)νBAD(Si)) i>0
• where:
• AF(Si) is the current state Si, and
• BAD(Si) is a Boolean predicate representing the failed states.

A computer implemented system for determining whether a computing system satisfies a temporal logic property by exploring state space of the computing system, the system comprising:

• a translator for translating a target model for the computing system 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
• a solver for solving the translated version of the target model that satisfies predetermined constrains defined as either:
• AF(S0)Bad(S0)
• AF(Si)(AF(Si−1)νBAD(Si)) i>0
• or
• AF(S0)→Bad(S0)
• AF(Si)→(AF(Si−1)νBAD(Si)) i>0
• where:
• AF(Si) is the current state Si, and
• BAD(Si) is a Boolean predicate representing the failed states.

Computer program product comprising logic code for determining whether a computing system satisfies a temporal logic property by exploring state space of the computing system, wherein the logic code is stored on a non-transient computer readable storage medium, wherein execution of the logic code on a computer causes the computer to:

• translate a target model for the computing system 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
• solve the translated version of the target model that satisfies predetermined constrains defined as either:
• AF(S0)Bad(S0)
• AF(Si)(AF(Si−1)νBAD(Si)) i>0
• or
• AF(S0)→Bad(S0)
• AF(Si)→(AF(Si−1)νBAD(Si)) i>0
• where:
• AF(Si) is the current state Si, and
• BAD(Si) is a Boolean predicate representing the failed states.