Doctor of Philosophy / Department of Computing and Information Sciences / David A. Schmidt / We are interested in modular static analysis to analyze softwares automatically. We
focus on programs with data structures, and in particular, programs with pointers. The
final goal is to find errors in a program (problems of dereferencing, aliasing, etc) or to prove
that a program is correct (regarding those problems) in an automatic way.
Isthiaq, Pym, O'Hearn and Reynolds have recently developed separation logics, which
are Hoare logics with assertions and predicates language that allow to prove the correctness
of programs that manipulate pointers. The semantics of the logic's triples ({P}C{P'}) is
defined by predicate transformers in the style of weakest preconditions.
We expressed and proved the correctness of those weakest preconditions (wlp) and
strongest postconditions (sp), in particular in the case of while-loops. The advance from
the existing work is that wlp and sp are defined for any formula, while previously existing
rules had syntactic restrictions.
We added fixpoints to the logic as well as a postponed substitution which then allow to
express recursive formula. We expressed wlp and sp in the extended logic and proved their
correctness. The postponed substitution is directly useful to express recursive formula. For
example, [equations removed, still appears in abstract]
describes the set of memory where x points to a list of integers.
Next, the goal was to use separation logic with fixpoints as an interface language for
pointer analysis. That is, translating the domains of those analyses into formula of the
logic (and conversely) and to prove their correctness. One might also use the translations
to prove the correctness of the pointer analysis itself.
We illustrate this approach with a simple pointers-partitioning analysis. We translate
the logic formula into an abstract language we designed which allows us to describe the
type of values registered in the memory (nil, integer, booleans, pointers to pairs of some
types, etc.) as well as the aliasing and non-aliasing relations between variables and locations in the memory. The main contribution is the definition of the abstract language and
its semantics in a concrete domain which is the same as the one for the semantics of formula. In particular, the semantics of the auxiliary variables, which is usually a question
of implementation, is explicit in our language and its semantics. The abstract language is
a partially reduced product of several subdomains and can be parametrised with existing
numerical domains. We created a subdomain which is a tabular data structure to cope with
the imprecision from not having sets of graphs. We expressed and proved the translations
of formula into this abstract language.
| Identifer | oai:union.ndltd.org:KSU/oai:krex.k-state.edu:2097/506 |
| Date | January 1900 |
| Creators | Sims, Elodie-Jane |
| Publisher | Kansas State University |
| Source Sets | K-State Research Exchange |
| Language | en_US |
| Detected Language | English |
| Type | Dissertation |
Page generated in 0.0023 seconds