Towards a Dereversibilizer: Fewer Asserts, Statically

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Standard

Towards a Dereversibilizer : Fewer Asserts, Statically. / Reholt, Jonas Wolpers; Glück, Robert; Kruse, Matthis.

Reversible Computation - 15th International Conference, RC 2023, Proceedings. ed. / Martin Kutrib; Uwe Meyer. Springer, 2023. p. 106-114 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13960 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Harvard

Reholt, JW, Glück, R & Kruse, M 2023, Towards a Dereversibilizer: Fewer Asserts, Statically. in M Kutrib & U Meyer (eds), Reversible Computation - 15th International Conference, RC 2023, Proceedings. Springer, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 13960 LNCS, pp. 106-114, 15th International Conference on Reversible Computation, RC 2023, Giessen, Germany, 18/07/2023. https://doi.org/10.1007/978-3-031-38100-3_8

APA

Reholt, J. W., Glück, R., & Kruse, M. (2023). Towards a Dereversibilizer: Fewer Asserts, Statically. In M. Kutrib, & U. Meyer (Eds.), Reversible Computation - 15th International Conference, RC 2023, Proceedings (pp. 106-114). Springer. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) Vol. 13960 LNCS https://doi.org/10.1007/978-3-031-38100-3_8

Vancouver

Reholt JW, Glück R, Kruse M. Towards a Dereversibilizer: Fewer Asserts, Statically. In Kutrib M, Meyer U, editors, Reversible Computation - 15th International Conference, RC 2023, Proceedings. Springer. 2023. p. 106-114. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13960 LNCS). https://doi.org/10.1007/978-3-031-38100-3_8

Author

Reholt, Jonas Wolpers ; Glück, Robert ; Kruse, Matthis. / Towards a Dereversibilizer : Fewer Asserts, Statically. Reversible Computation - 15th International Conference, RC 2023, Proceedings. editor / Martin Kutrib ; Uwe Meyer. Springer, 2023. pp. 106-114 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 13960 LNCS).

Bibtex

@inproceedings{65e895c014fc4f3ab87f1284e92a7fb1,
title = "Towards a Dereversibilizer: Fewer Asserts, Statically",
abstract = "Reversible programming is an unconventional paradigm that offers new ways to construct software. When programs have inherent inverse counterparts, such as compression/decompression, the invertibility of reversible implementations enables a “write once, verify once” approach. The nature of today{\textquoteright}s computers is, however, irreversible. This work-in-progress contribution explores the dereversibilization of reversible source programs into irreversible target programs. As a first step into this space, we explore the use of state-of-the-art Satisfiability-Modulo-Theories (SMT) solvers to statically remove redundant assertions. We divide the problem space into two parts: High-level dereversibilization of Janus-like source programs and classical compilation to machine code. In this contribution, we focus on the semantics-preserving removal of assertions from reversible control-flow statements. Our prototype reduces the size of the assembly code and marks the first step towards automatic dereversibilization and new opportunities of using reversible programs.",
keywords = "Compilation, Program Transformation, Reversible Languages, Satisfiability-Modulo-Theories (SMT) Solver, Static Analysis",
author = "Reholt, {Jonas Wolpers} and Robert Gl{\"u}ck and Matthis Kruse",
note = "Publisher Copyright: {\textcopyright} 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.; 15th International Conference on Reversible Computation, RC 2023 ; Conference date: 18-07-2023 Through 19-07-2023",
year = "2023",
doi = "10.1007/978-3-031-38100-3_8",
language = "English",
isbn = "9783031380990",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "106--114",
editor = "Martin Kutrib and Uwe Meyer",
booktitle = "Reversible Computation - 15th International Conference, RC 2023, Proceedings",
address = "Switzerland",

}

RIS

TY - GEN

T1 - Towards a Dereversibilizer

T2 - 15th International Conference on Reversible Computation, RC 2023

AU - Reholt, Jonas Wolpers

AU - Glück, Robert

AU - Kruse, Matthis

N1 - Publisher Copyright: © 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.

PY - 2023

Y1 - 2023

N2 - Reversible programming is an unconventional paradigm that offers new ways to construct software. When programs have inherent inverse counterparts, such as compression/decompression, the invertibility of reversible implementations enables a “write once, verify once” approach. The nature of today’s computers is, however, irreversible. This work-in-progress contribution explores the dereversibilization of reversible source programs into irreversible target programs. As a first step into this space, we explore the use of state-of-the-art Satisfiability-Modulo-Theories (SMT) solvers to statically remove redundant assertions. We divide the problem space into two parts: High-level dereversibilization of Janus-like source programs and classical compilation to machine code. In this contribution, we focus on the semantics-preserving removal of assertions from reversible control-flow statements. Our prototype reduces the size of the assembly code and marks the first step towards automatic dereversibilization and new opportunities of using reversible programs.

AB - Reversible programming is an unconventional paradigm that offers new ways to construct software. When programs have inherent inverse counterparts, such as compression/decompression, the invertibility of reversible implementations enables a “write once, verify once” approach. The nature of today’s computers is, however, irreversible. This work-in-progress contribution explores the dereversibilization of reversible source programs into irreversible target programs. As a first step into this space, we explore the use of state-of-the-art Satisfiability-Modulo-Theories (SMT) solvers to statically remove redundant assertions. We divide the problem space into two parts: High-level dereversibilization of Janus-like source programs and classical compilation to machine code. In this contribution, we focus on the semantics-preserving removal of assertions from reversible control-flow statements. Our prototype reduces the size of the assembly code and marks the first step towards automatic dereversibilization and new opportunities of using reversible programs.

KW - Compilation

KW - Program Transformation

KW - Reversible Languages

KW - Satisfiability-Modulo-Theories (SMT) Solver

KW - Static Analysis

UR - http://www.scopus.com/inward/record.url?scp=85169029277&partnerID=8YFLogxK

U2 - 10.1007/978-3-031-38100-3_8

DO - 10.1007/978-3-031-38100-3_8

M3 - Article in proceedings

AN - SCOPUS:85169029277

SN - 9783031380990

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 106

EP - 114

BT - Reversible Computation - 15th International Conference, RC 2023, Proceedings

A2 - Kutrib, Martin

A2 - Meyer, Uwe

PB - Springer

Y2 - 18 July 2023 through 19 July 2023

ER -

ID: 368342060