cl-banner

Automatic Constrained Rewriting Induction towards Verifying Procedural Programs

Cynthia Kop and Naoki Nishida

Proceedings of the 12th Asian Symposium on Programming Languages and Systems (APLAS 2014), Lecture Notes in Computer Science 8858, pp. 334 – 353, 2014.

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.

 

  PDF |    doi:10.1007/978-3-319-12736-1_18  |  © Springer International Publishing Switzerland

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"
}
Nach oben scrollen