• Return to the Imperial homepage
• Research
• Courses
• Faculties & Departments
• Campus
  Life
• News & Events
• Admin & Services
• About Imperial

Search

People

For:

• Prospective Students
• Students
• Alumni
• Staff
• Business
• Media

 

Cooperatively combining program verifiers: foundations and tool support

Nathaniel Charlton

PhD Thesis

October, 2008

Abstract

Computer science literature abounds with descriptions of program verifiers, systems which analyse a software program and attempt to prove automatically that the program satisfies behavioural specifications. Techniques used include predicate abstraction, three-valued heaps graphs and classes of polyhedra. Yet while these systems have had some encouraging successes, each deals only with particular patterns of program behaviour: e.g. predicate abstraction can infer arithmetical relationships but does not capture the "shape" of linked data structures; for three-valued shape graphs the reverse is true. Thus typical programs, in which different patterns of behaviour are mixed up together, still cannot be verified automatically. This thesis explores the question: "By combining several program verifiers, and making them cooperate, can we produce a verification system that solves a broader range of verification problems than its components do?". Specifically, our approach is to allow the verifiers to exchange information about program states, expressed as formulae of a single common logic, so that each can benefit from the others' findings.

We design a mechanism which enables the verifiers to cooperate. Our setup comprises several verifiers, cleanly separated as analysis modules implementing a common interface, and a central "broker" which oversees the verification process, propagating formulae between the analysis modules. We formalise this approach for programs of a core imperative heap-manipulating language with recursion, annotated with correctness assertions. We give an interprocedural verification algorithm for the broker and soundness conditions for analysis modules, and prove that these ensure the algorithm is sound (though perforce incomplete).

We report on the implementation of our new method in an experimental system HECTOR, which includes the broker and analysis modules for a range of techniques, including predicate abstraction and three-valued shape analysis. By means of a verification case study, we demonstrate some of the advantages of our approach.

PDF of full publication (4.4 megabytes)

(need help viewing PDF files?)

BibT_EX file for the publication

N.B.

Conditions for downloading publications from this site.