PhD studentship in Automated Verification through Coalgebras, Southampton (UK)

PhD studentship: Automated Verification through Coalgebras

Qualification type: PhD

Location: Southampton

Funding for: UK Students, EU Students

Funding amount: The funding covers EU/UK fees and stipend in line with EPSRC rates

Hours: Full Time

Start date: October 2018

Project Description

As part of this project, you will work on developing new foundations for quantitative verification, grounded in the theory of coalgebras.

Coalgebras are mathematical structures suited for modelling general state-based, dynamical systems, with features such as non-deterministic, stochastic or weighted behaviour being uniformly captured in the models. Coalgebras come equipped with modal logics that expressively support reasoning about the temporal behaviour of dynamical systems, both qualitatively and quantitatively. Owing to the diversity of semantic models that can be captured, coalgebra is the ideal framework for modelling and reasoning about heterogeneous systems whose components have varied quantitative verification concerns.

During your PhD, you will help build a synergy between the fields of coalgebra verification, and will publish at internationally leading conferences. Your project will contribute to the development of a new research area of coalgebraic model checking, aimed on the one hand at unifying existing quantitative verification techniques, and on the other at extending their applicability to complex systems, whose modelling requires a variety of underlying models. Application areas for such techniques include, but are not limited to: cloud computing, with a need for analysing the efficiency of resource-management operations; cyber security, with a need for resource-aware reasoning about system-attacker interactions; and autonomous systems, with a need for on-the-fly synthesis of resource-optimal plans.

You will work on one or more of the following topics:

- Generic algorithms for quantitative verification.

You will build on recent work on quantitative coalgebraic linear time logics and study automata-theoretic model checking algorithms for these logics. This work will be inspired by existing algorithms for specific model types, but it will be driven by a coalgebraic perspective on modelling and reasoning about systems, allowing several model types to be treated uniformly.

- Compositional verification of complex systems.

You will develop a compositional approach to modelling and verifying complex, heterogeneous systems, along with a general theory of quantitative, verification-driven abstractions, to allow model checking to scale from individual components to heterogeneous systems of interacting components, as demanded by modern applications.

- Quantitative synthesis using coalgebras.

You will build on existing work on quantitative synthesis, as well as on recent work on quantitative coalgebraic linear time logics, to provide a uniform foundation for quantitative synthesis, grounded in coalgebraic modelling.

Candidate profile

- good undergraduate degree in mathematics or computer science

- interest in theoretical computer science/logic/automated verification

- good programming skills (desirable).

For further details about the project, please contact Dr Corina Cirstea (cc2 at ecs.soton.ac.uk).

Application process

To apply, please email your CV, transcript of your degree and a brief research statement to: cc2 at ecs.soton.ac.uk . If your application is shortlisted, you will be invited to an interview (this may be via Skype/phone).

Application deadline: 31 May 2018 (but the position may be filled early if a suitable candidate is found).