Research Associate on Algorithmic Verification of String-Manipulating Programs

We have a new opportunity for a Research Associate on Algorithmic Verification
of String-Manipulating Programs. Led by Professor Anthony Lin, the project
aims to study fundamental algorithmic issues of automatic verification of
string-manipulating programs and transfer the algorithmic insights into
developing powerful verification and program analysis tools for real-world
programs.



Fundamental algorithmic issues concern decidability, computational complexity,
and expressiveness of constraint languages over the string domain. To apply
the techniques to real-world programs, you will contribute to the development
of an efficient string solver and apply it to string analysis of
Python/JavaScript programs (e.g. by means of symbolic execution and other
methods). Combination of string manipulation with other data types (e.g.
integers) will also be studied in the project.



You will have a doctoral degree (or be close to completion) in computer
science or related fields, together with a strong background in three or more
of the following fields: logic, automata theory, computability/complexity
theory, automated theorem proving, and program analysis. You will also have a
solid understanding of theoretical computer science and is an effective
programmer.



The closing date for applications is 12.00 noon on 22 February 2018.