In English

Incremental Deductive Verification for a subset of the Boogie language

Leo Anttila ; Mattias Åkesson
Göteborg : Chalmers tekniska högskola, 2017. 51 s.
[Examensarbete på avancerad nivå]

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.

Nyckelord: Computer science, formal verification, deductive verification, boogie, incremental verification, verification, sidecar



Publikationen registrerades 2017-09-04. Den ändrades senast 2017-09-04

CPL ID: 251609

Detta är en tjänst från Chalmers bibliotek