Publications

2026

• A. Ribeiro, M. Mamede, and C. Ferreira. Systematic API Testing Through Model Checking and Executable Contracts. ICST 2026: Conference on Software Testing, Verification and Validation. [paper]
• V. Mikytiv, B. Toninho, and C. Ferreira. In Perfect Harmony: Orchestrating Causality in Actor-Based Systems. ICST 2026: Conference on Software Testing, Verification and Validation. [paper]

2025

• D. Borrego, N. Preguiça, E. Gonzalez Boix, and C. Ferreira. Ensuring Convergence and Invariants Without Coordination. ECOOP 2025: European Conference on Object-Oriented Programming. [paper] [artifact]
• K. De Porre, C. Ferreira, and E. Gonzalez Boix. Concurrency Contracts for Designing Highly Available Replicated Data Types. Software: Practice and Experience, 55(9), 2025. [paper]
• D. Borrego, A. Vilalonga, H. Domingos, N. Preguiça, E. Gonzalez Boix, and C. Ferreira. ReDunT: Automatically Deriving Redundancy Relations for Pure Op-Based CRDTs. PaPoC@EuroSys 2025: Workshop on the Principles and Practice of Consistency for Distributed Data. [paper]
• A. Pandey, S. Dumbrava, M. Shapiro, C. Ferreira, M. Pereira, and N. Preguiça. Towards Local-First Distributed Property Graphs. PaPoC@EuroSys 2025: Workshop on the Principles and Practice of Consistency for Distributed Data. [paper]
• C. Ferreira and C. A. Mezzina (editors). Formal Techniques for Distributed Objects, Components, and Systems. FORTE 2025: 45th IFIP WG 6.1 International Conference, Springer LNCS, 2025. [book]

2024

• E. Schiebelbein, S. Hatia, A. Bieniusa, C. Ferreira, G. Petri, and M. Shapiro. Models for Storage in Database Backends. PaPoC@EuroSys 2024: Workshop on the Principles and Practice of Consistency for Distributed Data. [paper] [bibtex]
• J. Costa Seco, H. Lourenço, J. Parreira, and C. Ferreira. Going Beyond Templates: Composition and Evolution in Nested OSTRICH. Software and Systems Modeling, 2024. [paper] [bibtex]
• A. Pedro, T. Silva, T. Sequeira, J. Lourenço, J. Costa Seco, and C. Ferreira. Monitoring of Spatio-Temporal Properties with Nonlinear SAT Solvers. Journal on Software Tools for Technology Transfer, 26(2), 2024. [paper] [bibtex]

2023

• K. De Porre, C. Ferreira, and E. Gonzalez Boix. VeriFx: Correct Replicated Data Types for the Masses. ECOOP 2023: European Conference on Object-Oriented Programming. [paper] [artifact] [bibtex]
• H. Lourenço, C. Ferreira, J. Costa Seco, and J. Parreira. OSTRICH: a rich template language for low-code development (extended version). Software and Systems Modeling, 22(5), 2023. [paper] [bibtex]
• J. Quirino Silva, D. Melo, I. Pimenta Rodrigues, J. Costa Seco, C. Ferreira, and J. Parreira. An Ontology-Based Task-Oriented Dialogue to Create OutSystems Applications. SN Computer Science, 4(1), 2023. [paper] [bibtex]
• H. Lourenço, J. Costa Seco, C. Ferreira, T. Simões, V. Silva, F. Assunção, and A. Menezes. CHAMELEON: OutSystems Live Bidirectional Transformations. CoRR abs/2305.03361 (under revision). [paper]
• S. Simões, A. Ribeiro, C. Ferreira, and N. Preguiça. JepREST: Functional tests for distributed REST applications. CoRR abs/2303.14104 (2023). [paper]
• C. Ferreira and T. A. C. Willemse (editors). Software Engineering and Formal Methods. SEFM 2023: 21st International Conference, Springer LNCS, 2023. [book]

2022

• J. Costa Seco, H. Lourenço, J. Parreira, and C. Ferreira. Nested OSTRICH: hatching compositions of low-code templates. MoDELS 2022: Conference on Model Driven Engineering Languages and Systems. [paper] [bibtex]
• J. Costa Seco, J. Aldrich, L. Carvalho, B. Toninho, and C. Ferreira. Derivations with holes for concept-based program synthesis. Onward! 2022: Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software. [paper] [bibtex]
• A. Matos Pedro, T. Silva, T. Sequeira, J. Lourenço, J. Costa Seco, and C. Ferreira. Monitoring of Spatio-Temporal Properties with Nonlinear SAT Solvers. FMICS 2022: Conference on Formal Methods for Industrial Critical Systems. [paper] [bibtex]

2021

• K. De Porre, C. Ferreira, N. Preguiça, and E. Gonzalez Boix. ECROs: Building Global Scale Systems from Sequential Code. OOPSLA 2021: Object-Oriented Programming, Systems, Languages & Applications. [paper] [artifact] [bibtex]
• H. Lourenço, C. Ferreira, and J. Costa Seco. OSTRICH — A Type-safe Template Language for Low-code Development. MoDELS 2021: Conference on Model Driven Engineering Languages and Systems. [paper] [bibtex]
• B. Lopes, C. Ferreira, and S. Amorim. Solution Discovery over Feature Toggling with Built-in Abstraction in OutSystems. LowCode@MoDELS 2021: Conference on Model Driven Engineering Languages and Systems: Companion Proceedings. [paper] [bibtex]
• J. Quirino Silva, D. Melo, I. Pimenta Rodrigues, J. Costa Seco, C. Ferreira, and J. Parreira. An Ontology based Task Oriented Dialogue. KEOD 2021: Conference on Knowledge Discovery, Knowledge Engineering and Knowledge Management. [paper] [bibtex]
• S. Nair, F. Meirim, M. Pereira, C. Ferreira, and M. Shapiro. A coordination-free, convergent, and safe replicated tree. CoRR abs/2103.04828 (2021). [paper]

2020

• J. Costa Seco, P. Ferreira, H. Lourenço, C. Ferreira, and L. Ferrão. Robust Contract Evolution in a TypeSafe MicroServices Architecture. The Art, Science, and Engineering of Programming, 4(3), 2020. [paper] [bibtex]
• I. Ulidowski, I. Lanese, U. Schultz, and C. Ferreira (editors). Reversible Computation: Extending Horizons of Computing. Selected Results of the COST Action IC1405, Springer Nature, 2020. [book]
• P. Zeller, A. Bieniusa, and C. Ferreira. Teaching practical realistic verification of distributed algorithms in Erlang with TLA+. Erlang 2020: International Workshop on Erlang. [paper] [bibtex]
• A. Jacinto, M. Lourenço, and C. Ferreira. Test mocks for low-code applications built with OutSystems. LowCode@MoDELS 2020: Conference on Model Driven Engineering Languages and Systems: Companion Proceedings. [paper] [bibtex]

2019

• C. Ferreira. Techniques for safe and highly available cloud applications. PaPoC@EuroSys 2019: Workshop on Principles and Practice of Consistency for Distributed Data. [paper] [bibtex]
• P. Lopes, J. Sousa, V. Balegas, C. Ferreira, S. Duarte, A. Bieniusa, R. Rodrigues, and N. Preguiça. Antidote SQL: Relaxed When Possible, Strict When Necessary. CoRR abs/1902.03576 (2019). [paper]

2018

• V. Balegas, S. Duarte, C. Ferreira, R. Rodrigues, and N. Preguiça. IPA: invariant-preserving applications for weakly consistent replicated databases. Proceedings of the VLDB Endowment, 12(4), 2018. [paper] [bibtex]

2017

• R. Dias, C. Ferreira, J. Fiedor, J. Lourenço, A. Smrcka, D. Sousa, and T. Vojnar. Verifying concurrent programs using contracts. ICST 2017: Conference on Software Testing, Verification and Validation. [paper] [bibtex]
• G. Marcelino, V. Balegas, and C. Ferreira. Bringing hybrid consistency closer to programmers. PaPoC@EuroSys 2017: Workshop on the Principles and Practice of Consistency for Distributed Data. [paper] [bibtex]
• C. Baquero, P. Almeida, A. Cunha, and C. Ferreira. Composition in state-based replicated data types. Bulletin of the European Association for Theoretical Computer Science, 123, 2017. [paper] [bibtex]

2016

• M. Najafzadeh, A. Gotsman, H. Yang, C. Ferreira, and M. Shapiro. The CISE tool: proving weakly-consistent applications correct. PaPoC@EuroSys 2016: Workshop on the Principles and Practice of Consistency for Distributed Data. [paper] [bibtex]
• A. Gotsman, H. Yang, C. Ferreira, M. Najafzadeh, and M. Shapiro. 'Cause I'm strong enough: reasoning about consistency choices in distributed systems. POPL 2016: Symposium on Principles of Programming Languages. [paper] [bibtex]
• V. Balegas, C. Li, M. Najafzadeh, D. Porto, A. Clement, S. Duarte, C. Ferreira, J. Gehrke, J. Leitão, N. Preguiça, R. Rodrigues, M. Shapiro, and V. Vafeiadis. Geo-Replication: Fast If Possible, Consistent If Necessary. IEEE Data Engineering Bulletin, 39(1), 2016. [paper]

2015

• V. Balegas, D. Serra, S. Duarte, C. Ferreira, M. Shapiro, R. Rodrigues, and N. Preguiça. Extending Eventually Consistent Cloud Databases for Enforcing Numeric Invariants. SRDS 2015: Symposium on Reliable Distributed Systems. [paper]
• V. Balegas, S. Duarte, C. Ferreira, R. Rodrigues, N. Preguiça, M. Najafzadeh, and M. Shapiro. Putting the Consistency back into Eventual Consistency. EuroSys 2015: European Conference on Computer Systems. [paper]
• V. Balegas, S. Duarte, C. Ferreira, R. Rodrigues, N. Preguiça, M. Najafzadeh, and M. Shapiro. Towards Fast Invariant Preservation in Geo-replicated Systems. SIGOPS Operating Systems Review, 49(1): 121–125, 2015. [paper]

2012

• R. Bruni, C. Ferreira, and A. Kersten Kauer. First-order dynamic logic for compensable processes. COORD 2012: International Conference on Coordination Models and Languages. [paper]
• C. Vaz and C. Ferreira. On the analysis of compensation correctness. The Journal of Logic and Algebraic Programming, 81(5): 585–605, 2012. [paper]

2011

• C. Ferreira, I. Lanese, A. Ravara, H. Vieira, and G. Zavattaro. Advanced mechanisms for service combination and transactions. In Rigorous Software Engineering for Service-Oriented Systems — Results of the SENSORIA project, LNCS 6582, 2011. [paper]

2010

• L. Caires, C. Ferreira, and A. Ravara. A simple proof system for lock-free concurrency. PSPL 2010: International Workshop on Proof Systems for Program Logics. [paper]
• I. Lanese, C. Vaz, and C. Ferreira. On the expressive power of primitives for compensation handling. ESOP 2010: European Symposium on Programming, LNCS 6012, 2010. [paper]
• C. Vaz and C. Ferreira. Towards compensation correctness in interactive systems. WS-FM 2009: International Workshop on Web Services and Formal Methods, LNCS 6194, 2010. [paper]

2009

• C. Vaz, C. Ferreira, and A. Ravara. Dynamic recovering of long running transactions. TGC 2008: International Symposium on Trustworthy Global Computing, LNCS 5474, 2009. [paper]
• L. Caires, C. Ferreira, and H. Vieira. A Process Calculus Analysis of Compensations. TGC 2008: International Symposium on Trustworthy Global Computing, LNCS 5474, 2009. [paper]

2005

• M. Butler, C. Ferreira, and M.Y. Ng. Precise modelling of compensating business transactions and its application to BPEL. Journal of Universal Computer Science, 11(5): 712–743, 2005. [paper]
• M. Butler, C.A.R. Hoare, and C. Ferreira. A trace semantics for long-running transactions. In Communicating Sequential Processes: The First 25 Years, LNCS 3525, 2005. [paper]
• R. Bruni, M. Butler, C. Ferreira, C.A.R. Hoare, H. Melgratti, and U. Montanari. Comparing two approaches to compensable flow composition. CONCUR 2005: International Conference on Concurrency Theory, LNCS 3653, 2005. [paper]

2004

• M. Butler and C. Ferreira. An operational semantics for StAC, a language for modelling long-running business transactions. COORD 2004: International Conference on Coordination Models and Languages, LNCS 2949, 2004. [paper]

2003

• C. Ferreira and M. Butler. Using B refinement to analyse compensating business processes. ZB 2003: International ZB Conference, LNCS 2651, 2003. [paper]
• J. Augusto, M. Leuschel, M. Butler, and C. Ferreira. Using the extensible model checker XTL to verify StAC business specifications. AVoCS 2003: Workshop on Automated Verification of Critical Systems. [paper]
• J. Augusto, C. Ferreira, A. Gravell, M. Leuschel, and K. Ng. The benefits of rapid modelling for e-business system development. ER 2003: Conceptual Modeling for Novel Application Domains, LNCS 2814, 2003. [paper]
• J. Augusto, M. Butler, C. Ferreira, and S. Craig. Using SPIN and STeP to verify StAC specifications. PSI 2003: International A.P. Ershov Conference on Perspectives of System Informatics, LNCS 2890, 2003. [paper]
• J. Augusto, Y. Howard, A. Gravell, C. Ferreira, S. Gruner, and M. Leuschel. Model-based approaches for validating business critical systems. International Workshop on Software Technology and Engineering Practice, IEEE Press, 2003. [paper]
• Y. Howard, S. Gruner, A. Gravell, C. Ferreira, and J. Augusto. Model-based trace-checking. SoftTest 2003: UK Software Testing Research Workshop, York Computer Science Yellow Report Series, 2003. [paper]
• A. Gravell, Y. Howard, J. Augusto, C. Ferreira, and S. Gruner. Concurrent development of model and implementation. ICSSEA 2003: International Conference on Software and Systems Engineering and their Applications, 2003. [paper]

2002

• M. Chessell, D. Vines, C. Griffen, M. Butler, C. Ferreira, and P. Henderson. Extending the concept of transaction compensation. IBM Systems Journal, 41(4): 743–758, 2002. [paper]

2001

• M. Leuschel, L. Adhianto, M. Butler, C. Ferreira, and L. Mikhailov. Animation and model checking of CSP and B. VCL 2001: ACM SIGPLAN International Workshop on Verification and Computational Logic. [paper]

2000

• M. Butler and C. Ferreira. A process compensation language. IFM 2000: Integrated Formal Methods, LNCS 1945, 2000. [paper]

Theses

• C. Ferreira. Precise modelling of business processes with compensation. PhD thesis, University of Southampton, 2003.
• C. Ferreira. Uma abordagem formal ao problema da classificação de componentes de software (in Portuguese). Master's thesis, Universidade do Minho, 1997.