[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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
