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:
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), 3-25.
Cirstea, Corina, Jacobs, B. and Rutten, J. (eds.) (2002) A coalgebraic equational approach to specifying observational structures. Theoretical Computer Science, 280, (1), 35-68.
Cirstea, Corina (2002) On specification logics for algebra-coalgebra structures: reconciling reachability and observability. In, Foundations of Software Science and Computation Structures Conference, Grenoble, France, 10 - 12 Apr 2002. Springer, 82-97.
Cirstea, Corina, Reichel, H. (eds.) (2001) Integrating observational and computational features in the specification of state-based, dynamical systems. Theoretical Informatics and Applications, 35, (1), 1-29.
Cirstea, Corina (2003) On expressivity and compositionality in logics for coalgebras. In, 6th International Workshop on Coalgebraic Methods in Computer Science, Warsaw, Poland, 05 - 06 Apr 2003. Elsevier.
Cirstea, Corina (2002) Institutionalising many-sorted coalgebraic modal logic. In, 5th International Workshop on Coalgebraic Methods in Computer Science, Grenoble, France, 06 - 07 Apr 2003. Elsevier.
Cirstea, Corina and Pattinson, Dirk (2004) Modular Construction of Modal Logics. In, Fifteenth International Conference on Concurrency Theory, London, UK, 31 Aug - 03 Sep 2004. Springer, 258-275.
Cirstea, Corina, Gumm, H.P. (eds.) (2004) A compositional approach to defining logics for coalgebras. Theoretical Computer Science, 327, (1), 45-69.
Cirstea, Corina (2004) On Logics for Coalgebraic Simulation. In, 7th International Workshop on Coalgebraic Methods in Computer Science, Barcelona, Spain, 27 - 29 Mar 2004. Elsevier, 63-90.
Yang, Jingtao, Cirstea, Corina and Henderson, Peter (2005) An Operational Semantics for DFM, a Formal Notation for Modeling Asynchronous Web Services. In, The 5th International Conference on Quality Software (QSIC 2005), Melbourne, Australia, IEEE Computer Society, 446-451.
Yang, Jingtao, Cirstea, Corina and Henderson, Peter (2005) Document Flow Model: A Formal Notation for Modelling Asynchronous Web Services Composition. In, OnTheMove Workshops, LNCS 3762, 39-48.
Cirstea, Corina, Orejas, F. (eds.) (2006) An Institution of Modal Logics for Coalgebras. Journal of Logic and Algebraic Programming, 67, (1-2), 87-113.
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), 469-502.
Cirstea, C and Pattinson, D (2007) Modular Construction of Complete Coalgebraic Logics. Theoretical Computer Science, 388, 83-108.
Sadrzadeh, Mehrnoosh and Cirstea, Corina (2006) Relating Algebraic and Coalgebraic Logics of Knowledge and Update. In, Logic and the Foundations of Game and Decision Theory, University of Liverpool, 13 - 16 Jul 2006. University of Liverpool.
Cirstea, Corina (2000) An Algebra-Coalgebra Framework for System Specification. In, 3rd International Workshop on Coalgebraic Methods in Computer Science Elsevier, 80-110.
Cirstea, Corina (1999) A Coequational Approach to Specifying Behaviours. In, 2nd International Workshop on Coalgebraic Methods in Computer Science Elsevier, 142-163.
Cirstea, Corina (1998) Semantic Constructions for Hidden Algebra. In, 13th International Workshop on Algebraic Development Techniques Springer, 63-78.
Cirstea, Corina (1998) Coalgebra Semantics for Hidden Algebra: Parameterised Objects and Inheritance. In, 12th International Workshop on Algebraic Development Techniques Springer, 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. In, 8th International Workshop on Coalgebraic Methods in Computer Science Elsevier, 3-26.
Cirstea, Corina and Sadrzadeh, Mehrnoosh (2007) Coalgebraic Epistemic Update without Change of Model. In, 2nd Conference on Algebra and Coalgebra in Computer Science, Bergen, Norway, 20 - 24 Aug 2007. Springer Verlag, 158-172.
Cirstea, Corina and Sadrzadeh, Mehrnoosh (2008) Modular Games for Coalgebraic Fixed Point Logics. In, Coalgebraic Methods in Computer Science 2008 Elsevier, 71-92.
Cirstea, Corina, Kurz, Alexander, Pattinson, Dirk, Schröder, Lutz and Venema, Yde (2008) Modal Logics are Coalgebraic. In, Visions of Computer Science 2008
Cirstea, Corina, Kurz, Alexander, Pattinson, Dirk, Schröder, Lutz and Venema, Yde, Sassone, Vladimiro (eds.) (2011) Modal logics are coalgebraic. The Computer Journal, 54, (1), 31-41. (doi:10.1093/comjnl/bxp004).
Cirstea, Corina, Kupke, Clemens and Pattinson, Dirk (2009) EXPTIME Tableaux for the Coalgebraic Mu-Calculus. In, Computer Science Logic 2009 Springer, 179-193.
Cirstea, Corina (2010) Generic Infinite Traces and Path-Based Coalgebraic Temporal Logics. In, Coalgebraic Methods in Computer Science 2010 Elsevier, 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), 5025-5042. (doi:10.1016/j.tcs.2011.04.025).
Cirstea, Corina (2011) Model checking linear coalgebraic temporal logics: an automata-theoretic approach. In, 2011 International Conference on Algebra and Coalgebra in Computer Science Springer, 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. In, Automated Verification of Critical Systems (AVoCS 2013)
Cirstea, Corina (2014) A coalgebraic approach to linear-time logics. In, 17th International Conference on Foundations of Software Science and Computation Structures, Grenoble, FR, 05 - 14 Apr 2014. Springer15pp, 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. In, 43rd Symposium on Principles of Programming Languages , St. Petersburg , US, 20 - 23 Jan 2016. 15pp.
Cirstea, Corina (2016) From branching to linear time, coalgebraically. Fundamenta Informaticae, 1-27.
Alkhammash, Eman, Butler, Michael and Cirstea, Corina (2016) Modeling guidelines of FreeRTOS in Event-B. In, Communication, Management and Information Technology: Proceedings of the International Conference on Communication, Management and Information Technology (Iccmit 2016) , 453-462.