[isabelle] Post-Doc position with Cliff Jones



We are about to start a four-year project that looks at the links between rely/Guarantee reasoning and Separation Logic. The first pot-doc is to be appointed as soon as possible - after about 6 months, we will be joined by a second post-doc to help with tool construction.

The post-docs will work together with Prof Cliff Jones on the EPSRC-funded project “Taming Concurrency”. The initial research will involve getting completely familiar with both rely/guarantee and separation logic approaches to reasoning about concurrent programs. We will then undertake specifications and designs of many examples with the intention of teasing out the essential contribution that each method makes. The aim is to create a (possibly completely new) approach that is easier to use than the existing methods.


A PhD in Computing Science (or equivalent research experience) is required for the post. You should have experience with “formal methods” in general and specific experience with formalisms used for reasoning about shared variable concurrency (e.g. rely/guarantee method).

Apply via: http://www.ncl.ac.uk/vacancies/

Using reference: D1177R





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.