Abstraction-based partial deduction for solving inverse problems { a transformational approach to software veri

Abstract. We present an approach to software verification by program inversion, exploiting recent progress in the field of automatic program transformation, partial deduction and abstract interpretation. Abstrac-tion-based partial deduction can work on infinite state spaces and pro-duce finite representations of infinite solution sets. We illustrate the po-tential of this approach for infinite model checking of safety properties.