Invariants from Tests in Boogie; Combining Dynamic and Static Testing Methods to identify Loop Invariants of Boogie Programs

Examensarbete för masterexamen

Please use this identifier to cite or link to this item:
Download file(s):
File Description SizeFormat 
256247.pdfFulltext593.15 kBAdobe PDFView/Open
Type: Examensarbete för masterexamen
Master Thesis
Title: Invariants from Tests in Boogie; Combining Dynamic and Static Testing Methods to identify Loop Invariants of Boogie Programs
Authors: Lapawczyk, Timon
Abstract: Proving implementations with loops against their specifications using automatic verifiers, requires annotations in the form of loop invariants. Loop invariants are properties that must hold for every iteration of a loop and identifying them is generally a difficult endeavour. Invariant inference algorithms can assist this process by generating possible invariants and identifying candidate invariants, using static or dynamic testing. This thesis examines how symbolic execution can compensate for the lack of traditional dynamic testing methods in the context of Boogie programs, to identify candidate invariants for such programs using a combination of dynamic and static testing. Boogie is a verification language that combines a typed logic and a simple procedural language; this combination makes Boogie programs not executable in general, which makes applying dynamic analysis techniques challenging. This thesis implements an algorithm for invariant inference that generates possible invariants from templates and post-conditions. The identification of candidate invariants is split into disproving as many wrong invariants as possible, using the symbolic execution engine Boogaloo, and identifying candidate invariants from the remaining set of invariants, by proving them with the Boogie verifier. A detailed analysis, on 15 carefully selected Boogie programs, shows that the combination of dynamic and static testing can be quite powerful, being able to infer invariants sufficient to prove 10 of the 15 programs correct fully automatically. However, the results also suggests a connection between the kinds of possible invariants that are generated and the impact the symbolic execution has on the performance.
Keywords: Data- och informationsvetenskap;Computer and Information Science
Issue Date: 2018
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.