Tactics of Refinement. - Marcel Oliveira; Ana Cavalcanti 001 (SBES, 2000)

ArcAngel: a Tactic Language for Refinement. - Marcel Oliveira; Ana Cavalcanti 001; Jim Woodcock 001 (Formal Aspects Comput., 2003)

From Circus to JCSP. - Marcel Oliveira; Ana Cavalcanti 001 (ICFEM, 2004)

Refine and Gabriel: Support for Refinement and Tactics. - Marcel Oliveira; Manuela Xavier; Ana Cavalcanti 001 (SEFM, 2004)

Formal development of industrial-scale systems in Circus. - Marcel Oliveira; Ana Cavalcanti 001; Jim Woodcock 001 (Innov. Syst. Softw. Eng., 2005)

Formal derivation of state-rich reactive programs using Circus. - Marcel Vinícius Medeiros Oliveira (2005)

A Denotational Semantics for Circus. - Marcel Oliveira; Ana Cavalcanti 001; Jim Woodcock 001 (Refine@ICFEM, 2006)

Automatic Generation of Verified Concurrent Hardware. - Marcel Oliveira; Jim Woodcock 001 (ICFEM, 2007)

Tool Support for the CircusRefinement Calculus. - Alessandro Cavalcante Gurgel; Cristiano Gurgel de Castro; Marcel Vinícius Medeiros Oliveira (ABZ, 2008)

CRefine: Support for the Circus Refinement Calculus. - Marcel Vinícius Medeiros Oliveira; Alessandro Cavalcante Gurgel; Cristiano Gurgel de Castro (SEFM, 2008)

ArcAngelC: a Refinement Tactic Language for Circus. - Marcel Oliveira; Ana Cavalcanti 001 (Refine@FM, 2008)

Composing architectural aspects based on style semantics. - Christina Chavez; Alessandro F. Garcia 001; Thaís Vasconcelos Batista; Marcel Vinícius Medeiros Oliveira; Cláudio Sant'Anna; Awais Rashid (AOSD, 2009)

Formal Specification of a Cardiac Pacing System. - Artur Oliveira Gomes; Marcel Vinícius Medeiros Oliveira (FM, 2009)

Supporting ArcAngel in ProofPower. - Frank Zeyda; Marcel Oliveira; Ana Cavalcanti 001 (REFINE@FMWeek, 2009)

A UTP semantics for Circus. - Marcel Oliveira; Ana Cavalcanti 001; Jim Woodcock 001 (Formal Aspects Comput., 2009)

Integrating SMT-Solvers in Z and B Tools. - Alessandro Cavalcante Gurgel; Valério Gutemberg de Medeiros; Marcel Vinícius Medeiros Oliveira; David Boris Paul Déharbe (ASM, 2010)

Specification and Verification of a MPI Implementation for a MP-SoC. - Umberto Souza da Costa; Ivan Soares de Medeiros Júnior; Marcel Vinícius Medeiros Oliveira (ICTAC, 2010)

Formal Development of a Cardiac Pacemaker: From Specification to Code. - Artur Oliveira Gomes; Marcel Vinícius Medeiros Oliveira (SBMF, 2010)

Modelling and Implementing Complex Systems with Timebands. - Jim Woodcock 001; Marcel Oliveira; Alan Burns 001; Kun Wei (SSIRI, 2010)

B to CSP Migration: Towards a Formal and Automated Model-Driven Engineering of Hardware/Software Co-design. - Marcel Vinícius Medeiros Oliveira; David Déharbe; Luís C. D. S. Cruz (SBMF, 2011)

A tactic language for refinement of state-rich concurrent specifications. - Marcel Oliveira; Frank Zeyda; Ana Cavalcanti 001 (Sci. Comput. Program., 2011)

Implementing Tactics of Refinement in CRefine. - Madiel Conserva Filho; Marcel Vinícius Medeiros Oliveira (SEFM, 2012)

JCircus 2.0: an Extension of an Automatic Translator from Circus to Java. - S. L. M. Barrocas; Marcel Oliveira (CPA, 2012)

Mechanised support for sound refinement tactics. - Frank Zeyda; Marcel Oliveira; Ana Cavalcanti 001 (Formal Aspects Comput., 2012)

Using IT Education to Reveal New Horizons - A Large Scale Case Study on Digital and Social Inclusion. - Marcel Vinícius Medeiros Oliveira; Jair Cavalcanti Leite; Adrião Duarte Dória Neto; Pablo Javier Alsina; José Ivonildo Rego; Izabel Hazin; Jorge Tarcísio da Rocha Falcão (CSEDU, 2013)

A Verified Protocol to Implement Multi-way Synchronisation and Interleaving in CSP. - Marcel Vinícius Medeiros Oliveira; Ivan Soares de Medeiros Júnior; Jim Woodcock 001 (SEFM, 2013)

Unifying theories in ProofPower-Z. - Marcel Oliveira; Ana Cavalcanti 001; Jim Woodcock 001 (Formal Aspects Comput., 2013)

Model-Checking Circus State-Rich Specifications. - Marcel Vinícius Medeiros Oliveira; Augusto C. A. Sampaio; Madiel S. Conserva Filho (IFM, 2014)

Leadership Election: An Industrial SoS Application of Compositional Deadlock Verification. - Pedro R. G. Antonino; Marcel Vinícius Medeiros Oliveira; Augusto Sampaio 001; Klaus E. Kristensen; Jeremy W. Bryans (NASA Formal Methods, 2014)

Constructive extensibility of trustworthy component-based systems. - José Dihego; Augusto Sampaio 001; Marcel Vinícius Medeiros Oliveira (SAC, 2015)

Hard-Wiring CSP Hiding: Implementing Channel Abstraction to Generate Verified Concurrent Hardware. - F. J. S. Macário; Marcel Vinícius Medeiros Oliveira (SBMF, 2015)

Local Livelock Analysis of Component-Based Models. - Madiel S. Conserva Filho; Marcel Vinícius Medeiros Oliveira; Augusto Sampaio 001; Ana Cavalcanti 001 (ICFEM, 2016)

Rigorous development of component-based systems using component metadata and patterns. - Marcel Vinícius Medeiros Oliveira; Pedro Antonino; Rodrigo Ramos; Augusto Sampaio 001; Alexandre Cabral Mota; A. W. Roscoe 001 (Formal Aspects Comput., 2016)

BTS: A Tool for Formal Component-Based Development. - Dalay Israel de Almeida Pereira; Marcel Vinícius Medeiros Oliveira; Madiel S. Conserva Filho; Sarah Raquel Da Rocha Silva (IFM, 2017)

An Automated Environment for Teaching Programming Logic on Distance Learning IT Courses. - Nelson Ion de Oliveira; Marcel Vinícius Medeiros Oliveira; Jorge Tarcísio da Rocha Falcão (CSEDU (1), 2018)

Compositional and local livelock analysis for CSP. - Madiel Conserva Filho; Marcel Vinícius Medeiros Oliveira; Augusto Sampaio 001; Ana Cavalcanti 001 (Inf. Process. Lett., 2018)

A Research Landscape on Formal Verification of Software Architecture Descriptions. - Camila Araújo; Everton Cavalcante; Thaís Batista; Marcel Oliveira; Flávio Oquendo (IEEE Access, 2019)

Empowering SysML-Based Software Architecture Description with Formal Verification: From SysADL to CSP. - Fagner Dias; Marcel Oliveira; Thaís Vasconcelos Batista; Everton Cavalcante; Jair C. Leite; Flávio Oquendo; Camila Araújo (ECSA, 2020)

A refinement checking based strategy for component-based systems evolution. - José Dihego; Augusto Sampaio 001; Marcel Oliveira (J. Syst. Softw., 2020)

The CLEARSY safety platform: 5 years of research, development and deployment. - Thierry Lecomte; David Déharbe; Paulin Fournier; Marcel Oliveira (Sci. Comput. Program., 2020)

CSP specification and verification of relay-based railway interlocking systems. - Dalay Israel de Almeida Pereira; Marcel Vinícius Medeiros Oliveira; P. E. R. Bezerra; Philippe Bon; Simon Collart Dutilleul (SAC, 2022)

Automatic Generation of Verified Concurrent Hardware Using VHDL. - Luciano Silva; Marcel Oliveira (SBMF, 2022)

UTP, Circus, and Isabelle. - Jim Woodcock 001; Ana Cavalcanti 001; Simon Foster 001; Marcel Oliveira; Augusto Sampaio 001; Frank Zeyda (Theories of Programming and Formal Methods, 2023)

CSP Specification and Verification of a Relay-Based Railway Interlocking System. - P. E. R. Bezerra; Marcel Vinícius Medeiros Oliveira; Thierry Lecomte; Dalay Israel de Almeida Pereira (SBMF, 2023)