About the project
This project will make advances to the areas of automated verification and synthesis, by generalising existing techniques to match the complexity of modern software agents. Application domains include the synthesis of autonomous systems and automated planning with formal guarantees of correctness/optimality.
The area of coalgebraic verification aims to employ methods from the field of coalgebra in order to enhance and extend the applicability of automated verification and synthesis techniques.
Coalgebras are mathematical structures suited for modelling general state-based, dynamical systems. They come equipped with logics that support reasoning about temporal behaviour, both qualitatively and quantitatively. Coalgebraic techniques have already helped to better understand, unify and even generalise automata-based techniques used in automated verification.
Current limitations of automated verification and synthesis techniques include the lack of applicability to systems whose structure and interactions vary over time, and/or whose optimality requirements are complex (e.g.~optimal resource usage in a stochastic environment). This project will advance the coalgebraic approach to verification by addressing some of these limitations.
The School of Electronics and Computer Science is committed to promoting equality, diversity inclusivity as demonstrated by our Athena SWAN award. We welcome all applicants regardless of their gender, ethnicity, disability, sexual orientation or age, and will give full consideration to applicants seeking flexible working patterns and those who have taken a career break. The University has a generous maternity policy, onsite childcare facilities, and offers a range of benefits to help ensure employees’ well-being and work-life balance. The University of Southampton is committed to sustainability and has been awarded the Platinum EcoAward.
