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

Visa enkel post
dc.contributor.authorChen, Yuting
dc.contributor.departmentChalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)sv
dc.contributor.departmentChalmers University of Technology / Department of Computer Science and Engineering (Chalmers)en
dc.date.accessioned2019-07-03T13:55:43Z
dc.date.available2019-07-03T13:55:43Z
dc.date.issued2016
dc.description.abstractThe 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.
dc.identifier.urihttps://hdl.handle.net/20.500.12380/238557
dc.language.isoeng
dc.setspec.uppsokTechnology
dc.subjectData- och informationsvetenskap
dc.subjectInformations- och kommunikationsteknik
dc.subjectComputer and Information Science
dc.subjectInformation & Communication Technology
dc.titleReasoning About Loops Over Arrays using Vampire Loop Invariant Generation using a First-Order Theorem Prover
dc.type.degreeExamensarbete för masterexamensv
dc.type.degreeMaster Thesisen
dc.type.uppsokH
local.programmeComputer science – algorithms, languages and logic (MPALG), MSc
Ladda ner
Original bundle
Visar 1 - 1 av 1
Bild (thumbnail)
Namn:
238557.pdf
Storlek:
881.4 KB
Format:
Adobe Portable Document Format
Beskrivning:
Fulltext
Ladda ner
Samling
Examensarbeten för masterexamen