Reasoning About Loops Over Arrays using Vampire Loop Invariant Generation using a First-Order Theorem Prover

Examensarbete för masterexamen

Please use this identifier to cite or link to this item: https://hdl.handle.net/20.500.12380/238557
Download file(s):
File Description SizeFormat 
238557.pdfFulltext881.4 kBAdobe PDFView/Open
Type: Examensarbete för masterexamen
Master Thesis
Title: Reasoning About Loops Over Arrays using Vampire Loop Invariant Generation using a First-Order Theorem Prover
Authors: Chen, Yuting
Abstract: The search for automated loop invariants generation has been popularly pursued due to the fact that invariants play a critical role in the verification process. Invariants with quantifiers are particularly interesting for these quantified invariants can be used to express relationships among the elements of array variables and other scalar variables. Automated invariant generation using a first-order theorem prover was first introduced by the work of Kovacs and Voronkov [KV09a] in 2009. This approach employs a theorem prover, in our case the Vampire, as consequences inferencing engine and further to perform the symbol elimination for invariant generation. The entire approach can be separated into two phases: first, by performing static program analysis, one collects a set of static properties as static knowledge about the program and its variables. Second, these properties are sent to Vampire to infer invariants. This novel idea was further developed into a robust implementation introduced by the work of Ahrendt et al. [AKR15]. Our research originated from the idea of enhancing the existing implementation by adding in domain-specific theory. Particularly, we extended the work of Ahrendt et al. [AKR15] with first-order array theory reasoning. Using first-order array theory, we present an extension on the existing automated invariant generation approach by this research. The extension aims at enhancing the reasoning process of automated invariant generation for loop programs over unbounded arrays. In addition to the extension on domain specific theory reasoning, this study also explored the enhancement of the static program analysis phase by proposing new static properties over the indexing variables. Experiment results compared with the previous implementation showed the improvement in reasoning over previously unprovable examples. The improvement came from both domain specific theory reasoning and the newly proposed static property. Our study suggests the inclusion of domain specific theory can enrich the reasoning process of a theorem prover, in our case the first-order theorem prover Vampire. This enhancement can be further applied in program verification purposes such as automated invariant generation and direct proof of correctness. Also, with the theory-specific reasoning, the first-order theorem provers can deliver complex reasoning results containing quantifier alternation. We illustrate our approach on a number of examples coming from program verification.
Keywords: Data- och informationsvetenskap;Informations- och kommunikationsteknik;Computer and Information Science;Information & Communication Technology
Issue Date: 2016
Publisher: Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)
Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers)
URI: https://hdl.handle.net/20.500.12380/238557
Collection:Examensarbeten för masterexamen // Master Theses



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.