Encoding induction in correctness proofs of program transformations as a termination problem
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.
| Author: | Conrad Rau, David Sabel, Manfred Schmidt-Schauß |
|---|---|
| URN: | urn:nbn:de:hebis:30:3-269979 |
| Publisher: | University of Innsbruck, Institute of Computer Science |
| Place of publication: | Innsbruck |
| Document Type: | Conference Proceeding |
| Language: | English |
| Year of first Publication: | 2012 |
| Publishing Institution: | Univ.-Bibliothek Frankfurt am Main |
| Tag: | Correctness; Program Transformations; Termination |
| Pagenumber: | 5 |
| First Page: | 74 |
| Last Page: | 78 |
| Institutes: | Informatik |
| Dewey Decimal Classification: | 004 Datenverarbeitung; Informatik |
| Sammlungen: | Universitätspublikationen |
| Note: | 1998 ACM Subject Classification F.3.1 Specifying and Verifying and Reasoning about Programs, F.3.2 Semantics of Programming Languages |
| Licence (German): |  Creative Commons - Namensnennung-Nicht kommerziell-Keine Bearbeitung 3.0 |
