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
Cirstea, Corina, Jacobs, B., Moss, L., Reichel, H. and Rutten, J.(eds.) (2001) Semantic constructions for the specification of objects Theoretical Computer Science, 260, (1), pp. 3-25.
Cirstea, Corina, Jacobs, B. and Rutten, J.(eds.) (2002) A coalgebraic equational approach to specifying observational structures Theoretical Computer Science, 280, (1), pp. 35-68.
Cirstea, Corina, (2002) On specification logics for algebra-coalgebra structures: reconciling reachability and observability Nielsen, M. and Engberg, U. (eds.) At Foundations of Software Science and Computation Structures Conference, France. 10 - 12 Apr 2002. , pp. 82-97.
Cirstea, Corina, Reichel, H.(ed.) (2001) Integrating observational and computational features in the specification of state-based, dynamical systems Theoretical Informatics and Applications, 35, (1), pp. 1-29.
Cirstea, Corina, (2003) On expressivity and compositionality in logics for coalgebras Gumm, H.P. (ed.) At 6th International Workshop on Coalgebraic Methods in Computer Science, Poland. 05 - 06 Apr 2003.
Cirstea, Corina, (2002) Institutionalising many-sorted coalgebraic modal logic Moss, L.S. (ed.) At 5th International Workshop on Coalgebraic Methods in Computer Science, France. 06 - 07 Apr 2003.
Cirstea, Corina and Pattinson, Dirk, (2004) Modular Construction of Modal Logics Gardner, Philippa and Yoshida, Nobuko (eds.) At Fifteenth International Conference on Concurrency Theory, United Kingdom. 31 Aug - 03 Sep 2004. , pp. 258-275.
Cirstea, Corina, Gumm, H.P.(ed.) (2004) A compositional approach to defining logics for coalgebras Theoretical Computer Science, 327, (1), pp. 45-69.
Cirstea, Corina, (2004) On Logics for Coalgebraic Simulation Adámek, J. and Milius, S. (eds.) At 7th International Workshop on Coalgebraic Methods in Computer Science, Spain. 27 - 29 Mar 2004. , pp. 63-90.
Yang, Jingtao, Cirstea, Corina and Henderson, Peter (2005) An Operational Semantics for DFM, a Formal Notation for Modeling Asynchronous Web Services At The 5th International Conference on Quality Software (QSIC 2005), Australia. , pp. 446-451.
Yang, Jingtao, Cirstea, Corina and Henderson, Peter (2005) Document Flow Model: A Formal Notation for Modelling Asynchronous Web Services Composition At OnTheMove Workshops, Cyprus. , pp. 39-48.
Cirstea, Corina, Adámek, J and Milius, S(eds.) (2006) A modular approach to defining and characterising notions of simulation Information and Computation, 204, (4), pp. 469-502. (doi:10.1016/j.ic.2005.04.005).
Cirstea, C and Pattinson, D (2007) Modular Construction of Complete Coalgebraic Logics Theoretical Computer Science, 388, pp. 83-108.
Sadrzadeh, Mehrnoosh and Cirstea, Corina, (2006) Relating Algebraic and Coalgebraic Logics of Knowledge and Update van der Hoek, Wiebe, Wooldridge, Michael and Bonanno, Giacomo (eds.) At Logic and the Foundations of Game and Decision Theory. 13 - 16 Jul 2006.
Cirstea, Corina, (2000) An Algebra-Coalgebra Framework for System Specification Reichel, H. (ed.) At 3rd International Workshop on Coalgebraic Methods in Computer Science. , pp. 80-110.
Cirstea, Corina, (1999) A Coequational Approach to Specifying Behaviours Jacobs, B. and Rutten, J. (eds.) At 2nd International Workshop on Coalgebraic Methods in Computer Science. , pp. 142-163.
Cirstea, Corina, (1998) Semantic Constructions for Hidden Algebra Fiadeiro, J.L. (ed.) At 13th International Workshop on Algebraic Development Techniques. , pp. 63-78.
Cirstea, Corina, (1998) Coalgebra Semantics for Hidden Algebra: Parameterised Objects and Inheritance Parisi-Presicce, F. (ed.) At 12th International Workshop on Algebraic Development Techniques. , pp. 174-189.
Cirstea, Corina (2000) Integrating Observations and Computations in the Specification of State-Based, Dynamical Systems University of Oxford, Computing Laboratory, Doctoral Thesis .
Cirstea, Corina, (2006) Modularity in Coalgebra Adámek, J. and Milius, S. (eds.) At 8th International Workshop on Coalgebraic Methods in Computer Science. , pp. 3-26.
Cirstea, Corina and Sadrzadeh, Mehrnoosh, (2007) Coalgebraic Epistemic Update without Change of Model Mossakowski, T. (ed.) At 2nd Conference on Algebra and Coalgebra in Computer Science, Norway. 20 - 24 Aug 2007. , pp. 158-172.
Cirstea, Corina and Sadrzadeh, Mehrnoosh, (2008) Modular Games for Coalgebraic Fixed Point Logics Adámek, Jiri and Kupke, Clemens (eds.) At Coalgebraic Methods in Computer Science 2008. , pp. 71-92.
Cirstea, Corina, Kurz, Alexander, Pattinson, Dirk, Schröder, Lutz and Venema, Yde, (2008) Modal Logics are Coalgebraic Abramsky, Samson, Gelenbe, Erol and Sassone, Vladimiro (eds.) At Visions of Computer Science 2008.
Cirstea, Corina, Kurz, Alexander, Pattinson, Dirk, Schröder, Lutz and Venema, Yde, Sassone, Vladimiro(ed.) (2009) Modal logics are coalgebraic The Computer Journal, 54, (1), pp. 31-41. (doi:10.1093/comjnl/bxp004).
Cirstea, Corina, Kupke, Clemens and Pattinson, Dirk, (2009) EXPTIME Tableaux for the Coalgebraic Mu-Calculus Grädel, Erich and Kahle, Reinhard (eds.) At Computer Science Logic 2009. , pp. 179-193.
Cirstea, Corina, (2010) Generic Infinite Traces and Path-Based Coalgebraic Temporal Logics Jacobs, B.P.F., Niqui, M., Rutten, J.J.M.M. and Silva, A. (eds.) At Coalgebraic Methods in Computer Science 2010. , pp. 83-103.
Cirstea, Corina (2011) Maximal traces and path-based coalgebraic temporal logics [in special issue: CMCS Tenth Anniversary Meeting] Theoretical Computer Science, 412, (38), pp. 5025-5042. (doi:10.1016/j.tcs.2011.04.025).
Cirstea, Corina, (2011) Model checking linear coalgebraic temporal logics: an automata-theoretic approach Corradini, Andrea and Klin, Bartek (eds.) At 2011 International Conference on Algebra and Coalgebra in Computer Science. , pp. 130-144. (doi:10.1007/978-3-642-22944-2_10).
Cirstea, Corina, Seisenberger, Monika and Wilkinson, Toby (eds.) (2012) CALCO Young Researchers Workshop: CALCO-jnr 2011, 29 August 2011: selected papers, Southampton, GB, University of Southampton, 68pp.
Alkhammash, Eman, Salehi Fathabadi, Asieh, Butler, Michael and Cirstea, Corina (2013) Building Traceable Event-B Models from Requirements At Automated Verification of Critical Systems (AVoCS 2013).
Cirstea, Corina (2014) A coalgebraic approach to linear-time logics At 17th International Conference on Foundations of Software Science and Computation Structures, France. 05 - 14 Apr 2014. 15 pp, pp. 426-440.
Alkhammash, Eman, Butler, Michael, Fathabadi, Asieh Salehi and Cîrstea, Corina (2015) Building traceable Event-B models from requirements Science of Computer Programming, 1- 21. (doi:10.1016/j.scico.2015.06.002).
Cirstea, Corina (2015) Canonical coalgebraic linear time logics Leibniz International Proceedings in Informatics (LIPIcs)
Hasuo, Ichiro, Shimizu, Shunsuke and Cirstea, Corina (2015) Lattice-theoretic progress measures and coalgebraic model checking At 43rd Symposium on Principles of Programming Languages, United States. 20 - 23 Jan 2016. 15 pp.
Cirstea, Corina (2016) From branching to linear time, coalgebraically Fundamenta Informaticae, pp. 1-27.
Alkhammash, Eman, Butler, Michael and Cirstea, Corina (2016) Modeling guidelines of FreeRTOS in Event-B At Communication, Management and Information Technology: Proceedings of the International Conference on Communication, Management and Information Technology (Iccmit 2016). , pp. 453-462.