Postdoctoral position in Program Analysis

Postdoctoral Position in Program Analysis using Satisfiability Modulo Theories, Constrained Horn Clauses, and Symbolic Execution

Are you interested in working with program analysis with the help of Satisfiability Modulo Theories, Constrained Horn Clauses, and Symbolic Execution, with the support of competent and friendly colleagues in an international environment? Are you looking for an employer that invests in sustainable employeeship and offers safe, favourable working conditions? We welcome you to apply for a postdoctoral position at Uppsala University.

The Department of Information Technology holds a leading position in both research and education at all levels. We are currently Uppsala University's third largest department with around 350 employees, including 120 teachers and 120 PhD students. Approximately 5,000 undergraduate students take courses at the department each year. You can find more information about us on the Department of Information Technology website.

Research Topic
Symbolic Execution (SE) is a widely applied method for exploring the behavior of software programs, aiming at the detection of bugs that might affect safety or security or the generation of test inputs. The topic of the postdoctoral position is to develop new techniques for the symbolic execution of programs in dynamic programming languages, in particular in JavaScript, which are often used in security-critical applications. The work will address core challenges when symbolically executing dynamic programs such as the handling of dynamic typing, self-modifying programs and the JavaScript eval function, and the efficient handling of string constraints. The project connects research on symbolic execution with the development of tailor-made techniques for Satisfiability Modulo Theories (SMT), used to reason about constraints in SE, and Constrained Horn Clauses (CHC), used for representing paths and models generated as a side-effect of symbolic execution.

Duties
Research, publication, advising, and possibly teaching in formal methods and program analysis.

Requirements
PhD degree in Computer Science or a foreign degree equivalent to a PhD degree in Computer Science. The degree needs to be obtained by the time of the decision of employment. Priority will be given to applicants who have completed their degree no more than three years before the deadline for applications.  Due to special circumstances, the degree may have been obtained earlier. The three-year period can be extended due to circumstances such as sick leave, parental leave, duties in labour unions, etc.

The candidate should have excellent software implementation skills as the work will include tool development.

Excellent skills in spoken and written English are required. The candidate must clearly document a high degree of self-motivation in the application. In addition, the applicant must be able to work well in a diverse group, comfortable giving and receiving constructive criticism, and have strong abilities for critical thinking and structured work. These competencies are as important as the technical qualifications as they are essential for ensuring a constructive and collaborative work environment.

Additional qualifications
Candidates should have expertise in formal methods and the areas relevant for the planned work: Symbolic Execution, Satisfiability Modulo Theories, Constrained Horn Clauses.

About the employment
The employment is a temporary position of three years according to central collective agreement. Full time position. Starting date April 1 2026 or as agreed. Placement: Uppsala

For further information about the position, please contact: Philipp Ruemmer, +46 768 531787, philipp.ruemmer@it.uu.se.

In this recruitment we have replaced the cover letter with questions that you are asked to answer when making your application. The answers will be used as a part of the selection process.

Please submit your application by the 26th of January 2026, UFV-PA 2026/54.