Verifying Procedural Programs via Constrained Rewriting Induction

Carsten Fuhs, Cynthia Kop, Naoki Nishida

This paper aims to develop a verification method for procedural programs via a transformation into Logically Constrained Term Rewriting Systems (LCTRSs). To this end, we extend tra…