Abstract

This paper aims at developing a verification method for procedural programs via a transformation into logically constrained term rewriting systems (LCTRSs). To this end, we adapt existing rewriting induction methods to LCTRSs and propose a simple yet effective method to generalize equations. We show that we can handle realistic functions, involving, e.g., integers and arrays. An implementation is provided.

BibTeX

@inproceedings{CKNN-APLAS14,
  author    = "Cynthia Kop and Naoki Nishida",
  title     = "Automatic Constrained Rewriting Induction towards Verifying
               Procedural Programs",
  booktitle = "Proceedings of the 12th Asian Symposium on Programming
               Languages and Systems",
  editor    = "Jacques Garrigue",
  series    = "Lecture Notes in Computer Science",
  volume    = 8858,
  pages     = "334--353",
  year      = 2014,
  doi       = "10.1007/978-3-319-12736-1_18"
}