PhD Position on SMT Reasoning at Uppsala University

[Philipp Ruemmer]

======================================================================
--                  PhD Position on SMT Reasoning                   --
--                   Uppsala University, Sweden                     --
======================================================================

Applications are invited for a PhD student position in Computer
Science at Uppsala University, Sweden. The position is partly funded
through a Microsoft Research PhD scholarship, and includes benefits
such as a PhD summer school organised by Microsoft Research Cambridge.
Research will be carried out in the context of a collaboration between
Uppsala University and Microsoft Research Cambridge.

http://www.uu.se/jobb/phd-students/annonsvisning?tarContentId=248331

Information about the position can be given by
   Philipp Rümmer <philipp.ruemmer at it.uu.se>
   Christoph Wintersteiger <cwinter at microsoft.com>

Application deadline is 15 August, 2013.

Subject Area
------------

SMT solvers are constraint solvers that combine highly efficient
reasoning about Boolean logic with decision procedures for domains
like linear arithmetic, bit-vectors, or arrays. SMT solvers form the
backbone of many of today's verification systems, responsible for
discharging verification conditions that encode correctness properties
of hardware or software designs. Other application areas of SMT
solvers include mechanised mathematical reasoning, operations
research, compilation techniques, or malware detection.

Quantifier treatment in SMT is usually implemented by means of
instantiation heuristics. For verification and other applications,
efficient handling of quantifiers has been identified as one of the
main challenges in the development of solvers. The topic of this PhD
research is the extension of the SMT paradigm to the first-order
level, by including quantifiers as first-class citizens in
solvers. This will be done by combining central SMT concepts, in
particular the architecturing of SMT solvers as the combination of
little, domain-specific engines, with techniques developed in the
context of first-order logic, in particular delayed quantifier
instantiation by means of free variables and unification. The research
will partly build on tools previously developed in the Uppsala
University and Microsoft Research, including the theorem provers Z3
and Princess.

Research Environment
--------------------

The Department of Information Technology at Uppsala University has a
leading position in research as well as teaching at all levels. The
Department has about 200 employees, including 80 senior faculty and 80
PhD students. More than 3000 students are enrolled in one or more
courses annually.

Founded in 1991, Microsoft Research has become one of the largest,
fastest-growing, most respected software research organizations in the
world. The Microsoft Research Cambridge branch was set up in July
1997, and today hosts over 100 researchers, mostly from Europe.

Qualifications Required
-----------------------

The candidates should have a Master of Science in Computer Science,
Computer Engineering, or equivalent. Experience in mathematical logic,
automated reasoning, and formal methods are desirable, as are good
implementation skills.

The positions are for a maximum of five years and include departmental
duties at a level of at most 20% (typically teaching) as well as
course studies. You will be expected to teach in Swedish or
English. Excellent skills in spoken and written English are an
absolute requirement.

The department is striving to achieve a more equal gender balance and
female candidates are particularly invited to apply.