Title: Automatic Constrained Rewriting Induction towards Verifying Procedural Programs
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.
Publication Year: 2014
Publication Date: 2014-01-01
Language: en
Type: book-chapter
Indexed In: ['crossref']
Access and Citation
Cited By Count: 14
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot