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. We show that 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.