Patent ID: 7653520
Filing Date: 2010-01-26
Classification: G06F

Abstract:
1. A method for performing bounded model checking to test if a property of interest is violated within a number of steps of a program, comprising: unfolding the program for the number of steps to create a program formula; translating the property of interest into an automaton; encoding a transition system of said automaton into a Boolean formula creating a transition formula; conjoining the program formula with the transition formula to create a conjoined formula, wherein the conjoined formula contains at least one state variable with a non-finite domain; deciding a satisfiability of the conjoined formula, while maintaining the at least one state variable with a non-finite domain as a state variable with a non-finite domain, wherein the conjoined formula is satisfiable if there exists an assignment of values to variables of the conjoined formula that would make the conjoined formula true and wherein the conjoined formula is unsatisfiable if there does not exist an assignment of values to the variables of the conjoined formula that would make the conjoined formula true; and if the conjoined formula is satisfiable, outputting a signal that the property of interest is violated within the number of steps, and if the conjoined formula is unsatisfiable outputting a signal that the property of interest is not violated within the number of steps.