|
Job summary Applicants are invited to apply for a new position of Research Associate within the “Interface Reasoning for Interacting Systems” (IRIS) project. This is a multi-disciplinary project funded by an EPSRC Programme Grant that brings together researchers from several universities (UCL, LSE, QMUL and Imperial) who are studying a wide range of areas including logic, management science, cyber security, formal verification, automated reasoning,... Job listing information
Key information about the role
Job descriptionJob summaryApplicants are invited to apply for a new position of Research Associate within the “Interface Reasoning for Interacting Systems” (IRIS) project. This is a multi-disciplinary project funded by an EPSRC Programme Grant that brings together researchers from several universities (UCL, LSE, QMUL and Imperial) who are studying a wide range of areas including logic, management science, cyber security, formal verification, automated reasoning, and pure mathematics who are united in this project by a shared interest in the concept of interfaces. The successful applicant will be based at the South Kensington Campus and will jointly join the research groups of Dr John Wickerson in the Department of Electrical and Electronic Engineer and Professor Alastair Donaldson in the Department of Computing, working under their supervision. Donaldson and Wickerson and their research groups have an excellent track record of collaborating on research related to semantics, testing and verification of programming languages for heterogeneous computer systems, and they regularly publish at leading venues in the field such as POPL, PLDI and OOPSLA. We collaborate regularly with other investigators on the IRIS project, and in the context of this position we (and the applicant) will closely work with Dr James Brotherston at UCL, an expert on program logics and logic-based verification. Imperial’s contribution to the IRIS project concentrates on the kind of interfaces that appear in code. Beyond this, we are fairly flexible regarding the precise research topic. Here are three possible topics that the successful candidate could work on, to give an idea of the kind of candidate we are looking for: Possible Topic 1. Prior work has used "litmus testing" to explore the architectural interface that processors provide to programmers. Litmus testing has traditionally been applied to memory consistency models, which describe the semantics of loads/stores to shared memory. A candidate with an interest in computer architecture could explore litmus testing for memory persistency models, which describe the semantics of "non-volatile RAM", which is an emerging technology with substantial implications for programmers. Possible Topic 2. There is an enormous amount of interest at the moment in compilers that interface between software and hardware, e.g. by compiling from C to Verilog. These compilers allow software engineers to harness the power of custom hardware accelerators, such as the "F1" devices recently made available in the cloud by Amazon Web Services. Accordingly, there is an increasing need to improve the reliability of these tools, and we have been investigating how to do this by implementing a formally verified software-to-hardware compiler in Coq. A candidate with an interest in computer-aided proof could contribute to the development of this verified compiler. Possible Topic 3. We've recently developed an operational semantics for programs that execute across CPU/FPGA systems such as Intel's new Xeon+FPGA hybrid chip. With the shift towards more and more heterogeneity in computing devices, these systems are becoming more and more important. Having written down and tested the operational semantics, we can now start to think about reasoning principles above this semantics. A candidate with an interest in program logics could investigate what a Hoare-style logic would look like for these sorts of programs/devices. Duties and responsibilitiesThe post holder will be responsible for conducting research in Electrical Engineering and/or Computer Science. The job requires the candidate to have excellent written and oral communication skills, excellent time management skills and to be able to plan and work independently. The candidate is expected to attend regular meetings with the other members of the IRIS project. Essential requirementsYou must have a PhD in Computer Science or Electrical Engineering (or a related subject), or soon to be awarded your PhD. Further informationFor informal enquiries about the post please contact Dr John Wickerson at j.wickerson@imperial.ac.uk or Professor Alastair Donaldson at alastair.donaldson@imperial.ac.uk.
|
