SCorCH is looking to hire a postdoctoral research associate in the areas listed below. Information on how to apply will be made available shortly and initial queries and expressions of interest can be directed to Dr Giles Reger.

In all cases we are looking for candidates with a track record of publication and experience putting research into practice through the development of tools. Given the setting, we are also keen to find canditates comfortable with the C ecosystem and the related systems and architectural concepts related to the CHERI project.

Given the current environment, we anticipate that roles will begin remotely for as long as necessary.

Model Checking. We are looking for two candidates to work on extensions to the CBMC and/or ESBMC software model checkers to (i) support the capability hardware setting, and (ii) improve their scalability and applicability. The ideal candidate will have experience with software model checking but we are also interested in experience with fuzzing, symbolic execution, or abstract interpretation techniques.

Runtime Verification/Dynamic Analysis. We are looking for a candidate to work on dynamic analysis of compartmentalisation properties. The project will involve aspects of runtime verification, automated instrumentation, program synthesis, and dynamic symbolic execution. The ideal candidate will have rRelevant experience in one or more of those areas.

Automated Reasoning/Hardware Model Checking . We are looking for a candidate to work on (i) theory reasoning extensions in the Vampire or iProver theorem provers, and (ii) applications of those extensions within hardware model checking. The ideal candidate will have strong theoretical knowledge of first-order logic and theories, as well as pragmatic experience developing or working with theorem provers or SMT solvers.