PhDtopics

From PLSwiki

Some Possible Ph.D. topics within the PLS group

Bigraphical Programming Languages:

In the Bigraphical Programming Languages group, we research the design of models and programming languages based on the theory of bigraphs. The aim is to obtain models and programming languages that are (1) practically well-suited for applications in ubiquituous computing and (2) amenable to formal reasoning. Possible Ph.D. topics include investigations into context-awareness and bigraphical models; applications of bigraphs to systems biology and model-driven software engineering; development of tool support for (semi-)automatic verification of properties of bigraphical models; and extensions to the theory of bigraphs, e.g. type systems and quantitative analysis.

Modular Reasoning about Software:

The goal of our research on modular reasoning about software is to develop theories and methods for modular reasoning about software written in modern programming languages. The purpose is to lay the foundation for improvement of software tools, which are being and will be developed over the next five to ten years and which will be used to improve software practice. Possible Ph.D. topics include modular reasoning about shared heap objects (e.g., using variants of higher-order separation logic), parametricity for low-level code, and modular reasoning about higher-order store.

Tools and Methods for Scalable Software Verification:

The goal of this research project is to develop tools for practical verification of modern object-oriented software written in Java / C#. The project will be based on earlier developments in separation logic to reason about shared heap objects and on static analysis techniques, in particular abstract interpretation. Possible Ph.D. topics include developments of separation logic for reasoning about delegates, generics and inheritance; specification and verification of the C5 collection library; development and implementation of tools based on abstract interpretation.

Logical Frameworks:

The logical framework group is concerned with the development and implementation of meta-languages for advanced data structures as well as tools for programming with and reasoning about them. Those data structures include not only lists and trees (including abstract syntax trees) but also more complex data structures for the meaning of programs and the meaning of mathematical proofs. The main activities of the group focus on the development of the Twelf proof assistant, the functional programming language Delphin, digital libraries for mathematical knowledge, meta logics for LF and LLF, proofs by logical relations, logic programming, proof planning by proof abstraction, and complexity analysis of logic programs. A small but by no means complete list of ideas for doctoral theses include the meta theory of concurrent systems (such as CLF), meta reasoning by coinduction, disproving false conjectures, and complexity analysis of CLF programs.

Concurrency and Mobility

The concurrency and mobility group at ITU is researching operational and denotational semantics of concurrent and mobile processes and applications within security, web-services, business processes and workflow. The research is founded in the theory of process calculi, types, categorical models for concurrency and verification. Currently there is one or more vacant PhD scholarships in types for context-sensitive services. The scholarships are affiliated to the FIRST PhD school (www.first.dk) and the Jingling Genies project (http://sites.google.com/site/jinglinggenie/). The aim of the PhD projects is to develop a theory of types for context-sensitive services and thereby expand the limits of research in session types for communication-based computing and formal models for specifying context and contracts for web-services, as well as technologies and standards for describing web-service interfaces, contracts, and their context.

Contact Associate professor Thomas Hildebrandt or Associate professor Arne J. Glenstrup for more information.