Cookies

We use cookies to ensure that we give you the best experience on our website. By continuing to browse this repository, you give consent for essential cookies to be used. You can read more about our Privacy and Cookie Policy.


Durham e-Theses
You are in:

Program Analysis in A Combined Abstract Domain

HE, GUANHUA (2011) Program Analysis in A Combined Abstract Domain. Doctoral thesis, Durham University.

[img]
Preview
PDF - Accepted Version
1054Kb

Abstract

Automated verification of heap-manipulating programs is a challenging task due to the complexity of aliasing and mutability of data structures used in these programs. The properties of a number of important data structures do not only relate to one domain, but to combined multiple domains, such as sorted list, priority queues, height-balanced trees and so on. The safety and sometimes efficiency of programs do rely on the properties of those data structures. This
thesis focuses on developing a verification system for both functional correctness and memory safety of such programs which involve heap-based data structures.

Two automated inference mechanisms are presented for heap-manipulating programs in this thesis. Firstly, an abstract interpretation based approach is proposed to synthesise program invariants in a combined pure and shape domain. Newly designed abstraction, join and widening
operators have been defined for the combined domain. Furthermore, a compositional analysis approach is described to discover both pre-/post-conditions of programs with a bi-abduction technique in the combined domain.

As results of my thesis, both inference approaches have been
implemented and the obtained results validate the feasibility and precision of proposed approaches. The outcomes of the thesis confirm that it is possible and practical to analyse heap-manipulating programs automatically and precisely by using abstract interpretation
in a sophisticated combined domain.

Item Type:Thesis (Doctoral)
Award:Doctor of Philosophy
Keywords:Program Analysis; Combining Analysis; Fixpoint Analysis; Abstraction; Shape Analysis; Numerical Analysis; Separation Logic
Faculty and Department:Faculty of Science > Engineering and Computing Science, School of
Thesis Date:2011
Copyright:Copyright of this thesis is held by the author
Deposited On:09 Feb 2012 15:45

Social bookmarking: del.icio.usConnoteaBibSonomyCiteULikeFacebookTwitter