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. I
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.
show moreshow less

Download full text files

Export metadata

  • Export Bibtex
  • Export RIS

Additional Services

    Share in Twitter Search Google Scholar
Metadaten
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
Release Date:2012/10/29
Tag:Correctness; Program Transformations; Termination
Pagenumber:5
First Page:74
Last Page:78
Note:
1998 ACM Subject Classification F.3.1 Specifying and Verifying and Reasoning about Programs,
F.3.2 Semantics of Programming Languages
Institutes:Informatik
Dewey Decimal Classification:004 Datenverarbeitung; Informatik
Sammlungen:Universitätspublikationen
Licence (German):License LogoCreative Commons - Namensnennung-Nicht kommerziell-Keine Bearbeitung 3.0

$Rev: 11761 $