Incremental Deductive Verification for a subset of the Boogie language

Examensarbete för masterexamen

Please use this identifier to cite or link to this item:
Download file(s):
File Description SizeFormat 
251609.pdfFulltext720.62 kBAdobe PDFView/Open
Type: Examensarbete för masterexamen
Master Thesis
Title: Incremental Deductive Verification for a subset of the Boogie language
Authors: Anttila, Leo
Åkesson, Mattias
Abstract: As computer programs and systems get larger and more complex, the conventional method of ensuring system correctness by feeding it input data and analyzing the output becomes harder and more time consuming, since the space of possible input data becomes nearly infinite. Formal verification is a method of proving the correctness of a software or hardware system in accordance to a formal specification of its intended behavior, proposed as a complement to regular testing to increase the accuracy of detection of bugs in a system. An issue with formal verification today is its scalability. The SMT-problem is known to be at least NP-hard, thus the time required to verify a program increases rapidly as programs get larger. This thesis presents the design, implementation and evaluation of an incremental deductive verifier for a subset of the intermediate verification language Boogie. The technique is intended to speed up the verification of a program when moving between different iterations by identifying and re-verifying only those parts of the program that are affected by the modifications made since the last verification. This reduces the size of the input to the SMT-solver and can therefore help mitigate the issue of scalability in the verification process. The verifier is evaluated by running it on a set of test programs, each with multiple versions to simulate realistic software development, with incrementality turned on or off. The results show promise for the technique with the majority of tests showing considerable time save with up to 15-49% time saved for most programs with three iterations when solved incrementally compared to non-incrementally, and increased number of iterations generally lead to further time savings.
Keywords: Data- och informationsvetenskap;Computer and Information Science
Issue Date: 2017
Publisher: Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)
Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers)
Collection:Examensarbeten för masterexamen // Master Theses

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