[TYPES/announce] PhD studentship in formal methods & verification at University College London

[Matteo Sammartino]

Applications are invited for a PhD studentship at University College London, under the supervision of Prof. Alexandra Silva and Dr. Matteo Sammartino.

The start date is flexible. It should be in September 2018 at the latest.

The studentship is funded by the UK Research Institute in Verified Trustworthy Software Systems, and will be carried out within the Programming Principles, Logic and Verification (PPLV) group (http://pplv.cs.ucl.ac.uk/). The PPLV group offers an exciting research environment, with outstanding connections with cutting-edge industry.

Potential applicants are encouraged to contact Prof. Silva (alexandra.silva at ucl.ac.uk) and Dr. Sammartino (m.sammartino at ucl.ac.uk) for further information and expressions of interest.
Applications should be made via the UCL evision system:

https://evision.ucl.ac.uk/urd/sits.urd/run/siw_ipp_lgn.login?process=siw_ipp_app&code1=RRDCOMSING01&code2=0025


=================== PROJECT DESCRIPTION ===================

Our society is increasingly reliant on complex networking systems, consisting of several components that operate in a distributed/concurrent fashion, exchange data that may be highly sensitive, and are implemented with a mix of open and closed-source code. Examples are Software Defined Networks, cloud computing systems, Internet of Things and others. 

As the complexity of these systems increases, there is a pressing need of methods and tools to automatically verify security and privacy properties. High quality models – able to express all the behaviours of interest – are of paramount importance to this aim. However, it is often the case that the task of building a model is performed by humans and in a short span of time – if it is performed at all – and as such can be error-prone and inaccurate. 

The goal of the PhD project is to develop techniques and tools to automate the modelling and verification of networking software systems. The novel idea is to rely on the model learning paradigm, originally proposed in artificial intelligence, to automatically build an automaton model of a running system in a black-box fashion -- purely via interactions with the running system.