TY  - CONF
A1  - Rau, Conrad
A1  - Sabel, David
A1  - Schmidt-Schauß, Manfred
T1  - Encoding induction in correctness proofs of program transformations as a termination problem
T2  - 12th International Workshop on Termination (WST 2012) : WST 2012, February 19–23, 2012, Obergurgl, Austria / edited by Georg Moser
Termination (WST 2012)
N2  - The diagram-based method to prove correctness of program transformations consists of computing
complete set of (forking and commuting) diagrams, acting on sequences of standard reductions
and program transformations. In many cases, the only missing step for proving correctness of a
program transformation is to show the termination of the rearrangement of the sequences. Therefore
we encode complete sets of diagrams as term rewriting systems and use an automated tool
to show termination, which provides a further step in the automation of the inductive step in
correctness proofs.
KW  - Termination
KW  - Program Transformations
KW  - Correctness
Y1  - 2012
UR  - http://publikationen.ub.uni-frankfurt.de/frontdoor/index/index/docId/26997
UR  - https://nbn-resolving.org/urn:nbn:de:hebis:30:3-269979
N1  - 1998 ACM Subject Classification F.3.1 Specifying and Verifying and Reasoning about Programs,
F.3.2 Semantics of Programming Languages
SP  - 74
EP  - 78
PB  - University of Innsbruck, Institute of Computer Science
CY  - Innsbruck
ER  -