====================================================================== -- 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.
Description: This is a digitally signed message part