Postdoctoral position in computer science, Munich (Germany)

A position for a research assistant in a DFG project is available.

Project title: Pointers as an abstract data type: complexity-theoretic and programming-language aspects (PURPLE).

Investigators: Martin Hofmann and Ulrich Schöpp

Duration: 36 months

Start date: as soon as possible but not later than June 2011.

Remuneration: German scale 13 TV-L (38k-54k € according to age, experience, family status)

Background: PhD in theoretical informatics with some topical overlap, see project description. Candidates with an excellent Diploma or Master in this area are also encouraged to apply; in this case the project work may lead to a PhD.

Location: The project will be carried out at the Institute for Informatics of Ludwig-Maximilians-Universität Munich, Germany. LMU is an equal opportunities employer.

Applications should be sent by E-Mail to Sigrid Roden roden at tcs.ifi.lmu.de as a single PDF file containing in particular CV, research statement, and the names of two potential referees. There is no deadline. Applications will be assessed on an on-going basis until the position is filled.

Questions about the position can be directed to the investigators {mhofmann, schoepp}@tcs.ifi.lmu.de.

Project description:

In programming languages and logics, graphs and similar data structures are often treated as structured data rather than bit-sequences or words. This means that elements of abstract data structures are often accessed using pointers, which support only a restricted set of operations, such as lookup, update and test for equality. The concrete representation of pointers remains hidden. Traditional computability and complexity theory, on the other hand, rely on concrete representations of data.

In this project we want to explore the expressivity of abstract pointer concepts in the sense of complexity theory. In particular we aim at a separation of programming language versions of LOGSPACE and PTIME. For example, we conjecture that the PTIME-complete problem of Horn-satisfiability cannot be solved with a constant number of abstract pointers, even in the presence of non-determinism or an oracle for reachability.

Additionally, we want to contribute to the formal specification and verification of programs with abstract pointers. For instance, we would like to ascribe rigorous meaning to preconditions like `It makes no guarantees as to the iteration order of the set ...' in the specification of the HashSet class in java.util.

For further background reading, we refer to:

- Project proposal to Deutsche Forschungsgemeinschaft (DFG): http://www2.tcs.ifi.lmu.de/~schoepp/Docs/purple_antrag.pdf

- Martin Hofmann und Ulrich Schöpp. Pure Pointer Programs with Iteration. ACM Transactions on Computational Logic, 2010.

- Martin Hofmann und Ulrich Schöpp. Pointer Programs and Undirected Reachability. Logic in Computer Science (LICS), 2009. Extended version: Electronic Colloquium on Computational Complexity (ECCC) 15(090), 2008