×

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 CPHC/BCS Distinguished Dissertations selection panel (since 2016)

Member of IFIP Working Group 1.3

Member of CALCO Steering Committee

Member of CMCS Steering Committee

Organiser of CALCO 2011

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), 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,
Orejas, F.(ed.)
(2006)
An Institution of Modal Logics for Coalgebras
*Journal of Logic and Algebraic Programming*, 67, (1-2), pp. 87-113. (doi:10.1016/j.jlap.2005.09.004).

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.)
(2011)
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, Kupke, Clemens and Pattinson, Dirk
(2011)
EXPTIME tableaux for the coalgebraic µ-Calculus
*Logical Methods in Computer Science*, 7, (3:03), pp. 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), 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.

Cirstea, Corina
(2013)
From Branching to Linear Time, Coalgebraically
At * Workshop on Fixed Points in Computer Science**, Italy*.
*
17 pp, 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
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
(2016)
Lattice-theoretic progress measures and coalgebraic model checking
At * 43rd Symposium on Principles of Programming Languages**, United States*.
*20 - 23 Jan 2016.*
15 pp, pp. 718-732.

Cirstea, Corina
(2017)
From branching to linear time, coalgebraically
*Fundamenta Informaticae*, 150, (3-4), pp. 379-406.

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.
*

Cirstea, Corina, Shimizu, Shunsuke and Hasuo, Ichiro
(2017)
Parity automata for quantitative linear time logics
At * 7th International Conference on Algebra and Coalgebra in Computer Science**, Ljubljana, Slovenia*.
*14 - 16 Jun 2017.*
17 pp, 7:1-7:17.

**Telephone:** +442380593625

**Email:** cc2@ecs.soton.ac.uk

×