System and method for generating a predicate abstraction of a program

摘要

Described is a method that enables the automatic generation of a boolean program that is a predicate abstraction of a program written using a general programming language. The method is capable of abstracting code statements within the program that include procedure calls, assignments, goto statements, conditionals, and pointers. In accordance with the invention, predicates of interest are identified for each code statement in the program. For each particular code statement, the process generates predicate statements that describe an effect that the statement has on the predicates of interest. If the effect of a particular code statement is indeterminable, non-deterministic predicate statements are included in the boolean program to model the indeterminable nature of the code statement. In addition, if a particular code statement includes a procedure call, the arguments and return value of the procedure call are translated to associated predicates in the calling context.