The invention provides bounded model checking of a program with respect to a property of interest comprising unfolding the program for a number of steps to create a program formula; translating the property of interest into an automaton; encoding the transition system of the automaton into a Boolean formula creating a transition formula; conjoining the program formula with the transition formula to create a conjoined formula; and deciding the satisfiability of the conjoined formula.