Refine
Year of publication
- 2012 (1)
Document Type
- Conference Proceeding (1) (remove)
Language
- English (1)
Has Fulltext
- yes (1) (remove)
Is part of the Bibliography
- no (1)
Keywords
- Program Transformations (1) (remove)
Institute
- Informatik (1) (remove)
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.