Effectively Eliminating Auxiliaries

Stijn de Gouw; Jurriaan Rot

doi:10.1007/978-3-319-30734-3_16

Effectively Eliminating Auxiliaries

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-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 language	English
Title of host publication	Theory and Practice of Formal Methods
Subtitle of host publication	Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday
Editors	Erika Ábrahám, Marcello Bonsangue, Einar Broch Johnsen
Publisher	Springer
Pages	226-241
Number of pages	16
ISBN (Electronic)	978-3-319-30734-3
ISBN (Print)	978-3-319-30733-6
DOIs	https://doi.org/10.1007/978-3-319-30734-3_16
Publication status	Published - 2016
Externally published	Yes

Publication series

Series	Lecture Notes in Computer Science
Volume	9660
ISSN	0302-9743

Series	Theoretical Computer Science and General Issues (LNCS subseries)
Volume	9660

Access to Document

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

Cite this

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, Vol. 9660). (Theoretical Computer Science and General Issues (LNCS subseries), Vol. 9660).

@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",

address = "United States",

}

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. Springer, Lecture Notes in Computer Science, vol. 9660, Theoretical Computer Science and General Issues (LNCS subseries), vol. 9660, 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 (LNCS subseries), Vol. 9660).

Research output: Chapter in Book/Report/Conference proceeding › Chapter › Academic › peer-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, Vol. 9660). (Theoretical Computer Science and General Issues (LNCS subseries), Vol. 9660). Epub 2016 Mar 13. doi: 10.1007/978-3-319-30734-3_16

Effectively Eliminating Auxiliaries

Abstract

Publication series

Access to Document

Other files and links

Fingerprint

Cite this