PhD studentship: Automated Verification through Coalgebras

Electronic & Software Systems

Location: Highfield Campus

Closing Date:  Monday 31 July 2017

Reference: 867317FP

Funding for: UK Students, EU Students

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

Hours: Full Time

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 a large variety of state-based, dynamical systems, with features such as non-deterministic, stochastic or weighted behaviour being uniformly captured in the models. Coalgebras come with modal and temporal 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 different quantitative verification concerns.

During your PhD, you will help build a synergy between the fields of coalgebraic methods and automated verification, and will publish at internationally leading conferences and journals. 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 model checking techniques, and on the other at extending the applicability of such techniques 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 analyzing the efficiency of resource-management operations; industrial control systems, with a need for energy-aware controller synthesis; and cyber security, with a need for resource-aware reasoning about system-attacker interactions.

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 3 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 current 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 3, to provide a uniform foundation for quantitative synthesis, grounded in coalgebraic modelling.

 References:

• B. Jacobs and J. Rutten, An introduction to (co)algebras and (co)induction. In: D. Sangiorgi and J. Rutten (eds), Advanced topics in bisimulation and coinduction, p.38-99, 2011
• J. J. M. M. Rutten: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249(1): 3-80 (2000)
• C. Cirstea, A Coalgebraic Approach to Quantitative Linear Time Logics,

  arXiv:1612.07844 cs.LO

 Candidate profile

 good undergraduate degree in mathematics or computer science (required),

• interest in theoretical computer science/logic/automated verification (required),
• good programming skills (desirable).

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

 Application process

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