[TYPES/announce] Postdoc on Reasoning about program Incorrectness at University College London

[O'Hearn, Peter]

A postdoc is available at UCL, for up to 36 months.

The subject matter is reasoning about program incorrectness or under-approximation, and is based on observations on a mismatch between the foundations of reasoning tools and the way they are deployed in industry. In particular, we hypothesize that interfaces between program components should under-approximate in the failure cases, in order to avoid false positives. This hypothesis is relevant to testing as well as to verification and static analysis, and has been the subject of an initial theory begun by O’Hearn (Incorrectness Logic, see http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/IncorrectnessLogic.pdf).

The objective of this postdoc will be to do fundamental research, looking 2-10 years out, which complements work done in industry. It is expected that mathematical theorems will be proven about prototype program analysers.

Closing date for applications is on 5 Oct. For further information, including how to apply, see

https://www.jobs.ac.uk/job/BVB790/research-fellow-programming-principles-logic-and-verification-group
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20190914/fa8dd5b2/attachment-0001.html>