My ongoing research concerns the study of formal verification methodologies that have coalgebraic techniques at their heart. Coalgebras are mathematical structures suitable for modelling a large variety of state-based, dynamical systems; in particular, they can faithfully model software systems, with features such as non-deterministic, stochastic or weighted behaviour being captured in the models. This supports reasoning not just about qualitative aspects of system behaviour (correctness properties), but also about quantitative aspects, including performance analysis (e.g. likelihood of correct behaviour and resource usage). Furthemore, the coalgebraic framework supports a modular approach to modelling systems, and has the potential to deliver compositional verification techniques that (i) apply to a larger class of systems compared to existing techniques and tools and (ii) are more amenable to abstraction and therefore more likely to scale to large/complex systems.
My current work is particularly focused on so-called linear time logics. These are well understood for simple computational models such as transition systems, but their quantitative counterparts, interpreted over more general structures, have not yet been studied in their full generality. I aim to systematically study such logics using coalgebraic machinery, and to develop associated model checking algorithms and tools as part of a modular, coalgebraic approach to system verification.
Towards a Modular Approach to Model-Based Verification: logical, semantical and algorithmic support (EPSRC)
DPhil in Computation (University of Oxford, 2000)
MSc in Computer Science (Babes-Bolyai University, 1993)
Member of 2016 CPHC/BCS Distinguished Dissertations selection panel
Member of IFIP Working Group 1.3
Member of CALCO Steering Committee
Member of CMCS Steering Committee
Organiser of CALCO 2011
Involvement in Program Committes: