Email Gateway (Nov 14 2021 at 00:16): Email Gateway (Nov 14 2021 at 00:16):From: Giles Reger <giles.reger@manchester.ac.uk>
Hello,
This is an advert for a Research Associate (postdoc) position available for working on data structures for parallel theorem proving.
Closing Date: 23rd Nov
The University of Manchester in the UK has a world-famous automated reasoning group that has produced the award-winning Vampire and iProver theorem provers. This project explores data structures (mainly term indexing structures) within the context of the Vampire theorem prover (https://vprover.github.io/) and will aim to produce (i) thread safe structures, and (ii) specialise structures for particular reasoning use cases.
This project is ideal for somebody who wants to tackle a well-defined, significant problem within automated reasoning.
Salary from £33,309. Should have, or be about to receive, a PhD.
For further details see here
https://www.jobs.manchester.ac.uk/displayjob.aspx?jobid=21224
Note that
(i) Start date is negotiable
(ii) The position could be remote within the UK (UK only for tax reasons) if needed
(iii) There is funding available to extend the position for up to an additional 12 months (depending on start date)
The interested candidate may wish to review the short paper “A Multithreaded Vampire with Shared Persistent Grounding” presented at FMCAD 2021. Video and slides available from FMCAD website. Preprint here: https://easychair.org/publications/preprint/ZDmb. There are many good resources on Term Indexing techniques and their use within theorem proving – the interested candidate should understand what term indexing is!
Last updated: Apr 19 2024 at 12:27 UTC