Effectively Eliminating Auxiliaries

Stijn de Gouw, Jurriaan Rot

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

Abstract

Auxiliary variables are used in the intermediate steps of a correctness proof to store additional information about the computation. We investigate for which classes of programs auxiliary variables can be avoided in the associated proof system, and give effective translations of proofs whenever this is the case.
Original languageEnglish
Title of host publicationTheory and Practice of Formal Methods
Subtitle of host publicationEssays Dedicated to Frank de Boer on the Occasion of His 60th Birthday
EditorsErika Ábrahám, Marcello Bonsangue, Einar Broch Johnsen
PublisherSpringer
Pages226-241
Number of pages16
ISBN (Electronic)978-3-319-30734-3
ISBN (Print)978-3-319-30733-6
DOIs
Publication statusPublished - 2016
Externally publishedYes

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume9660
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349
NameTheoretical Computer Science and General Issues
PublisherSpringer
Volume9660

Fingerprint

Auxiliary Variables
Proof System
Correctness
Class

Cite this

Gouw, S. D., & Rot, J. (2016). Effectively Eliminating Auxiliaries. In E. Ábrahám, M. Bonsangue, & E. Broch Johnsen (Eds.), Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday (pp. 226-241). (Lecture Notes in Computer Science; Vol. 9660), (Theoretical Computer Science and General Issues; Vol. 9660). Springer. https://doi.org/10.1007/978-3-319-30734-3_16
Gouw, Stijn de ; Rot, Jurriaan. / Effectively Eliminating Auxiliaries. Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday. editor / Erika Ábrahám ; Marcello Bonsangue ; Einar Broch Johnsen. Springer, 2016. pp. 226-241 (Lecture Notes in Computer Science). (Theoretical Computer Science and General Issues).
@inbook{213f74ad5c184fbf95f5b153d257af9e,
title = "Effectively Eliminating Auxiliaries",
abstract = "Auxiliary variables are used in the intermediate steps of a correctness proof to store additional information about the computation. We investigate for which classes of programs auxiliary variables can be avoided in the associated proof system, and give effective translations of proofs whenever this is the case.",
author = "Gouw, {Stijn de} and Jurriaan Rot",
year = "2016",
doi = "10.1007/978-3-319-30734-3_16",
language = "English",
isbn = "978-3-319-30733-6",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "226--241",
editor = "Erika {\'A}brah{\'a}m and Marcello Bonsangue and {Broch Johnsen}, Einar",
booktitle = "Theory and Practice of Formal Methods",

}

Gouw, SD & Rot, J 2016, Effectively Eliminating Auxiliaries. in E Ábrahám, M Bonsangue & E Broch Johnsen (eds), Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday. Lecture Notes in Computer Science, vol. 9660, Theoretical Computer Science and General Issues, vol. 9660, Springer, pp. 226-241. https://doi.org/10.1007/978-3-319-30734-3_16

Effectively Eliminating Auxiliaries. / Gouw, Stijn de; Rot, Jurriaan.

Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday. ed. / Erika Ábrahám; Marcello Bonsangue; Einar Broch Johnsen. Springer, 2016. p. 226-241 (Lecture Notes in Computer Science; Vol. 9660), (Theoretical Computer Science and General Issues; Vol. 9660).

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

TY - CHAP

T1 - Effectively Eliminating Auxiliaries

AU - Gouw, Stijn de

AU - Rot, Jurriaan

PY - 2016

Y1 - 2016

N2 - Auxiliary variables are used in the intermediate steps of a correctness proof to store additional information about the computation. We investigate for which classes of programs auxiliary variables can be avoided in the associated proof system, and give effective translations of proofs whenever this is the case.

AB - Auxiliary variables are used in the intermediate steps of a correctness proof to store additional information about the computation. We investigate for which classes of programs auxiliary variables can be avoided in the associated proof system, and give effective translations of proofs whenever this is the case.

UR - https://link.springer.com/book/10.1007/978-3-319-30734-3

U2 - 10.1007/978-3-319-30734-3_16

DO - 10.1007/978-3-319-30734-3_16

M3 - Chapter

SN - 978-3-319-30733-6

T3 - Lecture Notes in Computer Science

SP - 226

EP - 241

BT - Theory and Practice of Formal Methods

A2 - Ábrahám, Erika

A2 - Bonsangue, Marcello

A2 - Broch Johnsen, Einar

PB - Springer

ER -

Gouw SD, Rot J. Effectively Eliminating Auxiliaries. In Ábrahám E, Bonsangue M, Broch Johnsen E, editors, Theory and Practice of Formal Methods: Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday. Springer. 2016. p. 226-241. (Lecture Notes in Computer Science). (Theoretical Computer Science and General Issues). https://doi.org/10.1007/978-3-319-30734-3_16