Towards a dereversibilizer: fewer asserts, statically

DOI10.1007/978-3-031-38100-3_8MaRDI QIDQ6148113

Matthis Kruse, Jonas Wolpers Reholt, Robert Glück

Publication date: 11 January 2024

Published in: Reversible Computation (Search for Journal in Brave)

zbMATH Keywords

static analysisprogram transformationcompilationreversible languagessatisfiability-modulo-theories (SMT) solver

Mathematics Subject Classification ID

Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.) (68Q10) Quantum computation (81P68) Other nonclassical models of computation (68Q09)

Cites Work

• Unnamed Item
• Fundamentals of reversible flowchart languages
• Effective use of SMT solvers for program equivalence checking through invariant-sketching and query-decomposition
• Encryption and reversible computations. Work-in-progress paper
• Optimizing reversible programs
• Infinite-state invariant checking with IC3 and predicate abstraction
• Reversible computing from a programming language perspective
• Horn Clause Solvers for Program Verification
• Dafny: An Automatic Program Verifier for Functional Correctness
• RSSA: A Reversible SSA Form
• Simplification by Cooperating Decision Procedures
• Analysis and Transformation of Constrained Horn Clauses for Program Verification

This page was built for publication: Towards a dereversibilizer: fewer asserts, statically