The University of Southampton
×
Electronics and Computer Science
Telephone:
+442380593625
Email:
cc2@ecs.soton.ac.uk

Dr Corina Cirstea 

Personal homepage

Programme Leader for the BEng/MEng in Software Engineering undergraduate courses.

Dr Corina Cirstea is an Associate Professor in the Agents, Interaction and Complexity research group in the School of Electronics and Computer Science at the University of Southampton. She holds a DPhil in Computation from the University of Oxford (2000) and was the holder of a Junior Research Fellowship in Computer Science at St. John's College Oxford (1999-2003) prior to joining the University of Southampton. Her research interests are in logic and models of computation, more specifically in coalgebras, their close connection to modal logics, and their applications to automated verification.

External activities

Member of editorial board, Compositionality journal

Co-chair of IFIP Working Group 1.3

Member of CALCO Steering Committee

Member of CMCS Steering Committee

Program Committees:

Research

Research interests

Dr Cirstea's research concerns the study of automated verification and synthesis techniques that have coalgebras at their heart. Coalgebras are mathematical structures suitable for modelling a large variety of state-based, dynamical systems; in particular, they can faithfully model both software and hardware systems, with features such as non-deterministic, stochastic or resource-aware behaviour being captured in the models. This supports reasoning not just about qualitative aspects of system behaviour (correctness guarantees), but also about quantitative ones (e.g. likelihood of correct behaviour and guarantees on resource usage).

Dr Cirstea is the PI on the Leverhulme Trust Research Project Grant COVER: COalgebraic foundations for quantitative VERification (2021-2024, joint with the University of Strathclyde). This project aims to develop new foundations for quantitative model checking and synthesis, grounded in coalgebra, and thereby widen the applicability of automated verification to complex systems with a range of correctness and optimality guarantees. 

Teaching

Modules taught (2021-22):

  • COMP1201 Algorithmics (Part 1, module leader)
  • COMP2210 Theory of Computing (Part 2, module leader)
  • COMP6210 Automated Software Verification (Part 4/MSc, module leader)

Publications

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. Nielsen, M. and Engberg, U. (eds.) Foundations of Software Science and Computation Structures Conference, Grenoble, France. 09 - 11 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), 1-29.

Cirstea, Corina (2003) On expressivity and compositionality in logics for coalgebras. Gumm, H.P. (ed.) 6th International Workshop on Coalgebraic Methods in Computer Science, Warsaw, Poland. 04 - 05 Apr 2003.

Cirstea, Corina (2002) Institutionalising many-sorted coalgebraic modal logic. Moss, L.S. (ed.) 5th International Workshop on Coalgebraic Methods in Computer Science, Grenoble, France. 05 - 06 Apr 2003.

Cirstea, Corina and Pattinson, Dirk (2004) Modular Construction of Modal Logics. Gardner, Philippa and Yoshida, Nobuko (eds.) Fifteenth International Conference on Concurrency Theory, London, United Kingdom. 30 Aug - 02 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), 45-69.

Cirstea, Corina (2004) On Logics for Coalgebraic Simulation. Admek, J. and Milius, S. (eds.) 7th International Workshop on Coalgebraic Methods in Computer Science, Barcelona, Spain. 27 - 28 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. The 5th International Conference on Quality Software (QSIC 2005), Melbourne, Australia. pp. 446-451 .

Yang, Jingtao, Cirstea, Corina and Henderson, Peter (2005) Document Flow Model: A Formal Notation for Modelling Asynchronous Web Services Composition. OnTheMove Workshops, Cyprus. pp. 39-48 .

Cirstea, Corina , Orejas, F. (ed.) (2006) An Institution of Modal Logics for Coalgebras. Journal of Logic and Algebraic Programming, 67 (1-2), 87-113. (doi:10.1016/j.jlap.2005.09.004).

Cirstea, Corina , Admek, J and Milius, S (eds.) (2006) A modular approach to defining and characterising notions of simulation. Information and Computation, 204 (4), 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, 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.) Logic and the Foundations of Game and Decision Theory, University of Liverpool. 12 - 15 Jul 2006.

Cirstea, Corina (2000) An Algebra-Coalgebra Framework for System Specification. Reichel, H. (ed.) 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.) 2nd International Workshop on Coalgebraic Methods in Computer Science. pp. 142-163 .

Cirstea, Corina (1998) Semantic Constructions for Hidden Algebra. Fiadeiro, J.L. (ed.) 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.) 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. Admek, J. and Milius, S. (eds.) 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.) 2nd Conference on Algebra and Coalgebra in Computer Science, Bergen, Norway. 19 - 23 Aug 2007. pp. 158-172 .

Cirstea, Corina and Sadrzadeh, Mehrnoosh (2008) Modular Games for Coalgebraic Fixed Point Logics. Admek, Jiri and Kupke, Clemens (eds.) Coalgebraic Methods in Computer Science 2008. pp. 71-92 .

Cirstea, Corina, Kurz, Alexander, Pattinson, Dirk, Schrder, Lutz and Venema, Yde (2008) Modal Logics are Coalgebraic. Abramsky, Samson, Gelenbe, Erol and Sassone, Vladimiro (eds.) Visions of Computer Science 2008.

Cirstea, Corina, Kurz, Alexander, Pattinson, Dirk, Schrder, Lutz and Venema, Yde , Sassone, Vladimiro (ed.) (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. Grdel, Erich and Kahle, Reinhard (eds.) 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.) Coalgebraic Methods in Computer Science 2010. pp. 83-103 .

Cirstea, Corina, Kupke, Clemens and Pattinson, Dirk (2011) EXPTIME tableaux for the coalgebraic -Calculus. Logical Methods in Computer Science, 7 (3:03), 1-33. (doi:10.2168/LMCS-7(3:3)2011).

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. Corradini, Andrea and Klin, Bartek (eds.) 2011 International Conference on Algebra and Coalgebra in Computer Science. pp. 130-144 . (doi:10.1007/978-3-642-22944-2_10).

Cirstea, Corina (2013) From Branching to Linear Time, Coalgebraically. Workshop on Fixed Points in Computer Science, Torino, Italy. pp. 11-27 . (doi:10.4204/EPTCS.126).

Alkhammash, Eman, Salehi Fathabadi, Asieh, Butler, Michael and Cirstea, Corina (2013) Building Traceable Event-B Models from Requirements. Automated Verification of Critical Systems (AVoCS 2013).

Cirstea, Corina (2014) A coalgebraic approach to linear-time logics. Muscholl, A (ed.) In Foundations of Software Science and Computation Structures: FoSSaCS 2014. vol. 8412, Springer. pp. 426-440 . (doi:10.1007/978-3-642-54830-7_28).

Alkhammash, Eman, Butler, Michael, Fathabadi, Asieh Salehi and Crstea, 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 (2016) Lattice-theoretic progress measures and coalgebraic model checking. In POPL '16 Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. vol. 51, ACM. pp. 718-732 . (doi:10.1145/2837614.2837673).

Cirstea, Corina (2017) From branching to linear time, coalgebraically. Fundamenta Informaticae, 150 (3-4), 379-406. (doi:10.3233/FI-2017-1474).

Alkhammash, Eman, Butler, Michael and Cirstea, Corina (2016) Modeling guidelines of FreeRTOS in Event-B. Communication, Management and Information Technology: Proceedings of the International Conference on Communication, Management and Information Technology (Iccmit 2016). pp. 453-462 .

Cirstea, Corina, Shimizu, Shunsuke and Hasuo, Ichiro (2017) Parity automata for quantitative linear time logics. 7th International Conference on Algebra and Coalgebra in Computer Science, , Ljubljana, Slovenia. 13 - 16 Jun 2017. 7:1-7:17 . (doi:10.4230/LIPIcs.CALCO.2017.7).

Zhu, Chenyang, Butler, Michael and Cirstea, Corina (2018) Refinement of timing constraints for concurrent tasks with scheduling. Butler, M., Raschke, A., Hoang, T. and Reichl, K. (eds.) In Abstract State Machines, Alloy, B, TLA, VDM, and Z: ABZ 2018. vol. 10817, Springer. pp. 219-233 . (doi:10.1007/978-3-319-91271-4).

Zhu, Chenyang, Butler, Michael and Cirstea, Corina (2018) Semantics of real-time trigger-response properties in Event-B. In 2018 International Symposium on Theoretical Aspects of Software Engineering (TASE). IEEE. pp. 150-156 . (doi:10.1109/TASE.2018.00028).

Zhu, Chenyang, Butler, Michael and Cirstea, Corina (2019) Towards refinement semantics of real-time trigger-response properties in Event-B. 13th International Symposium on Theoretical Aspects of Software Engineering, Guilin, Guilin, China. 29 Jul - 01 Aug 2019. 8 pp .

Cirstea, Corina (2019) Resource-aware automata and games for optimal synthesis. The Tenth International Symposium on Games, Automata, Logics, and Formal Verification, , Bordeaux, France. 02 - 03 Sep 2019. pp. 50-65 .

Zhu, Chenyang (2019) Dataset for 'Formalizing Hierarchical Scheduling for Refinement of Real-Time Systems'. University of Southampton doi:10.5258/SOTON/D1075 [Dataset]

Zhu, Chenyang, Butler, Michael and Cirstea, Corina (2020) Formalizing hierarchical scheduling for refinement of real-time systems. Science of Computer Programming, 189, [102390]. (doi:10.1016/j.scico.2020.102390).

Zhu, Chenyang, Butler, Michael and Cirstea, Corina (2020) Real-time trigger-response properties for Event-B applied to the pacemaker. In The 14th International Symposium on Theoretical Aspects of Software Engineering. IEEE. 8 pp . (In Press)

Zhu, Chenyang, Butler, Michael and Cirstea, Corina (2020) Trace semantics and refinement patterns for real-time properties in event-B models. Science of Computer Programming, 197, [102513]. (doi:10.1016/j.scico.2020.102513).

Yazdanpanah, Vahid, Gerding, Enrico H., Stein, Sebastian, Cirstea, Corina, schraefel, m.c., Norman, Timothy J. and Jennings, Nicholas R. (2021) Collective responsibility in multiagent settings. ACM Collective Intelligence Conference 2021 (CI-2021), Virtual, Copenhagen, Denmark. 29 - 30 Jun 2021. 4 pp . (In Press)

Zhu, Chenyang, Butler, Michael, Cirstea, Corina and Hoang, Thai Son (2021) Reasoning About Real-Time Systems in Event-B Models with Fairness Assumptions. In Proceedings of TASE2021 Conference. (In Press)

Yazdanpanah, Vahid, Gerding, Enrico, Stein, Sebastian, Cirstea, Corina, schraefel, m.c., Norman, Timothy and Jennings, Nicholas R. (2021) Different Forms of Responsibility in Multiagent Systems: Sociotechnical Characteristics and Requirements. IEEE Internet Computing, 25 (6), 15-22. (doi:10.1109/MIC.2021.3107334).

Contact

Telephone: +44 (0) 23 8059 3625

Email: cc2@ecs.soton.ac.uk

Share this profile FacebookTwitterWeibo