Incremental Deductive Verification for a subset of the Boogie language
Ladda ner
Typ
Examensarbete för masterexamen
Master Thesis
Master Thesis
Program
Computer science – algorithms, languages and logic (MPALG), MSc
Publicerad
2017
Författare
Anttila, Leo
Åkesson, Mattias
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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.
Beskrivning
Ämne/nyckelord
Data- och informationsvetenskap , Computer and Information Science