[ The Types Forum (announcements only),
http://lists.seas.upenn.edu/mailman/listinfo/types-announce ]
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 and can be negotiated. 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 conducted within the Programming Principles,
Logic
and Verification (PPLV) group (http://pplv.cs.ucl.ac.uk/).
Computer Science at UCL was ranked among the top 20 in the world and fifth in
the UK.
The PPLV group provides an exciting research environment, with outstanding
connections
with cutting-edge industry.
Potential applicants are encouraged to contact Prof. Silva
([email protected]) and
Dr. Sammartino ([email protected]) for further information and expressions
of interest.
Applications should be made via the UCL evision website:
https://evision.ucl.ac.uk/urd/sits.urd/run/siw_ipp_lgn.login?process=siw_ipp_app&code1=RRDCOMSING01&code2=0025
Here is a short description of the project.
Title: Automated Black-box Verification of Networking Systems
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 proposed 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.