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.si...@ens.fr
_______________________________________________
Haskell mailing list
Haskell@haskell.org
http://www.haskell.org/mailman/listinfo/haskell
