Dear all, The chair II for computer science at the Technical University Munich is offering two PhD positions in the area of program analysis. The first position ("low-level analysis") is centered around defining an implementing an analysis of x86 assembler code and, in particular, of concurrency constructs. The second position ("high-level analysis") is geared towards the analysis of data structures (aka shape analysis) using numeric invariants. The intention is to extend an existing analyzer that performs a forward-reachability analysis with the aim to prove the absence of memory management errors and other defects in legacy C software. This analyzer is written in Haskell. first position: low-level analysis ---------------------------------- Most program analysis tools operate on the source code, usually C, since information on variable types, data structures and basic blocks is not available in the executable. One problem with this approach is the definition of the exact semantics of C source code as many constructs commonly found in hand-written programs are ``implementation-dependent'' or even ``undefined'' according to the C standard. These uncertainties are exacerbated when analyzing programs that make use of concurrency constructs. The goal is therefore to directly analyze the resulting x86 machine code and to reconstruct the control flow graph and data structures on-the-fly. The analysis of concurrent programs moreover requires that (abstract) states are propagated between different threads. The challenge here lies in storing a minimum number of abstract states (to reduce the memory requirements) and to get away with a minimum amount of propagation between threads. ------------------------------------- second position: high-level analysis ----------------------------------- One recurring challenge in analysing programs is the precise summarization of data structures. This so-called shape analysis commonly uses logic formulae (e.g. separation logic) to describe a data structure contained in a memory region. In this approach, a predicate must be present that describes the invariant (e.g. "list(p)" might mean that p points to a memory region containing a singly-linked list). If no predicate is available that matches the data structure that is being built by a program, the logic formula must be discarded in order to ensure termination, thereby discarding both, the shape of a memory region and the information on how it is connected to other memory regions. The goal of this position is to find novel abstractions that infer the shape of a memory region and its connection to other memory regions separately. The connection to other memory regions are then annotated with numeric variables that denote how many memory regions are reachable via the connection. The values of these variables is then tracked separately, allowing a more graceful loss of precision. am only the numeric information needs to be relaxed since number of different shapes is fixed by the structure of the program. ------------------------------------- Both positions are fully funded for 4 years and do not come with any teaching duties. The PhD students may start as soon as January 1, 2010. The salary is TVL E13 (about 2900 EUR/1650 EUR per month). The positions are part of the Emmy Noether Programme "Verifying Legacy C Programs using Numeric Domains" which is headed by Axel Simon. This project, in turn, is located within the chair of Helmut Seidl. The PhD students will be supervised by Axel Simon. What you should provide: - Master (or equivalent) degree in Computer Science or Maths - good programming skills - an interest in compiler construction, program optimization and the like - not afraid of discrete maths, lattices etc. - good writing skills in English and Haskell - an electronic application including detailed CV by December 1 (later applications may not be considered) Contact: Please send applications and any enquiries to: Axel.Simon@ens.fr