Redundancy Checking in Reversible Flowcharts via Logic-Based Operational Semantics

This study addresses the problem of detecting redundant assertions in reversible programs. We investigate an interpretive method for the automatic verification of assertion redundancy by checking satisfiability of Constrained Horn Clauses (CHCs), a fragment of first-order logic. By formalizing a transition semantics of reversible flowcharts in CHC and using well-known examples, including Dijkstra’s permutation-to-code algorithm, we show that standard techniques and tools developed in the field of CHC-based verification appear suitable for addressing this unconventional optimization problem. The scalability of the approach may be achieved through techniques such as CHC specialization and abstract interpretation.