Property Checking Without Invariant Generation

摘要: We introduce a procedure for proving safety properties. This is based on technique called Partial Quantifier Elimination (PQE). In contrast to complete quantifier elimination, in PQE, only part of the formula taken out scope quantifiers. So, PQE can be dramatically more efficient than elimination. The appeal our twofold. First, it prove property without generating an inductive invariant. Second, employs depth-first search and so used find deep bugs.