The following PhD projects offer opportunities for research ranging from purely theoretical work to implementation-based work. The projects are examples, I am happy to discuss other ideas for PhD topics.
GP is a rule-based, nondeterministic programming language for solving graph problems at a high level of abstraction, freeing programmers from dealing with low-level data structures. GP's design aims at syntactic and semantic simplicity, to facilitate formal reasoning about programs. The language contains just four control constructs (rule application, sequential composition, branching and looping), has a simple formal semantics, and is computationally complete.
Speeding up GP. This project will attempt to speed up GP's current implementation, which is based on a compiler and the York abstract machine [1,2], to rival with the fastest graph transformation tools currently available [3]. Activities to make GP faster include the introduction of a powerful type system for graphs to support the analysis of graphs at run time, the implementation of dynamic search plans for graph pattern matching, and the use of so-called rooted graph transformation rules which can be matched in constant time.
Static analysis of graph programs. This project will develop an automatic program analysis for detecting confluence and termination in graph programs. A nondeterministic program is confluent (or 'don't care' nondeterministic) if all its executions on a given input will produce the same result. Confluence is essential for run time efficiency because GP's backtracking mechanism [1] can be turned off for confluent subprograms without compromising the semantics. Sufficient conditions for confluence will be developed by generalizing so-called critical pair techniques [4] from sets of graph transformation rules to programs. A simple static analysis of termination will complement the analysis of confluence.
Verification of graph programs. Currently, correctness proofs for GP programs are done ad hoc rather than in a formal calculus [5,6]. This project will develop a Hoare-like calculus in which correctness proofs for GP programs can be carried out rigorously. This requires a sufficiently powerful logic for expressing graph properties, proof rules for GP's control constructs, and a theory showing that these rules are sound with respect to the semantics [7]. A completeness result for the calculus would be desirable, too. To make the calculus practical, it could be implemented in a proof assistant such as Coq or Isabelle.
The type systems of current imperative programming languages are too weak to detect non-trivial pointer errors which violate the shapes of linked data structures such as cyclic lists, balanced trees, etc. The goal is to provide powerful 'shape types' by which programmers can specify and manipulate pointer structures, together with a static analysis which guarantees that pointer programs preserve shapes [8,9].
Theory and practice of shape types. The experimental language C-GRS extends C with shape types, it comes with a translation to standard C and an abstraction algorithm that allows shape types to be checked for shape-safety [10,11].This project will extend the scope of the shape checking-algorithm and also implement tools for visualising and testing shape types. More on the theoretical side, the project should attempt to clarify the relationship between the C-GRS approach and logic-based approaches to shape safety.