The Department of Computer Science at the University of Manchester (UK) seeks one Research Associate (RA) position to work on Automated Verification of CHERI C++ Programs. This RA position is full-time for two years, starting after October 1st, 2021, ideally January 1st, 2022.
With its focus on real-world security through cutting-edge Digital Security by Design (DSbD) technology, this position is a unique opportunity to make a real impact, advance state-of-the-art in applied software verification research, and join a top-class team of collaborators. The role also offers an outstanding opportunity for career development that is equally well-suited to an academic or industrial research path or subsequent work as a software verification engineer in the industry.
You will be a member of the Soteria team, working closely with Dr. Lucas Cordeiro, Dr. Giles Reger, and Dr. Konstantin Korovin at the University of Manchester. The ideal candidate will research and apply novel formal software verification methods on components of innovative DSbD technology being developed in the project. In particular, we will extend the Efficient SMT-based bounded model checking (ESBMC) tool with a Clang C++ frontend, new operational models reflecting the Morello architecture, new analyses for the modified notion of memory safety and compartmentalization requirements, and further extensions to improve their applicability in the industrial context.
● Have, or be about to obtain, a Ph.D. in a relevant area
● Excellent knowledge in at least one of the following areas
○ Compiler design
○ Bounded Model Checking
○ Runtime Verification
○ Dynamic Symbolic Execution/Abstract Interpretation
○ Automated Reasoning/First-order Theorem Proving
● Strong coding skills (C/C++)
● Excellent communication and interpersonal skills
● Ability and willingness to work closely with industry
● Ability to work independently and as part of a team
● Ability to present in both written and oral publications
● A track record of high-quality publications
● Previous implementation experience with a formal analysis tool
● Knowledge and experience of compilers
● Understanding of the Arm Morello architecture
● Expertise in the Arm architecture
Applications must be sent via:
Deadline: August 8th, 2021.
*Enquiries about the vacancy, shortlisting, and interviews:
Name: Dr. Lucas Cordeiro
This vacancy will close for applications at midnight on the closing date.