ORA Thesis: "Program analysis with interpolants" - uuid:6987de8b-92c2-4309-b762-f0b0b9a165e6




Links & Downloads


Reference: Georg Weißenbacher, (2010). Program analysis with interpolants. DPhil. University of Oxford.

Citable link to this page: http://ora.ox.ac.uk/objects/uuid:6987de8b-92c2-4309-b762-f0b0b9a165e6
Title: Program analysis with interpolants

Abstract: This dissertation discusses novel techniques for interpolation-based software model checking, an approximate method which uses Craig interpolation to compute invariants of programs. Our work addresses two aspects of program analyses based on model checking: verification (the construction of correctness proofs for programs) and falsification (the detection of counterexamples that violate the specification). In Hoare's calculus, a proof of correctness comprises assertions which establish that a program adheres to its specification. The principal challenge is to derive appropriate assertions and loop invariants. Contemporary software verification tools use Craig interpolation (as opposed to traditional predicate transformers such as the weakest precondition) to derive approximate assertions. The performance of the model checker is contingent on the Craig interpolants computed. We present novel interpolation techniques which provide the following advantages over existing methods. Firstly, the resulting interpolants are sound with respect to the bit-level semantics of programs, which is an improvement over interpolation systems that use linear arithmetic over the reals to approximate bit-vector arithmetic and/or do not support bit-level operations. Secondly, our interpolation systems afford us a choice of interpolants and enable us to fine-tune their logical strength and structure. In contrast, existing procedures are limited to a single ad-hoc choice of an interpolant. Interpolation-based verification tools are typically forced to refine an initial approximation repeatedly in order to achieve the accuracy required to establish or refute the correctness of a program. The detection of a counterexample containing a repetitive construct may necessitate one refinement step (involving the computation of additional interpolants) for each iteration of the loop. We present a heuristic that aims to avoid the repeated and computationally expensive construction of interpolants, thus enabling the detection of deeply buried defects such as buffer overflows. Finally, we present an implementation of our techniques and evaluate them on a set of standardised device driver and buffer overflow benchmarks.

Digital Origin:Born digital
Type of Award:DPhil
Level of Award:Doctoral
Awarding Institution: University of Oxford
About The Authors
institutionUniversity of Oxford
facultyMathematical,Physical & Life Sciences Division - Computing Laboratory
oxfordCollegeMagdalen College
Dr Daniel Kroening More by this contributor
Bibliographic Details
Issue Date: 2010
Copyright Date: 2010
Urn: uuid:6987de8b-92c2-4309-b762-f0b0b9a165e6
Item Description
Member of collection : ora:thesis
Alternate metadata formats
Copyright Holder: Georg Weissenbacher
Terms of Use: Click here for our Terms of Use