MOVES Seminars 7 Oct 2010
Carsten Fuhs
Lazy Abstraction for Size-Change Termination
Abstract:
Size-change termination is a widely used means of proving termination
where source programs are first abstracted to size-change graphs which
are then analyzed to determine if they satisfy the size-change
termination property. Here, the choice of the abstraction is crucial to
the success of the method, and it is an open problem how to choose an
abstraction such that no critical loss of precision occurs. We show how
to couple the search for a suitable abstraction and the test for
size-change termination via an encoding to a single SAT instance. In
this way, the problem of choosing the right abstraction is solved en
passant by a SAT solver. For the setting of term rewriting, the
integration of this approach into the dependency pair framework works
smoothly and gives rise to a new class of size-change reduction pairs.
We implemented size-change reduction pairs in the termination prover
AProVE and evaluated their usefulness in extensive experiments.
Size-change termination is a widely used means of proving termination
where source programs are first abstracted to size-change graphs which
are then analyzed to determine if they satisfy the size-change
termination property. Here, the choice of the abstraction is crucial to
the success of the method, and it is an open problem how to choose an
abstraction such that no critical loss of precision occurs. We show how
to couple the search for a suitable abstraction and the test for
size-change termination via an encoding to a single SAT instance. In
this way, the problem of choosing the right abstraction is solved en
passant by a SAT solver. For the setting of term rewriting, the
integration of this approach into the dependency pair framework works
smoothly and gives rise to a new class of size-change reduction pairs.
We implemented size-change reduction pairs in the termination prover
AProVE and evaluated their usefulness in extensive experiments.
