Marcel Vinicius Medeiros Oliveira

  • Endereço para acessar este CV: http://lattes.cnpq.br/1756952696097255
  • Última atualização do currículo em 21/09/2018


Marcel Vinicius Medeiros Oliveira é Professor Associado do Departamento de Informática e Matemática Aplicada (DIMAp) da Universidade Federal do Rio Grande do Norte (UFRN). Ele possui Bacharelado em Ciência da Computação pela Universidade Federal de Pernambuco (2000), Mestrado em Ciência da Computação pela Universidade Federal de Pernambuco (2002) e é Ph.D. em Ciência da Computação pela Universidade de York, Inglaterra (2006). Atualmente, ele é membro do Instituto Nacional de Engenharia de Software, membro do Comitê Especial de Métodos Formais da Sociedade Brasileira de Computação, membro do Colegiado da Pós-Graduação em Sistemas e Computação (PPgSC) da UFRN, e Coordenador de Cursos Técnicos do Instituto Metrópole Digital da UFRN com cerca de 2000 alunos. No Instituto Metrópole Digital, ele é membro colaborador, além de ser membro da Comissão de Desenvolvimento Acadêmico, Diretor Adjunto de Ensino e Vice-Coordenador do SETE, Núcleo de Integração, Pesquisado e Inovação em Engenharia de Software do Instituto. Marcel Oliveira tem experiência na área de Ciência da Computação, com ênfase em Métodos Formais. Mais especificamente, sua pesquisa tem focado em cálculo e táticas de refinamentos, concorrência, semântica de linguagens formais, integração de métodos formais e síntese de código a partir de especificações formais. Ele tem ensinado as disciplinas de Banco de Dados, Lógica Aplicada à Engenharia de Software e Métodos Formais. (Texto informado pelo autor)


Identificação


Nome
Marcel Vinicius Medeiros Oliveira
Nome em citações bibliográficas
OLIVEIRA, M. V. M.;Oliveira, Marcel;OLIVEIRA, MARCEL VINÍCIUS MEDEIROS;OLIVEIRA, M.V.M.

Endereço


Endereço Profissional
Universidade Federal do Rio Grande do Norte, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.
Campus Universitário
Lagoa Nova
59072970 - Natal, RN - Brasil
Telefone: (84) 33422216
Ramal: 119
URL da Homepage: http://dimap.ufrn.br/~marcel


Formação acadêmica/titulação


2003 - 2005
Doutorado em Ciência da Computação.
University of York, YORK, Inglaterra.
Título: Formal Derivation of State-Rich Reactive Programs using Circus, Ano de obtenção: 2006.
Orientador: Ana Lúcia Caneca Cavalcanti.
Bolsista do(a): Engineering and Physical Sciences Research Council, EPSRC, Inglaterra.
Palavras-chave: Métodos Formais; Desenvolvimento de Programas; Cálculo de Refinamentos; Concorrência.
Grande área: Ciências Exatas e da Terra
Setores de atividade: Desenvolvimento de Programas (Software).
2001 - 2002
Mestrado em Ciências da Computação.
Universidade Federal de Pernambuco, UFPE, Brasil.
Título: ArcAngel: a Tactic Language for Refinement and its Tool Support,Ano de Obtenção: 2003.
Orientador: Ana Lúcia Caneca Cavalcanti.
Palavras-chave: Desenvolvimento de Programas; Refinamento; Suporte Ferramental.
Grande área: Ciências Exatas e da Terra
Setores de atividade: Desenvolvimento de Programas (Software).
1996 - 2000
Graduação em Ciência da Computação.
Universidade Federal de Pernambuco, UFPE, Brasil.
Título: Tactics of Refinement.
Orientador: Ana Lúcia Caneca Cavalcanti.


Pós-doutorado


2011 - 2012
Pós-Doutorado.
Universidade Federal de Pernambuco, UFPE, Brasil.
Grande área: Ciências Exatas e da Terra


Formação Complementar


2016 - 2016
Lean Six Sigma Yellow Belt. (Carga horária: 8h).
Convictus Sinergia Corporativa, CSC, Brasil.
2008 - 2008
Models Based Approaches for Interactive System Pro. (Carga horária: 4h).
Universidade Federal da Bahia, UFBA, Brasil.
2007 - 2007
Pernambuco School of Software Engineering/Testing. (Carga horária: 40h).
Universidade Federal de Pernambuco, UFPE, Brasil.
2007 - 2007
Oficina Pedagócia Elaboração de Projetos de Ensino. (Carga horária: 8h).
Universidade Federal do Rio Grande do Norte, UFRN, Brasil.
2006 - 2006
Modelagem e Valid. de Sist. Usando Redes de Petri. (Carga horária: 4h).
Universidade Federal do Rio Grande do Norte, UFRN, Brasil.
2005 - 2005
IFM - Verifying Industrial Control System Software. (Carga horária: 8h).
Newcastle University, NCL, Inglaterra.
2005 - 2005
FM - SPARK. (Carga horária: 8h).
Newcastle University, NCL, Inglaterra.
2004 - 2004
Marktoberdorf Summer School. (Carga horária: 70h).
Technische Universität München, TUM, Alemanha.
2004 - 2004
IFM- A Tutorial Introduction to Designs in the UTP. (Carga horária: 4h).
University of Kent, U. KENT, Inglaterra.
2003 - 2003
SEUJP - CSP. (Carga horária: 12h).
University of London, UL, Inglaterra.
2003 - 2003
SEUJP - Refinement. (Carga horária: 12h).
University of Kent, U. KENT, Inglaterra.
2000 - 2000
Aplicações Distribuídas Em Java e Xml. (Carga horária: 12h).
Universidade Federal de Pernambuco, UFPE, Brasil.


Atuação Profissional



Universidade Federal do Rio Grande do Norte, UFRN, Brasil.
Vínculo institucional

2018 - Atual
Vínculo: Servidor Público, Enquadramento Funcional: Professor Associado II, Carga horária: 40, Regime: Dedicação exclusiva.

Vínculo institucional

2016 - 2018
Vínculo: Servidor Público, Enquadramento Funcional: Professor Associado I, Carga horária: 40, Regime: Dedicação exclusiva.

Vínculo institucional

2014 - 2016
Vínculo: Servidor Público, Enquadramento Funcional: Professor Adjunto IV, Carga horária: 40, Regime: Dedicação exclusiva.

Vínculo institucional

2012 - 2014
Vínculo: Servidor Público, Enquadramento Funcional: Professor Adjunto III, Carga horária: 40, Regime: Dedicação exclusiva.

Vínculo institucional

2010 - 2012
Vínculo: Servidor Público, Enquadramento Funcional: Professor Adjunto II, Carga horária: 40, Regime: Dedicação exclusiva.

Vínculo institucional

2008 - 2010
Vínculo: Servidor Público, Enquadramento Funcional: Professor Adjunto I, Carga horária: 40, Regime: Dedicação exclusiva.

Vínculo institucional

2006 - 2008
Vínculo: Bolsista, Enquadramento Funcional: Bolsista, Carga horária: 40

Atividades

06/2016 - Atual
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, .

Cargo ou função
Membro do Núcleo Docente Estruturante do curso de Ciência da Computação.
10/2014 - Atual
Conselhos, Comissões e Consultoria, Departamento de Informática e Matemática Aplicada, .

Cargo ou função
Membro do Núcleo Docente Estruturante do Bacharelado em Engenharia de Software.
03/2014 - Atual
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro da Comissão de Desenvolvimento Acadêmico do Instituto Metrópole Digital.
03/2014 - Atual
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Comissão de Avaliação de Progressão Funcional do Instituto Metrópole Digital.
12/2013 - Atual
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, .

Cargo ou função
Membro do Conselho do Centro de Ciências Exatas e da Terra.
04/2013 - Atual
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Colegiado do Curso de Engenharia de Software.
01/2012 - Atual
Direção e administração, Instituto Metrópole Digital, .

Cargo ou função
Coordenador de Cursos Técnicos do Instituto Metrópole Digital.
08/2009 - Atual
Conselhos, Comissões e Consultoria, Departamento de Informática e Matemática Aplicada, .

Cargo ou função
Presidente da Comissão Especial de Métodos Formais da SBC.
08/2008 - Atual
Ensino, Ciência da Computação, Nível: Graduação

Disciplinas ministradas
Métodos Formais
Banco de Dados
Prática de Conceitos e Técnicas de Programação
01/2008 - Atual
Ensino, Sistemas e Computação, Nível: Pós-Graduação

Disciplinas ministradas
Especificações Formais
01/2008 - Atual
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Comitê de Programa do Simpósio Brasileiro de Métodos Formais.
01/2007 - Atual
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Colegiado da Pós-Graduação.
05/2006 - Atual
Pesquisa e desenvolvimento , Centro de Ciências Exatas, .

07/2018 - 08/2018
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comitê de Programa do XXI Simpósio Brasileiro de Métodos Formais.
04/2014 - 04/2017
Direção e administração, Instituto Metrópole Digital, .

Cargo ou função
Supervisor de Cursos PRONATEC do Instituto Metrópole Digital.
09/2016 - 11/2016
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comité de Programa da Escola de Informática Teórica e Métodos Formais.
07/2016 - 08/2016
Conselhos, Comissões e Consultoria, Instituto Metrópole Digital, .

Cargo ou função
Comissão de Homologação do Estágio Probatório (Prof. IVANOVITCH MEDEIROS DANTAS DA SILVA).
03/2016 - 05/2016
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comitê de Programa do 6th International Symposium on Unifying Theories of Programming.
03/2015 - 09/2015
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, .

Cargo ou função
Presidente do Comitê de Programa da Sessão de Ferramentas do CBSOFT 2015.
01/2015 - 06/2015
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comitê de Programa do Refinement Workshop 2015.
07/2014 - 09/2014
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comitê de Programa do Simpósio Brasileiro de Métodos Formais.
02/2014 - 04/2014
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comitê de Programa do 5th International Symposium on Unifying Theories of Programming.
11/2013 - 12/2013
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Comissão de Seleção da Pós-Graduação 2014.1.
10/2013 - 12/2013
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comitê de Programa do 7th International Conference on Software Testing.
06/2013 - 07/2013
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comitê de Programa do Simpósio Brasileiro de Métodos Formais 2013.
05/2013 - 06/2013
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comitê de Programa da Sessão de Ferramentas do Congresso Brasileiro de Software: Teoria e Prática (CBSoft) 2013.
04/2013 - 06/2013
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comitê de Programa do XL Seminário Integrado de Software e Hardware - SEMISH 2013.
04/2012 - 07/2012
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comitê de Programa do Simpósio Brasileiro de Métodos Formais 2012.
05/2012 - 06/2012
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comitê de Programa da Sessão de Ferramentas do Congresso Brasileiro de Software: Teoria e Prática (CBSoft) 2012.
04/2012 - 06/2012
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comitê de Programa do XXXIX Seminário Integrado de Software e Hardware.
03/2012 - 04/2012
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Revisor Externo do International Symposium on Formal Methods 2012.
10/2011 - 12/2011
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comitë de Programa do Fifth International Conference on Software Testing, Verification and Validation.
05/2011 - 06/2011
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comitê de Programa da Sessão de Ferramentas do CBSoft 2011.
04/2011 - 05/2011
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comitê de Seleção dos Tutoriais do CBSoft 2011.
03/2011 - 04/2011
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comitê de Programa do 15º BCS FACS Refinement Workshop.
03/2011 - 04/2011
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comitê de Programa do SEMISH - XXXVIII Seminário Integrado de Software e Hardware.
06/2010 - 06/2010
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro da Comissão de Seleção da Pós-Graduação 2010.2.
10/2009 - 12/2009
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comitê de Programa do Workshop on Tool Building in Formal Methods 2009.
01/2009 - 12/2009
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Presidente do Comitê de Programa do Simpósio Brasileiro de Métodos Formais 2009.
09/2009 - 10/2009
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Revisor Externo do ABZ 2010.
07/2009 - 09/2009
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro do Comitê de Programa do International Conference on Formal Engineering Methods 2009.
01/2009 - 09/2009
Conselhos, Comissões e Consultoria, Departamento de Informática e Matemática Aplicada, .

Cargo ou função
Revisor Externo do RULE 09 - The Tenth International Workshop on Rule-Based Programming.
06/2009 - 06/2009
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro da Comissão de Seleção 2009.2 da Pós-Graduação.
05/2009 - 05/2009
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Revisor do RULE 09 - The 10th International Workshop on Rule-Based Programming.
03/2009 - 05/2009
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro da Comissão de Elaboração do Projeto Pedagógico do Bacharelado em Engenharia de Software.
12/2008 - 12/2008
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Membro da Comissão de Seleção da Pós-Graduação.
03/2008 - 05/2008
Conselhos, Comissões e Consultoria, Centro de Ciências Exatas, Departamento de Informática e Matemática Aplicada.

Cargo ou função
Revisor do Simpósio Brasileiro de Linguagens de Programação (SBLP 2008).
08/2007 - 12/2007
Ensino, Ciência da Computação, Nível: Graduação

Disciplinas ministradas
DIM0095 - Programação Funcional
03/2007 - 07/2007
Ensino, Ciência da Computação, Nível: Graduação

Disciplinas ministradas
DIM0098 - Cálculo de Programas
01/2007 - 06/2007
Ensino, Sistemas e Computação, Nível: Pós-Graduação

Disciplinas ministradas
2007.1 - DIM0805 - Especificações Formais
08/2006 - 12/2006
Ensino, Ciência da Computação, Nível: Graduação

Disciplinas ministradas
DIM0098 - Cálculo de Programas
05/2006 - 09/2006
Conselhos, Comissões e Consultoria, Departamento de Informática e Matemática Aplicada, .

Cargo ou função
Revisor do Software Engineering and Formal Methods (SEFM 2007).
6/2006 - 7/2006
Conselhos, Comissões e Consultoria, Universidade Federal do Rio Grande do Norte, .

Cargo ou função
Revisor do Simpósio Brasileiro de Métodos Formais (SBMF2006)..

University of York, YORK, Inglaterra.
Vínculo institucional

2004 - 2006
Vínculo: Colaborador, Enquadramento Funcional: Pesquisador Associado, Carga horária: 35

Atividades

01/2006 - 03/2006
Pesquisa e desenvolvimento , Department of Computer Science, .

01/2005 - 06/2005
Ensino, Computer Science, Nível: Graduação

Disciplinas ministradas
Formal Program Development
01/2005 - 06/2005
Ensino, Computer Science, Nível: Pós-Graduação

Disciplinas ministradas
A Tutorial Introduction to Designs in the Unifying Theories of Programming
07/2004 - 12/2004
Ensino, Computer Science, Nível: Graduação

Disciplinas ministradas
Formal Program Specification

University of Kent, U. KENT, Inglaterra.
Vínculo institucional

2003 - 2004
Vínculo: Colaborador, Enquadramento Funcional: Pesquisador Associado, Carga horária: 35

Atividades

1/2003 - 10/2004
Pesquisa e desenvolvimento , Computing Laboratory, .

Linhas de pesquisa
Métodos Formais
9/2003 - 6/2004
Ensino, Computer Science, Nível: Graduação

Disciplinas ministradas
Information Systems
1/2004 - 4/2004
Conselhos, Comissões e Consultoria, University of Kent, .

Cargo ou função
Comissão Organizadora - 4th International Conference on Integrated Formal Methods.

Instituto de Planejamento e Apoio ao Desenvolvimento Tecnológico e Científi, IPAD, Brasil.
Vínculo institucional

2001 - 2002
Vínculo: Colaborador, Enquadramento Funcional: Analista, Carga horária: 35

Atividades

11/2001 - 12/2002
Pesquisa e desenvolvimento , Datacenter, .

Linhas de pesquisa
Web
Engenharia de Software
01/2002 - 03/2002
Ensino, Cursos de Extensão do IPAD, Nível: Aperfeiçoamento

Disciplinas ministradas
Modelagem de Banco de Dados e Microsoft Access
Java Básico

Comércio Soluções Inteligentes, CSI, Brasil.
Vínculo institucional

2000 - 2001
Vínculo: Colaborador, Enquadramento Funcional: Analista, Carga horária: 40

Atividades

09/2000 - 10/2001
Pesquisa e desenvolvimento , Projeto P2K, .

Linhas de pesquisa
Engenharia de Software

Universidade Federal de Pernambuco, UFPE, Brasil.
Vínculo institucional

2001 - 2002
Vínculo: Aluno de Mestrado, Enquadramento Funcional: Aluno de Mestrado, Carga horária: 40

Vínculo institucional

1999 - 2000
Vínculo: Bolsa de Iniciação Científica, Enquadramento Funcional: Bolsista, Carga horária: 15

Vínculo institucional

1996 - 2000
Vínculo: Aluno de Graduação, Enquadramento Funcional: Aluno de Graduação, Carga horária: 40, Regime: Dedicação exclusiva.

Atividades

01/1999 - 12/2000
Outras atividades técnico-científicas , Centro de Informática, Centro de Informática.

Atividade realizada
Monitoria em Disciplina de Graduação: Bancos de Dados 1.
01/1996 - 12/1996
Outras atividades técnico-científicas , Centro de Informática, Centro de Informática.

Atividade realizada
Monitoria em Disciplina de Graduação: Algoritmos e Estrutura de Dados.


Linhas de pesquisa


1.
Engenharia de Software
2.
Web
3.
Engenharia de Software
4.
Suporte ao Cálculo de Refinamentos de Programs Concorrentes
5.
Automatic Generation of Verified Hardware
6.
Métodos Formais


Projetos de pesquisa


2011 - 2016
Confiabilidade e Seguran ça em Software Cr ítico Embarcado
Descrição: Sistemas Embarcados têm se tornado cada vez mais comuns no suporte a execução de atividades críticas, tais como controle, monitoração e tomada de decisões, onde falhas podem resultar em perdas ou injúrias a pessoas, ao meio ambiente ou a negócios. Tais sistemas se enquadram no quinto grande desafio da SBC que tem como enfoque o desenvolvimento tecnológico de qualidade de sistemas. O objetivo deste projeto é prover fundamentação teórica e tecnologia para o desenvolvimento de software crítico embarcado correto e seguro, com base na aplicação de técnicas de modelagem formal, transformação, geração automática, verificação de modelos e validação através de teste de software. Serão considerados aspectos e conceitos tais como abstração, tradução de linguagens, independência de plataforma, verificação de propriedades temporais e análise probabilística. As soluções serão aplicadas, prioritariamente, ao domínio aeronáutico, através de cooperação com a empresa Embraer, e de material de transporte metroferroviário, através de uma colaboração com a empresa AeS..
Situação: Concluído; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (1) / Doutorado: (2) .
Integrantes: Marcel Vinicius Medeiros Oliveira - Coordenador / Augusto Sampaio - Integrante / David Deharbe - Integrante / Anamaria Martins Moreira - Integrante / Martin Alejandro Musicante - Integrante / Alexandre Cabral Mota - Integrante / Patricia Duarte de Lima Machado - Integrante.
2011 - Atual
COMPASS
Descrição: The design of innovative products and services that take advantage of Systems of Systems (SoS) technology is in its infancy. It is hampered by the complexity caused by the heterogeneity and independence of SoS constituent systems and the difficulty of communication between diverse stakeholders. The state of the art in SoS engineering lacks models and tools that help developers to make trade-off decisions during design and evolution, and assist in working out and recording precise contracts between constituents and the global SoS. This leads to sub-optimal design and expensive rework during integration and in service. COMPASS will augment existing industry tools and practice with an underlying modelling language in which SoS architectures and contracts can be expressed. A formal semantic foundation ? the first to be developed specifically for SoS engineering ? will enable this language to support analysis of global SoS properties. The language and methods will be supported by an open, extendible tools platform with integrated prototype plug-ins for model construction, dynamic analysis by simulation and test automation, static analysis by model- checking and proof, and links to an established architectural modelling language (SysML). These strengthened foundations and tools will support enhanced methods guidelines that help users embed this new technology in industrial SoS practice. Technical advances in COMPASS are focussed on industry needs evaluated through substantial industry-led case studies in three diverse and complementary areas. These will be augmented by challenge problems solicited from a range of SoS stakeholders and developer organisations through a special interest group. The open platform, tools plug-ins, semantics, development guidelines, industry case study experience and challenge problems will ensure that COMPASS‟s outputs can be readily exploited by SoS developers and stakeholders as well.
Situação: Em andamento; Natureza: Pesquisa.
2008 - 2010
Verified Software Repository - UK Computer Science Grand Challenges
Descrição: Proposto no Reino Unido, este projeto busca a geração de um corpo significante de programas verificados que têm especificações externas precisas, especificações internas completas, e provas mecânicas da corretude com respeito a uma teoria correta de programação..
Situação: Em andamento; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (1) .
Integrantes: Marcel Vinicius Medeiros Oliveira - Coordenador.
2008 - 2010
Combinando Técnicas de Métodos Formais e Teste na Construção de Sistemas Embarcados de Tempo Real
Descrição: Neste projeto focaremos no uso combinado de métodos formais e técnicas de teste baseado em modelos para sistemas embarcados de tempo real. O principal objetivo é compartilhar conhecimentos e experiências para promover avanços conjuntos nesta área de pesquisa. Em particular, procuramos com este projeto promover o desenvolvimento tecnológico de qualidade de sistemas corretos e seguros. O projeto considerará as seguintes direções de pesquisa: (1) investigação de modelos de sistemas de software heterogêneos com características tais como não-determinismo, tempo e interrupção; (2) desenvolvimento de padrões de modelagem para sistemas embarcados utilizando formalismos baseados em estados e processos; (3)proposta de padrões de desenvolvimento baseado em refinamento de modelos baseados em estados e processos; (4) geração automática de código para hardware e software; (5) testes a partir de modelos parciais, considerando sua geração a partir de casos de teste abstratos e comportamento observável; (6) aprimoramento de técnicas atuais para a geração de casos de teste considerando critérios semânticos de cobertura além dos critérios de cobertura estrutural, bem como relações de conformidade pertinentes e critérios de cobertura de verificação de modelos; (7) investigação das relações de conformidade com base em falha e divergência em álgebras de processo; (8) proposta de estratégias para a seleção automática de casos de teste com base em funções de similaridade..
Situação: Em andamento; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (2) / Doutorado: (1) .
Integrantes: Marcel Vinicius Medeiros Oliveira - Integrante / Augusto Sampaio - Coordenador / David Deharbe - Integrante / Anamaria Martins Moreira - Integrante / Alexandre Cabral Mota - Integrante / Juliano Manabu Iyoda - Integrante / Flávia de Almeida Barros - Integrante / Franklin de Souza Ramalho - Integrante / Marcelo Bezerra d'Amorim - Integrante / Patricia Duarte de Lima Machado - Integrante / Paulo Henrique Monteiro Borba - Integrante.Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
Número de produções C, T & A: 2
2006 - 2008
Suporte ao Cálculo de Refinamentos de Programas Concorrentes
Descrição: A grande maioria dos desenvolvimentos de software de hoje não utilizam as teorias e formalismos existentes. Esta falta de uso de formalismos aumenta os custos de desenvolvimento de softwares confiáveis de custo relativamente baixos. As màs experiências com as técnicas informais constituem a principal razão para o uso de métodos formais no processo de desenvolvimento de software. Nas últimas décadas duas escolas têem desenvolvido técnicas formais para um desenvolvimento de software preciso, correto, e consciso. Porém, elas tomaram abordagens diferentes: uma delas focou sua atenção aos aspectos dos dados do sistemas, enquanto a outra focou nos aspectos de comportamento do sistema. Muitas tentativas foram feitas para trazerem estas duas escolas juntas. Porém, até onde sabemos, nenhuma delas tem um cálculo de refinamentos relacionado. É exatamente esta falta de cuporte ao refinamento com um estilo calculacional que motivou a criação de Circus, o qual caracteriza sistemas como processos, os quais agrupam construtores que descrevem o comportamento dos dados e do controle. Na nossa tese de doutourado, nós provemos um cálculo de refinamento para Circus; este cálculo suporta o desenvolvimento formal de uma especificação abstrata centralizada para uma especificação concreta distribuída. Além disso, nós provemos uma estratégia de tradução de Circus para Java e apresentamos um estudo de caso de escala industrial. Como resultado do nosso trabalho, além das leis e de uma estratégia de refinamento, um protótipo de um provador de teoremas para Circus foi desenvolvido. Este protótipo implementa a versão final da semântica de Circus e provê algumas das leis em forma de teoremas que podem ser usados em desenvolvimentos futuros. Um dos objetivos deste projeto de pesquisa é a definição de um conjunto completo de leis de refinamento com o qual podemos ter certeza que se o refinamento não for possível, então a especificação concreta realmente n.
Situação: Concluído; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (3) / Especialização: (0) / Mestrado acadêmico: (0) / Mestrado profissional: (0) / Doutorado: (0) .
Integrantes: Marcel Vinicius Medeiros Oliveira - Coordenador / Artur Oliveira Gomes - Integrante / Alessandro Cavalcante Gurgel - Integrante / Cristiano Gurgel de Castro - Integrante.Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
Número de produções C, T & A: 4
2006 - Atual
CSP2HC
Descrição: CSP is a formalism that can be used to specify distributed reactive systems. It has a large tool support (i.e the FDR model checker) that allows users to formally verify properties such as deadlock freedom and refinement of systems specified in CSP. However, after such verification, there is still the need to implement the system itself, and for this, we still need a link between CSP and a practical programming language. This project aims at the automatic generation of hardware, more specifically FPGA's from CSP specifications. For this, we target at the Handel-C programming language. Handel-C is a programming language designed to enable the compilation of programs into synchronous hardware. Handel-C is not a hardware description language though; rather it is a programming language aimed at compiling high level algorithms directly into gate level hardware (FPGA)..
Situação: Em andamento; Natureza: Pesquisa.
2004 - 2005
Formal Derivation of State-Rich Reactive Programs using Circus
Descrição: The lack of formalism in most software developments can lead to a loss of precision and correctness in the resulting software. Formal techniques of program development have been developed in the past decades and can tackle this problem. Two different approaches have been taken: one focuses on data aspects, and the other focuses on behavioural aspects of the systems. Some combined languages have already been proposed to integrate these two approaches; however, as far as we know, none of them, apart from Circus, includes a refinement calculus. This work presents a method that can be applied in order to achieve a formal derivation of state-rich reactive programs, using Circus, in a calculational style. It extends the existing Circus refinement strategy to reach Java implementation and formalises its refinement calculus. For that we proposed and mechanised a denotational semantics for Circus, which was used to prove over one-hundred and forty refinement laws, many of which were suggested by an industrial case study on which we worked. As far as we know, this is the only mechanised semantics for languages like Circus; the mechanisation of the Circus semantics and its theoretical basis, the Unifying Theories of Programming, are the basis for a theorem prover for \Circus. A translation strategy from Circus to Java is also an important part of this work. Our method is illustrated by the case study: a safety-critical fire control system. So far, this is the largest case study on the Circus refinement calculus. We present the refinement of its abstract centralised specification to a concrete distributed one, and then its translation to Java, using our translation strategy. We believe that this industrial case study provides empirical evidence that the formal development of state-rich reactive processes using Circus is possible in both theory and practice..
Situação: Concluído; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (0) / Especialização: (0) / Mestrado acadêmico: (1) / Mestrado profissional: (0) / Doutorado: (2) .
Integrantes: Marcel Vinicius Medeiros Oliveira - Integrante / Ana Lúcia Caneca Cavalcanti - Integrante / Jim Woodcock - Coordenador / Manuela Xavier - Integrante / Augusto Sampaio - Integrante / Andrew Butterfield - Integrante / Leonardo Freitas - Integrante.Financiador(es): University of York - Bolsa / Engineering and Physical Sciences Research Council - Bolsa.
Número de produções C, T & A: 17
1999 - 2000
ArcAngel: a Tactic Language For Refinement
Descrição: Morgan's refinement calculus is a successful technique for developing software in a precise and consistent way. This technique, however, can be hard to use, as developments may be long and repetitive. Many authors have pointed out that a lot can be gained by identifying commonly used development strategies, documenting them as tactics, and using them as single transformation rules. Also, it is useful to have a notation for describing derivations, so that they can be analysed and modified. In this project, we developed ArcAngel, a language for defining such refinement tactics; we developed the language, its semantics, and some of its algebraic laws. Apart from Angel, a general-purpose tactic language that we extended, no other tactic language has a denotational semantics and proof theory of its own..
Situação: Concluído; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (1) .
Integrantes: Marcel Vinicius Medeiros Oliveira - Integrante / Ana Lúcia Caneca Cavalcanti - Coordenador.Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Bolsa.
Número de produções C, T & A: 4


Projetos de desenvolvimento


2006 - 2006
CSP2HC
Descrição: CSP is a formalism that can be used to specify distributed reactive systems. It has a large tool support (i.e the FDR model checker) that allows users to formally verify properties such as deadlock freedom and refinement of systems specified in CSP. However, after such verification, there is still the need to implement the system itself, and for this, we still need a link between CSP and a practical programming language. This project aims at the automatic generation of hardware, more specifically FPGA's from CSP specifications. For this, we target at the Handel-C programming language. Handel-C is a programming language designed to enable the compilation of programs into synchronous hardware. Handel-C is not a hardware description language though; rather it is a programming language aimed at compiling high level algorithms directly into gate level hardware (FPGA)..
Situação: Concluído; Natureza: Desenvolvimento.
Alunos envolvidos: Graduação: (0) / Especialização: (0) / Mestrado acadêmico: (0) / Mestrado profissional: (0) / Doutorado: (0) .
Integrantes: Marcel Vinicius Medeiros Oliveira - Integrante / Jim Woodcock - Coordenador.Financiador(es): Qinetiq - Remuneração.
2001 - 2002
Gabriel - Extending Refine for the support of tactics
Descrição: Gabriel is tactic editor plugged-in to Refine, a tool that supports program development using Morgan's refinement calculus. Using Refine, the user starts with a formal specification, and repeatedly applies laws of refinement in order to obtain the program which correctly implements the initial formal specification. After each law application, Refine shows to the user the program development, the collected code and the proof obligations generated with the law applications. Refine also allows users to save a program development in order to continue it later. Furthermore, Refine also has the undo and redo operations. Gabriel is activated from Refine. Using Gabriel, the user can: (1) Create a tactic: the user writes a tactic in ASCII ArcAngel; (2) Edit a tactic; (3) Generate a tactic: the system verifies the syntax correctness, and includes the tactic to the list of tactics of Refine. Afterwards, the user can (4) apply the generated tactic in program developments; (5) Remove a tactic; (6) Apply a tactic..
Situação: Concluído; Natureza: Desenvolvimento.
Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (1) .
Integrantes: Marcel Vinicius Medeiros Oliveira - Integrante / Ana Lúcia Caneca Cavalcanti - Coordenador / Manuela Xavier - Integrante.Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Bolsa.
Número de produções C, T & A: 4


Revisor de periódico


2008 - 2008
Periódico: Concurrency and Computation. Practice & Experience
2011 - 2011
Periódico: Theoretical Computer Science
2011 - 2012
Periódico: Formal Aspects of Computing
2012 - 2012
Periódico: Journal of Zhejiang University Science C (Computers & Electronics)
2016 - 2016
Periódico: Science of Computer Programming (Print)
2014 - 2014
Periódico: Science of Computer Programming (Print)


Áreas de atuação


1.
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação.
2.
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodologia e Técnicas da Computação/Especialidade: Engenharia de Software.


Idiomas


Inglês
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.
Alemão
Compreende Bem, Fala Razoavelmente, Lê Razoavelmente, Escreve Razoavelmente.
Espanhol
Compreende Bem, Fala Pouco, Lê Razoavelmente, Escreve Pouco.


Prêmios e títulos


2012
Award of Best Paper of the Communicating Processes Architectures 2012 - 34th WoTUG, WoTUG.
2003
Prestigious Paper Award 2002-2003, University of Kent.


Produções



Produção bibliográfica
Citações

SCOPUS

Artigos completos publicados em periódicos

1.
CONSERVA FILHO, M.S.2018CONSERVA FILHO, M.S. ; OLIVEIRA, M.V.M. ; SAMPAIO, A. ; Cavalcanti, Ana . Compositional and Local Livelock Analysis for CSP. INFORMATION PROCESSING LETTERS, v. 133, p. 21-25, 2018.

2.
OLIVEIRA, M. V. M.2016OLIVEIRA, M. V. M.; ANTONINO, P. ; RAMOS, R. ; SAMPAIO, A. ; MOTA, A. ; ROSCOE, A. W. . Rigorous development of component-based systems using component metadata and patterns. FORMAL ASPECTS OF COMPUTING, v. 28, p. 937-1004, 2016.

3.
REIS, JULIANA TEIXEIRA DA CÂMARA2015REIS, JULIANA TEIXEIRA DA CÂMARA ; HAZIN, IZABEL ; FALCÃO, JORGE TARCÍSIO DA ROCHA ; MEIRA, LUCIANO ; BENDASSOLLI, PEDRO ; GUERRA, AMANDA ; FALCÃO, TACIANA PONTUAL ; GOMES, APUENA VIEIRA ; OLIVEIRA, MARCEL VINÍCIUS MEDEIROS ; RÊGO, JOSÉ IVONILDO DO . Development and Results of an Instrument to Search for Competences and Abilities in Information Technology. Creative Education, v. 06, p. 2384-2396, 2015.

4.
Oliveira, Marcel2013Oliveira, Marcel; Cavalcanti, Ana ; WOODCOCK, JIM . Unifying theories in ProofPower-Z. Formal Aspects of Computing (Internet), v. 25, p. 133-158, 2013.

5.
Zeyda, Frank2012 Zeyda, Frank ; OLIVEIRA, M. V. M. ; Cavalcanti, Ana . Mechanised support for sound refinement tactics. Formal Aspects of Computing, v. 24, p. 127-160, 2012.

6.
Oliveira, Marcel2011 Oliveira, Marcel; Zeyda, Frank ; Cavalcanti, Ana . A tactic language for refinement of state-rich concurrent specifications. Science of Computer Programming (Print), v. 76, p. 792-833, 2011.

7.
OLIVEIRA, M. V. M.;Oliveira, Marcel;OLIVEIRA, MARCEL VINÍCIUS MEDEIROS;OLIVEIRA, M.V.M.2009 OLIVEIRA, M. V. M.; CAVALCANTI, A. L. C. ; WOODCOCK, J. C. P. . A UTP Semantics for Circus. Formal Aspects of Computing, v. 21, p. 3-32, 2009.

8.
Zeyda, Frank2009Zeyda, Frank ; Cavalcanti, Ana ; OLIVEIRA, M. V. M. . Supporting ArcAngel in ProofPower. Electronic Notes in Theoretical Computer Science, v. 259, p. 225-243, 2009.

9.
OLIVEIRA, M. V. M.;Oliveira, Marcel;OLIVEIRA, MARCEL VINÍCIUS MEDEIROS;OLIVEIRA, M.V.M.2008 OLIVEIRA, M. V. M.; CAVALCANTI, A. L. C. . ArcAngelC: a Refinement Tactic Language for Circus. Electronic Notes in Theoretical Computer Science, v. 214, p. 203-229, 2008.

10.
OLIVEIRA, M. V. M.;Oliveira, Marcel;OLIVEIRA, MARCEL VINÍCIUS MEDEIROS;OLIVEIRA, M.V.M.2007OLIVEIRA, M. V. M.; CAVALCANTI, A. L. C. ; WOODCOCK, J. C. P. . A Denotational Semantics for Circus. Electronic Notes in Theoretical Computer Science, v. 187, p. 107-123, 2007.

11.
OLIVEIRA, M. V. M.;Oliveira, Marcel;OLIVEIRA, MARCEL VINÍCIUS MEDEIROS;OLIVEIRA, M.V.M.2005 OLIVEIRA, M. V. M.; CAVALCANTI, A. L. C. ; WOODCOCK, J. C. P. . Formal development of industrial-scale systems. Innovations in Systems and Software Engineering, Springer-Verlag, v. 1, n.2, p. 126-147, 2005.

12.
OLIVEIRA, M. V. M.;Oliveira, Marcel;OLIVEIRA, MARCEL VINÍCIUS MEDEIROS;OLIVEIRA, M.V.M.2003OLIVEIRA, M. V. M.; CAVALCANTI, A. L. C. ; WOODCOCK, J. C. P. . ArcAngel: a Tactic Language for Refinement. Formal Aspects of Computing, England, v. 15, n.1, p. 28-47, 2003.

Livros publicados/organizados ou edições
1.
CAVALHEIRO, S. A. C. (Org.) ; MUSICANTE, M. A. (Org.) ; RIBEIRO, L. (Org.) ; OLIVEIRA, M. V. M. (Org.) . 1a Escola de Informática Teórica e Métodos Formais. 1. ed. Porto Alegre: Sociedade Brasileira de Computação, 2016. v. 1. 175p .

2.
OLIVEIRA, M. V. M.; WOODCOCK, J. C. P. (Org.) . Formal Methods: Foundations and Applications:2th Brazilian Symposium on Formal Methods, SBMF 2009. 1. ed. Heidelberg: Springer Verlag, 2009. v. 1. 349p .

Textos em jornais de notícias/revistas
1.
OLIVEIRA, M. V. M.. Análise do Livro Linguagem, Prova e Lógica. Revista de Sistemas de Informação da Faculdade Salesiana Maria Auxiliadora, p. 53 - 56, 01 dez. 2014.

Trabalhos completos publicados em anais de congressos
1.
OLIVEIRA, N. I. ; OLIVEIRA, M. V. M. ; FALCAO, J. T. R. . An Automated Environment for Teaching Programming Logic on Distance Learning IT Courses. In: 10th International Conference on Computer Supported Education, 2018, Funchal. 10th International Conference on Computer Supported Education. Portugal: SCITEPRESS ? Science and Technology Publications, Lda, 2018. v. 1. p. 267-274.

2.
BARROCAS, S. L. ; OLIVEIRA, M. V. M. . A Sound Operational Semantics for Circus. In: International Conference on Software Engineering Research and Practice - SERP 2017, 2017, Las Vegas. Proceedings of the 2017 International Conference on Software Engineering Research and Practice - SERP 2017. Las Vegas: CSREA Press, 2017. p. 56-61.

3.
PEREIRA, D. I. A. ; OLIVEIRA, M. V. M. ; CONSERVA FILHO, M. S. ; SILVA, S. R. R. . BTS: A Tool for Formal Component-Based Development. In: 13th International Conference on Integrated Formal Methods, 2017, Turim. Proceedings of the 13th International Conference on Integrated Formal Methods - IFM 2017. Switzerland: Springer, 2017. v. 10510. p. 221-226.

4.
CONSERVA FILHO, M. S. ; OLIVEIRA, M. V. M. ; SAMPAIO, A. C. A. ; CAVALCANTI, A. L. C. . Local Livelock Analysis of Component-Based Models. In: 18th International Conference on Formal Engineering Methods, 2016, Tóquio. Formal Methods and Software Engineering - 18th International Conference on Formal Engineering Methods, ICFEM 2016. Heidelberg: Springer International Publishing, 2016. v. 10009. p. 279-295.

5.
REIS, J. T. C. ; SANTOS, A. S. ; FERNANDES, B. ; GOMES, A. V. ; OLIVEIRA, M. V. M. . Percepção de estudantes de curso técnico semipresencial em Tecnologia da Informação de uma Universidade Federal. In: Ctrl+E 2016 - Congresso Regional sobre Tecnologias na Educação, 2016, Natal. Ctrl+E 2016 - Congresso Regional sobre Tecnologias na Educação. Aachen: CEUR - Worskshop Proceedings, 2016. v. 1667. p. 472-482.

6.
PEREIRA, D. I. A. ; OLIVEIRA, M. V. M. ; SILVA, S. R. R. . Tool Support for Formal Component-based Development. In: I Escola de Informática Teórica e Métodos Formais, 2016, Natal. 1a ESCOLA DE INFORMÁTICA TEÓRICA E MÉTODOS FORMAIS. Porto Alegre: Sociedade Brasileira de Computação, 2016. p. 43-52.

7.
BARROCAS, S. L. ; OLIVEIRA, M. V. M. . A Validation Strategy for an Automatic Code Generator using Java Pathfinder. In: 14th International Conference on Software Engineering Research and Practice - SERP 2016, 2016, Las Vegas. Proceedings of the 14th International Conference on Software Engineering Research and Practice - SERP 2016. Las Vegas: CSREA Press, 2016. p. 277-283.

8.
OLIVEIRA, J. D. S. ; SAMPAIO, A. C. A. ; OLIVEIRA, M. V. M. . Constructive Extensibility of Trustworthy Component-Based Systems. In: 30th Annual ACM Symposium on Applied Computing, 2015, Salamanca. Proceedings of the 30th Annual ACM Symposium on Applied Computing. {New York, NY, USA: ACM, 2015.

9.
MACARIO, F. J. S. ; OLIVEIRA, M. V. M. . Hard-wiring CSP Hiding: Implementing Channel Abstraction to Generate Veri ed Concurrent Hardware. In: 18th Brazilian Symposium on Formal Methods, 2015, Belo Horizonte. Formal Methods: Foundations and Applications - 18th Brazilian Symposium on Formal Methods. Heidelberg: Springer-Verlag, 2015. v. 9526. p. 3-18.

10.
ANTONINO, P. R. G. ; OLIVEIRA, M. V. M. ; SAMPAIO, A. C. A. ; KRISTENSEN, K. E. ; BRYANS, J. W. . Leadership Election: An Industrial SoS Application of Compositional Deadlock Verification. In: NASA Formal Methods, 2014, Houston. NASA Formal Methods - 6th International Symposium. Heidelberg: Springer Verlag, 2014. v. 8430. p. 31-45.

11.
OLIVEIRA, M. V. M.; SAMPAIO, A. C. A. ; CONSERVA FILHO, M. S. . Model-checking Circus State-Rich Specifications. In: 11th International Conference on Integrated Formal Methods, IFM 2014, 2014, Bertinoro. 11th International Conference on Integrated Formal Methods, IFM 2014 (LNCS). Heidelberg: Springer, 2014. v. 8739. p. 39-54.

12.
OLIVEIRA, M. V. M.; LEITE, J. C. ; DORIA NETO, A. D. ; ALSINA, P. J. ; HAZIN, I. ; FALCAO, J. T. R. . Using IT Education to Reveal New Horizons: A Large Scale Case Study on Digital and Social Inclusion. In: 5th International Conference on Computer Supported Education, 2013, Aachen. Proceeding of the 5th International Conference on Computer Suppoorted Education. Portugal: SCITEPRESS - Science and Technology Publications, 2013. p. 603-611.

13.
OLIVEIRA, M. V. M.; MEDEIROS JUNIOR, I. S. ; WOODCOCK, J. C. P. . A Verified Protocol to Implement Multi-way Synchronisation and Interleaving in CSP. In: International Conference on Software Engineering and Formal Methods, 2013, Madrid. 11th International Conference on Software Engineering and Formal Methods 2013. Heidelberg: Springer, 2013. v. 8137. p. 46-60.

14.
BARROCAS, S. L. ; OLIVEIRA, M. V. M. . JCircus 2.0: an extension of an automatic translator from Circus to Java. In: Communicating Process Architectures 2012, 2012, Dundee. Communicating Processes Architectures - 34th WoTUG Technical Meeting. England: Open Channel Publishing, 2012. p. 15-36.

15.
OLIVEIRA, M. V. M.; DEHARBE, D. ; CRUZ, L. C. D. S . B to CSP migration: towards a formal and automated model-driven engineering of hardware/software co-design. In: Simpósio Brasileiro de Métodos Formais 2011, 2011, Sáo Paulo. Formal Methods, Foundations and Applications: 14th Brazilian Symposium, SBMF 2011. Heidelberg: Springer-Verlag, 2011. v. 7021. p. 44-59.

16.
WOODCOCK, J. C. P. ; OLIVEIRA, M. V. M. ; BURNS, A. ; WEI, K. . Modelling and Implementing Complex Systems with Timebands. In: 4th IEEE International Conference on Secure System Integration and Reliability Improvement, SSIRI 2010, 2010, Singapore. 4th IEEE International Conference on Secure System Integration and Reliability Improvement, SSIRI 2010. Los Alamitos, CA, USA: IEEE Computer Society, 2010. v. 0. p. 1-13.

17.
COSTA, U. S. ; MEDEIROS JUNIOR, I. S. ; OLIVEIRA, M. V. M. . Specification and Verification of a MPI Implementation for a MP-Soc. In: 7th International Colloquium on Theoretical Aspects of Computing, 2010, Natal. Theoretical Aspects of Computing - ICTAC 2010 (LNCS). Heidelberg: Springer, 2010. v. 6255. p. 168-183.

18.
LEITE, J. C. ; KULESZA, U. ; COSTA, U. S. ; DEHARBE, D. ; PIRES, P. F. ; OLIVEIRA, M. V. M. ; ARANHA, E. . Curso de Engenharia de Software da UFRN. In: III Fórum de Educação em Engenharia de Software - FEES 2010, 2010, Salvador. Anais do Congresso Brasileiro de Software, 2010. v. 5. p. 59-66.

19.
BARROCAS, S. L. ; COELHO, R. de S. ; OLIVEIRA, M. V. M. . JCSPUnit: A JUnit extension for testing JCSP programs. In: 4th Brazilian Workshop on Systematic and Automated Software Testing, 2010, Natal. 4th Brazilian Workshop on Systematic and Automated Software Testing, 2010. p. 101-110.

20.
GOMES, A. O. ; OLIVEIRA, M. V. M. . Formal Development of a Cardiac Pacemaker: from Specification to Code. In: 13th Brazilian Symposium on Formal Methods, 2010, Natal. Formal Methods: Foundations and Applications - 13th Brazilian Symposium on Forma Methods - LNCS 6527. Heidelberg: Springer, 2010. v. 6527. p. 210-225.

21.
GARCIA, A. ; CHAVEZ, C. ; Batista, T. V. ; OLIVEIRA, M. V. M. ; SANTANNA, C. ; RASHID, A. . Composing architectural aspects based on style semantics. In: 8th ACM international conference on Aspect-oriented software development, 2009, Charllotesville. Proceedings of the 8th ACM international conference on Aspect-oriented software development. New York: ACM, 2009. p. 111-122.

22.
GOMES, A. O. ; OLIVEIRA, M. V. M. . Formal Specification of a Cardiac Pacing System. In: Formal Methods 2009, 2009, Eindhoven. FM 2009: Formal Methods. Heidelberg: Springer, 2009. v. 5850. p. 692-707.

23.
Zeyda, Frank ; OLIVEIRA, M. V. M. ; CAVALCANTI, A. L. C. . Supporting ArcAngel in ProofPower. In: REFINE 2009, 2009, Eindhoven. Electronic Notes in Theoretical Computer Science, 2009. v. 259. p. 225-243.

24.
FREIRE, C. J. S. ; PIRES, P. F. ; DELICATO, F. C. ; CAMPOS, M. L. M. ; PIRMEZ, L. ; OLIVEIRA, M. V. M. . Regente: Um Arcabouço para Gerenciamento Eficiente de Orquestrações de Serviços Web. In: 26o. Simpósio Brasileiro de Redes de Computadores, 2008, Rio de Janeiro. 26o. Simpósio Brasileiro de Redes de Computadores. 0: Sociedade Brasileira de Computação, 2008. v. 0. p. 149-162.

25.
OLIVEIRA, M. V. M.; CAVALCANTI, A. L. C. . ArcAngelC: a Refinement Tactic Language for Circus. In: International Refinement Workshop, 2008, Turku. Proceeding of the International Refinement Workshop, 2008.

26.
OLIVEIRA, M. V. M.; GURGEL, A. C. ; de CASTRO, C. G. . CRefine: Support for the Circus Refinement Calculus. In: 6th IEEE International Conference on Software Engineering and Formal Methods, 2008, Cidade do Cabo. 6th International Conference on Software Engineering and Formal Methods. California: IEEE Computer Society Press, 2008. p. 281-290.

27.
OLIVEIRA, M. V. M.; WOODCOCK, J. C. P. . Automatic Generation of Verified Concurrent Hardware. In: 9th International Conference on Formal Engineering Methods, 2007, Boca Raton. 9th International Conference on Formal Engineering Methods (LNCS). Heidelberg: Springer-Verlag, 2007. v. 4789. p. 286-306.

28.
OLIVEIRA, M. V. M.; CAVALCANTI, A. L. C. ; WOODCOCK, J. C. P. . Unifying Theories in ProofPower-Z. In: UTP2006: The first international symposium of unifying theories of programming, 2006, Walworth Castle. UTP2006: The first international symposium of unifying theories of programming (LNCS), 2006. v. 4010. p. 123-140.

29.
OLIVEIRA, M. V. M.; CAVALCANTI, A. L. C. ; WOODCOCK, J. C. P. . Refining Industrial Scale Systems in Circus. In: Communicating Sequential Processes, 2004, Oxford. Communicating Sequential Processes (Concurrent Systems Engineering Series). Oxford: IOS Press, 2004. v. 62. p. 281-310.

30.
OLIVEIRA, M. V. M.; XAVIER, M. ; CAVALCANTI, A. L. C. . Refine and Gabriel: Support for Refinement and Tactics. In: Software Engineering and Formal Methods, 2004, Beijing. Second International Conference on Software Engineering and Formal Methods. Washington: IEEE Computer Society Press, 2004. p. 310-319.

31.
OLIVEIRA, M. V. M.; CAVALCANTI, A. L. C. . From Circus to JCSP. In: International Conference on Formal Engineering Methods, 2004, Seattle. Formal Methods and Software Engineering (LNCS). Heidelberg: Springer Verlag, 2004. v. 3308. p. 320-340.

32.
OLIVEIRA, M. V. M.; CAVALCANTI, A. L. C. . Tactics of Refinement. In: XIV Simpósio Brasileiro de Engenharia de Software, 2000, João Pessoa. XIV Simpósio Brasileiro de Engenharia de Software, 2000. p. 117-132.

Resumos expandidos publicados em anais de congressos
1.
GURGEL, A. C. ; de CASTRO, C. G. ; OLIVEIRA, M. V. M. . Tool Support for the Circus Refinement Calculus. In: ABZ2008 Conference, 2008, Londres. Proceeding of the ABZ 2008 Conference (LNCS). Berlin Heidelberg: Springer-Verlag, 2008. v. 5238. p. 349-349.

2.
GOMES, A. O. ; OLIVEIRA, M. V. M. . Towards a Formal Development of an Artificial Pacemaker. In: Simpósio Brasileiro de Métodos Formais, 2008, Salvador. SBMF 2008 Special Tracks, 2008. p. 17-24.

Resumos publicados em anais de congressos
1.
OLIVEIRA, M. V. M.. The Pacemaker Challenge: Developing Certifiable Medical Devices. In: Dagstuhl Seminar 14062 - The Pacemaker Challenge: Developing Certifiable Medical Devices, 2014, Daghstul. The Pacemaker Challenge: Developing Certifiable Medical Devices (Dagstuhl Seminar 14062). Dagstuhl: Dagstuhl Reports, 2014. v. 4. p. 30-30.

2.
MEDEIROS JUNIOR, I. S. ; OLIVEIRA, M. V. M. ; WOODCOCK, J. C. P. . Hard-wiring CSP Parallelism: Implementing Multi-Synchronisation and Interleaving. In: XV Simpósio Brasileiro de Métodos Formais, 2012, Natal. 15th Brazilian Symposium on Formal Methods, 2012. v. 11. p. 20-30.

3.
CONSERVA FILHO, M. S. ; OLIVEIRA, M. V. M. . Implementing Tactics of Refinement in CRefine. In: SOFTWARE ENGINEERING AND FORMAL METHODS, 2012, Thessaloniki. SOFTWARE ENGINEERING AND FORMAL METHODS - LNCS. Heidelberg: Springer, 2012. v. 7504. p. 342-351.

4.
CONSERVA FILHO, M. S. ; OLIVEIRA, M. V. M. . Extending CRefine to Support Tactics of Refinement. In: Simpósio Brasileiro de Métodos Formais 2011, 2011, Sáo Paulo. Proceedings of the 14. Brazilian Symposium on Formal Methods - SBMF 2011 short papers. São Paulo: ICMC/USP, 2011.

5.
OLIVEIRA, D. ; OLIVEIRA, M. V. M. . Joker: An Animator for Formal Languages. In: Simpósio Brasileiro de Métodos Formais 2011, 2011, São Paulo. Proceedings of the 14. Brazilian Symposium on Formal Methods - SBMF 2011 short papers. São Paulo: ICMC/USP, 2011.

6.
GURGEL, A. C. ; MEDEIROS JUNIOR, V. G. ; OLIVEIRA, M. V. M. ; DEHARBE, D. . Integrating SMT-Solvers in Z and B Tools. In: Abstract State Machines, Alloy, B and Z, 2010, Orford. Second International Conference, ABZ 2010 (LNCS). Heidelberg: Springer Berlin / Heidelberg, 2010. v. 5977. p. 412-413.

Apresentações de Trabalho
1.
OLIVEIRA, M. V. M.; GOMES, A. O. . Modelling the Pacemaker: early results on the pulse generator. 2008. (Apresentação de Trabalho/Conferência ou palestra).

Outras produções bibliográficas
1.
BARKER-PLUMMER, D. ; BARWISE, J. ; ETCHEMENDY, J. ; OLIVEIRA, M. V. M. . Linguagem, Prova e Lógica. Petrópolis: Ensinart, 2014. (Tradução/Livro).

2.
OLIVEIRA, M. V. M.. Formal Derivation of State-rich Reactive Programs using Circus 2005 (Tese de Doutorado).

3.
OLIVEIRA, M. V. M.. A Tactic Language for Refinement and its Tool Support 2002 (Tese de Mestrado).


Produção técnica
Programas de computador sem registro
1.
OLIVEIRA, M. V. M.. CSP2HC. 2006.

2.
OLIVEIRA, M. V. M.. Fire Control System. 2005.

3.
OLIVEIRA, M. V. M.. Expoimovel. 2002.

4.
OLIVEIRA, M. V. M.. Gabriel. 2002.

5.
OLIVEIRA, M. V. M.. P2K. 2001.

6.
OLIVEIRA, M. V. M.. Metro Way Finder. 2000.

7.
OLIVEIRA, M. V. M.; COSTA FILHO, I. G. ; LINS, L. D. ; AQUINO JUNIOR, G. . VVM. 2000.

8.
OLIVEIRA, M. V. M.; CAJUEIRO, A. . Functional and OO Language Compiler. 2000.

9.
OLIVEIRA, M. V. M.; COSTA FILHO, I. G. ; AQUINO JUNIOR, G. ; LINS, L. D. . Lógica Sobre Objetos Geométricos. 1999.

10.
OLIVEIRA, M. V. M.; LINS, L. D. . Basketball Stats. 1999.

11.
OLIVEIRA, M. V. M.; AQUINO JUNIOR, G. ; COSTA FILHO, I. G. ; LINS, L. D. . Serial File Transfer. 1998.

12.
OLIVEIRA, M. V. M.; LINS, L. D. ; AQUINO JUNIOR, G. ; GLASNER, R. H. . Secretária Virtual. 1998.

13.
OLIVEIRA, M. V. M.; GLASNER, R. H. ; LINS, L. D. ; COSTA FILHO, I. G. . Concurrent Threads. 1998.

14.
OLIVEIRA, M. V. M.; CAJUEIRO, A. . Functional Language Compiler. 1997.

15.
OLIVEIRA, M. V. M.. Squares. 1997.

16.
OLIVEIRA, M. V. M.. Colors and Choices. 1996.

17.
OLIVEIRA, M. V. M.; LINS, L. D. ; AQUINO JUNIOR, G. ; COSTA FILHO, I. G. . MMQ. 1996.

Trabalhos técnicos
1.
OLIVEIRA, M. V. M.. ArcAngelC - A Refinement Tactic Language for Circus. 2007.

2.
OLIVEIRA, M. V. M.. Formal Derivation of State-Rich Reactive Programs using Circus - Extended Version. 2005.

3.
OLIVEIRA, M. V. M.. A Refinement Calculus for Circus - Mini-thesis. 2004.

4.
OLIVEIRA, M. V. M.. ArcAngel: tactics examples and their usage. 2002.

5.
OLIVEIRA, M. V. M.. Teste de Usabilidade de REFINE e T-REFINE. 2001.

6.
OLIVEIRA, M. V. M.. Tactics of Refinement. 2000.


Demais tipos de produção técnica
1.
OLIVEIRA, M. V. M.; WOODCOCK, J. C. P. . Brazilian Symposium on Formal Methods. 2009. (Editoração/Anais).

2.
OLIVEIRA, M. V. M.. Derivação Formal de Programas Concorrentes usando Circus. 2006. (Curso de curta duração ministrado/Outra).



Bancas



Participação em bancas de trabalhos de conclusão
Mestrado
1.
DEHARBE, D.; MEDEIROS JUNIOR, V. G.; OLIVEIRA, M. V. M.. Participação em banca de Diego de Azevedo Oliveira. BTestBox: uma ferramenta de teste para implementações B. 2018. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

2.
COSTA, U. S.; MUSICANTE, M. A.; MEDEIROS, S. Q.; OLIVEIRA, M. V. M.; BIGONHA, M. A. S.. Participação em banca de Fred de Castro Santos. Um mecanismo para avaliar consultas livres de contexto em bases de dados em grafos inspirados em analisadores LR(1). 2018. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

3.
MUSICANTE, M. A.; COSTA, U. S.; OLIVEIRA, M. V. M.; MEDEIROS, S. Q.; BIGONHA, M. A. S.. Participação em banca de Ciro Morais Medeiros. Avaliação top-down de Consultas de Caminhos Livres-de-Contexto em Grafos. 2018. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

4.
OLIVEIRA, M. V. M.; LUCENA, M. J. N. R.; FALCAO, J. T. R.; GOMES, A. S.. Participação em banca de Nelson Ion de Oliveira. Um Ambiente Interativo de Apoio ao Ensino de Lógica de Programação nos Cursos Técnicos (EaD) do Instituto Metrópole Digital/UFRN. 2017. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

5.
Oliveira, Marcel; MUSICANTE, M. A.; SAMPAIO, A. C. A.. Participação em banca de Dalay Israel de Almeida Pereira. An Extension of a Tool for the Formal Support for Component-based Development. 2017. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

6.
OLIVEIRA, M. V. M.; SAMPAIO, A. C. A.; MELLO, C. A. B.. Participação em banca de Hugo Leonardo da Silva Araújo. A Process for Sound Conformance Testing of Cyper-Physical Systems. 2017. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

7.
DEHARBE, D.; BONICHON, R. W. A.; GOMES, B. E. G.; OLIVEIRA, M. V. M.. Participação em banca de Paulo Ewerton Gomes Fragoso. Contribuições para o Processo de Verificação de Satisfatibilidade Módulo Teoria em Event-B. 2015. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

8.
OLIVEIRA, M. V. M.; MOTA, A. C.; KREUTZ, M.. Participação em banca de Ivan Soares de Medeiros Júnior. Geração Automática de Hardware a partir de Especificações Formais: Estendendo uma Abordagem de Tradução. 2012. Dissertação (Mestrado em Programa de Pós-Graduação em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

9.
SAMPAIO, A. C. A.; MOTA, A. C.; OLIVEIRA, M. V. M.. Participação em banca de José Dihego da Silva Oliveira. Algebraic Laws for Process Subtyping. 2011. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

10.
MUSICANTE, M. A.; OLIVEIRA, M. V. M.; D., Adolfo. Participação em banca de Samuel Lincoln Magalhães Barrocas. JCircus 2.0: Uma Extensao da ferramenta de traducao de Circus para Java. 2011. Dissertação (Mestrado em Programa de Pós-Graduação em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

11.
MOTA, A. C.; DEHARBE, D.; OLIVEIRA, M. V. M.. Participação em banca de Diego Henrique Oliveira de Souza. Clown: A Generic GUI API for Animating Formal Specifications. 2011. Dissertação (Mestrado em Programa de Pós-Graduação em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

12.
MOREIRA, A. M.; SAMPAIO, A. C. A.; OLIVEIRA, M. V. M.. Participação em banca de MADIEL DE SOUSA CONSERVA FILHO. Estendendo CRefine para o Suporte de Taticas de Refinamento. 2011. Dissertação (Mestrado em Programa de Pós-Graduação em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

13.
ANDRADE, A. M. S.; OLIVEIRA, M. V. M.; DEHARBE, D.. Participação em banca de Stephenson de Sousa Lima Galvão. Modelagem Formal do Sistema Operacional de Tempo Real FreeRTOS Utilizando o Método B. 2010. Dissertação (Mestrado em Programa de Pós-Graduação em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

14.
MOREIRA, A. M.; MOTA, A. C.; COELHO, R. de S.; OLIVEIRA, M. V. M.. Participação em banca de Fernanda de Monteiro de Souza. Geração de Casos de Teste a Partir de Especificações B. 2009. Dissertação (Mestrado em Programa de Pós-Graduação em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

15.
MACIEL, P. R. M.; MOTA, A. C.; OLIVEIRA, M. V. M.. Participação em banca de Joabe Bezerra de Jesus Júnior. Design e Validação Formal de Sistemas de Controle de Voo Fly-by-Wire. 2009. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

16.
LYRA, A.; DIMURO, G. P.; BEDREGAL, B. R. C.; OLIVEIRA, M. V. M.. Participação em banca de Hélida Salles Santos. The Interval Constructor on Classes of ML-Algebras. 2008. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

17.
SILVA, F. S. C.; GUBITOSO, M. D.; OLIVEIRA, M. V. M.. Participação em banca de Álvaro Heiji Miyazawa. Geração Parcial de Código Java a partir de Especificações Formais Z. 2008. Dissertação (Mestrado em Ciências da Computação) - Universidade de São Paulo.

18.
OLIVEIRA, M. V. M.; FIGUEIREDO, J. C. A.; DEHARBE, D.. Participação em banca de Cláudia Fernanda Oliveira Kiermes Tavares. Prova Automática de Satisfabilidade Módulo Teoria Aplicada ao Método B. 2007. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

19.
OLIVEIRA, M. V. M.; DEHARBE, D.; MERZ, S.. Participação em banca de Diego Caminha Barbosa de Oliveira. Deciding Defference Logic in a Nelson-Oppen Combination Framework. 2007. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

20.
OLIVEIRA, M. V. M.; SAMPAIO, A. C. A.; DEHARBE, D.. Participação em banca de Bruno Emerson Gurgel Gomes. BSmart: Desenvolvimento Rigoroso de Aplicações Java Card com Base no Método Formal B. 2007. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

Teses de doutorado
1.
OLIVEIRA, M. V. M.; MUSICANTE, M. A.; COSTA, U. S.; MOTA, A. C.; GOMES, B. E. G.. Participação em banca de Samuel Lincoln Magalhães Barrocas. A Strategy to verify the Code Generation from Circus to Java. 2018. Tese (Doutorado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

2.
SIMAO, A. S.; GAULDEL, M. A. R.; VINCENZI, A. M. R.; OLIVEIRA, M. V. M.; MOREIRA, A. M.. Participação em banca de Alex Donizeti Betez Alberto. Formal mutation testing in Circus process algebra. 2018. Tese (Doutorado em Ciências da Computação e Matemática Computacional) - Universidade de São Paulo.

3.
BORBA, P. H. M.; MOTA, A. C.; TEIXEIRA, L. M.; OLIVEIRA, M. V. M.; SANTIAGO JUNIOR, V. A.. Participação em banca de Lucas Albertins Lima. Formalisation of SysML Design Models and an Analysis Strategy Using Refinement. 2016. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.

4.
DEHARBE, D.; MUSICANTE, M. A.; OLIVEIRA, M. V. M.; MOTA, A. C.; GOMES, B. E. G.. Participação em banca de Valério Gutemberg de Medeiros Júnior. Método B e a Síntese Verificada para Código de Montagem. 2016. Tese (Doutorado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

5.
MOREIRA, A. M.; LEUSCHEL, M.; MOTA, A. C.; MACHADO, P. D. L.; OLIVEIRA, M. V. M.. Participação em banca de Ernesto Cid Brasil de Matos. BETA: a B Based Testing Approach. 2016. Tese (Doutorado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

6.
OLIVEIRA, M. V. M.; MOREIRA, A. M.; MUSICANTE, M. A.; MOTA, A. C.; RIBEIRO, L.. Participação em banca de Madiel de Souza Conserva Filho. Livelock Analysis for Component-Based Systems. 2016. Tese (Doutorado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

7.
DEHARBE, D.; SAMPAIO, A. C. A.; GHEYI, R.; OLIVEIRA, M. V. M.; MOREIRA, A. M.. Participação em banca de Bruno Emerson Gurgel Gomes. Desenvolvimento Formal de Aplicações Smart Cards. 2012. Tese (Doutorado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

8.
SAMPAIO, A. C. A.; MOTA, A. C.; IYODA, J. M.; OLIVEIRA, M. V. M.. Participação em banca de Tiago Lima Massoni. A Model-Driven Approach to Formal Refactoring. 2008. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.

Qualificações de Doutorado
1.
OLIVEIRA, M. V. M.; MUSICANTE, M. A.; COELHO, R. de S.. Participação em banca de Samuel Lincoln Magalhães Barrocas. A strategy to validate the code generator from Circus to Java. 2017. Exame de qualificação (Doutorando em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

2.
DEHARBE, D.; ALMEIDA, J. M.; OLIVEIRA, M. V. M.; FONTAINE, P.. Participação em banca de Haniel Moreira Barbosa. New techniques for instantiation and proof production in SMT solving. 2017. Exame de qualificação (Doutorando em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

3.
Batista, T. V.; OLIVEIRA, M. V. M.; NAKAGAWA, E. Y.; OQUENDO, F.. Participação em banca de Eduardo Alexandre Ferreira Silva. Mission-driven System-of-Systems Architecture Development. 2017. Exame de qualificação (Doutorando em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

4.
BORBA, P. H. M.; OLIVEIRA, M. V. M.; MOTA, A. C.. Participação em banca de Lucas Albertins Lima. Formalisation of SysML Design Models and an Analysis Strategy using Refinement. 2015. Exame de qualificação (Doutorando em Ciências da Computação) - Universidade Federal de Pernambuco.

Qualificações de Mestrado
1.
OLIVEIRA, M. V. M.; GOMES, B. E. G.; MUSICANTE, M. A.. Participação em banca de Dalay Israel de Almeida Pereira. Uma extensão de uma ferramenta para suporte formal ao desenvolvimento baseado em componentes. 2017. Exame de qualificação (Mestrando em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

2.
MUSICANTE, M. A.; OLIVEIRA, M. V. M.; COSTA, U. S.; MEDEIROS, S. Q.. Participação em banca de Ciro Morais Medeiros. Consultas LL em Grafos RDF. 2017. Exame de qualificação (Mestrando em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

3.
ARANHA, E.; Oliveira, Marcel; NUNES, I. D.; MENDES NETO, F. M.. Participação em banca de Alan de Oliveira Santana. Um Sistema Tutor para Ensino de Programação na Educação Básica. 2017. Exame de qualificação (Mestrando em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

4.
DEHARBE, D.; MOREIRA, A. M.; Oliveira, Marcel. Participação em banca de DIEGO DE AZEVEDO OLIVEIRA. BTestBox: uma ferramenta de teste para implementações B. 2017. Exame de qualificação (Mestrando em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

5.
COSTA, U. S.; MUSICANTE, M. A.; OLIVEIRA, M. V. M.; MEDEIROS, S. Q.. Participação em banca de Fred de Castro Santos. Um Mecanismo para Avaliar Consultas Livres de Contexto em Base de Dados em Grafos Inspirado em analisadores LR(1). 2017. Exame de qualificação (Mestrando em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

6.
OLIVEIRA, M. V. M.; GOMES, A. V.; FALCAO, J. T. R.. Participação em banca de Nelson Ion de Oliveira. Ensino de Lógica de Programação nos cursos técnicos semipresenciais do Instituto Metrópole Digital/UFRN: uma proposta de material interativo. 2016. Exame de qualificação (Mestrando em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

7.
DEHARBE, D.; OLIVEIRA, M. V. M.; BONICHON, R. W. A.. Participação em banca de Paulo Ewerton Gomes Fragoso. Contribuições para o Processo de Verificação de Satisfatibilidade Módulo Teoria em Event-B. 2014. Exame de qualificação (Mestrando em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

8.
DEHARBE, D.; KREUTZ, M.; OLIVEIRA, M. V. M.. Participação em banca de Haniel Moreira Barbosa. Formal Verification of PLC Programs using the B Method. 2012. Exame de qualificação (Mestrando em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte.

Trabalhos de conclusão de curso de graduação
1.
FIGUEIRA FILHO, F. M.; BARROCA FILHO, I. M.; OLIVEIRA, M. V. M.. Participação em banca de Rafael Fernandes de Queiroz.Desenvolvimento de um Sistema de Informação Web para Controle de Espaços Físicos. 2016. Trabalho de Conclusão de Curso (Graduação em Engenharia de Software) - Universidade Federal do Rio Grande do Norte.

2.
DEHARBE, D.; OLIVEIRA, M. V. M.; ROCHA, B.. Participação em banca de Haniel Barbosa.Desenvolvendo um Sistema Crítico Através de Formalização de Requisitos Utilizando o Método B. 2010. Trabalho de Conclusão de Curso (Graduação em Ciência da Computação) - Universidade Federal do Rio Grande do Norte.

3.
OLIVEIRA, M. V. M.; DEHARBE, D.; GOMES, B. E. G.. Participação em banca de Artur Oliveira Gomes.Formal Development of a Cardiac Pacemaker: from Specification to Code. 2010. Trabalho de Conclusão de Curso (Graduação em Ciência da Computação) - Universidade Federal do Rio Grande do Norte.

4.
OLIVEIRA, M. V. M.; DEHARBE, D.; MAITELLI, A. L.. Participação em banca de Alessandro Cavalcante Gurgel.Suporte ao Cálculo de Refinamentos de Sstemas Concorrentes. 2009. Trabalho de Conclusão de Curso (Graduação em Engenharia da Computação) - Universidade Federal do Rio Grande do Norte.

5.
DEHARBE, D.; MOREIRA, A. M.; OLIVEIRA, M. V. M.. Participação em banca de Luis Celso Dantas Silveira Cruz.Tradutor B-CSP. 2009. Trabalho de Conclusão de Curso (Graduação em Ciência da Computação) - Universidade Federal do Rio Grande do Norte.

6.
OLIVEIRA, M. V. M.; COSTA, U. S.; GOMES, B. E. G.. Participação em banca de Ivan Soares de Medeiros Júnior.Especificação e Verificação de uma Implementação MPI para MP-Soc. 2009. Trabalho de Conclusão de Curso (Graduação em Ciência da Computação) - Universidade Federal do Rio Grande do Norte.

7.
OLIVEIRA, M. V. M.; MOREIRA, A. M.; DEHARBE, D.. Participação em banca de Katia Karinne de Oliveira Moraes.Geração Automática de APIs para o Desenvolvimento de Aplicações Cliente JavaCard a partir da Especificação Formal. 2007. Trabalho de Conclusão de Curso (Graduação em Ciência da Computação) - Universidade Federal do Rio Grande do Norte.

8.
OLIVEIRA, M. V. M.; DEHARBE, D.; MUSICANTE, M. A.. Participação em banca de Éberton da Silva Marinho.BatCave: Uma Ferramenta de Suporte à Verificação Formal para o Método B. 2007. Trabalho de Conclusão de Curso (Graduação em Ciência da Computação) - Universidade Federal do Rio Grande do Norte.



Participação em bancas de comissões julgadoras
Concurso público
1.
MUSICANTE, M. A.; OLIVEIRA, M. V. M.; CHAVEZ, C.. Comissão Examinadora de Concurso Público de Provas e Títulos. 2010. Universidade Federal do Rio Grande do Norte.

2.
MOREIRA, A. M.; OLIVEIRA, M. V. M.; Santiago, J. S.. Processo Seletivo para Professor Efetivo. 2008. Universidade Federal Rural do Semi-Árido.

Outras participações
1.
Campos, A. M. C.; Goldbarg, E. F. G.; OLIVEIRA, M. V. M.. Comitê de Seleção do Processo Seletivo da Pós-graduação. 2009. Universidade Federal do Rio Grande do Norte.

2.
Canuto, A. M. de P.; Batista, T. V.; Goldbarg, E. F. G.; OLIVEIRA, M. V. M.. Comitê de Seleção do Processo Seletivo da Pós-graduação. 2008. Universidade Federal do Rio Grande do Norte.



Eventos



Participação em eventos, congressos, exposições e feiras
1.
Congresso da Sociedade Brasileira de Computação. 2018. (Congresso).

2.
I Congresso de Iniciação Científica da Educação Básica do RN. Cursos Técnicos em TI do Instituto Metrópole Digital. 2018. (Congresso).

3.
Workshop em Comemoração aos 10 anos do LoLITA.Lógica: Uma Ferramenta Importante para Aplicações de Métodos Formais. 2018. (Oficina).

4.
13th International Conference on Integrated Formal Methods. BTS: A Tool for Formal Component-Based Development. 2017. (Congresso).

5.
1st IEEE Summer School on Smart Cities. 2017. (Outra).

6.
II Escola de Informática Teórica e Métodos Formais. 2017. (Outra).

7.
XX Brazilian Symposium on Formal Methods. 2017. (Simpósio).

8.
14th International Conference on Software Engineering Research and Practice - SERP 2016. A Validation Strategy for an Automatic Code Generator using Java Pathfinder. 2016. (Congresso).

9.
18th International Conference on Formal Engineering Methods. Local Livelock Analysis of Component-Based Models. 2016. (Congresso).

10.
I Escola de Informática Teórica e Métodos Formais.Tool Support for Formal Component-based Development. 2016. (Oficina).

11.
XIX Simpósio Brasileiro de Métodos Formais. 2016. (Simpósio).

12.
18th Brazilian Symposium on Formal Methods (SBMF 2015).Hard-wiring CSP Hiding: Implementing Channel Abstraction to Generate Verified Concurrent Hardware. 2015. (Simpósio).

13.
19th Brazilian Symposium on Programming Languages (SBLP 2015)
. 2015. (Simpósio).

14.
29th Brazilian Symposium on Software Engineering (SBES 2015). 2015. (Simpósio).

15.
98th Brazilian Symposium on Software Components, Architectures and Reuse (SBCARS 2015). 2015. (Simpósio).

16.
VI Congresso Brasileiro de Software: Teoria e Prática (CBSOFT 2015). 2015. (Congresso).

17.

8th Brazilian Symposium on Software Components, Architectures and Reuse (SBCARS 2014). 2014. (Simpósio).

18.
11th International Conference on Integrated Formal Methods, IFM 2014. Model-checking Circus State-Rich Specifications. 2014. (Congresso).

19.
17th Brazilian Symposium on Formal Methods (SBMF 2014). 2014. (Simpósio).

20.
18th Brazilian Symposium on Programming Languages (SBLP 2014)
. 2014. (Simpósio).

21.
28th Brazilian Symposium on Software Engineering (SBES 2014). 2014. (Simpósio).

22.
Dagstuhl Seminar 14062 - The Pacemaker Challenge: Developing Certifiable Medical Devices.The Pacemaker grand challenge: from Specification to Hardware. 2014. (Seminário).

23.
V Congresso Brasileiro de Software: Teoria e Prática (CBSOFT 2014). 2014. (Congresso).

24.
5th International Conference on Computer Supported Education. Using IT Education to Reveal New Horizons: A Large Scale Case Study on Digital and Social Inclusion. 2013. (Congresso).

25.
International Conference on Software Engineering and Formal Methods.A Verified Protocol to Implement Multi-way Synchronisation and Interleaving in CSP. 2013. (Simpósio).

26.
III Congresso Brasileiro de Software: Teoria e Prática (CBSOFT 2012). 2012. (Congresso).

27.
VI Simpósio Brasileiro de Componentes, Arquitetura e Reutilização de Software. 2012. (Simpósio).

28.
XVI Simpósio Brasileiro de Linguagens de Programação. 2012. (Simpósio).

29.
XV Simpósio Brasileiro de Métodos Formais.Hard-wiring CSP Parallelism: Implementing Multi-Synchronisation and Interleaving. 2012. (Simpósio).

30.
XXVI Simpósio Brasileiro de Engenharia de Software (SBES). 2012. (Simpósio).

31.
17th International Symposium on Formal Methods. 2011. (Congresso).

32.
2011 Refinement Workshop. 2011. (Oficina).

33.
II Congresso Brasileiro de Software: Teoria e Prática (CBSOFT 2011). 2011. (Congresso).

34.
Simpósio Brasileiro de Componentes, Arquiteturas e Reutilização de Software. 2011. (Simpósio).

35.
Simpósio Brasileiro de Engenharia de Software. 2011. (Simpósio).

36.
Simpósio Brasileiro de Linguagens de Programação. 2011. (Simpósio).

37.
Simpósio Brasileiro de Métodos Formais 2011. B to CSP Migration: Towards a Formal and Automated Model-Driven Engineering of Hardware/Software Co-design. 2011. (Congresso).

38.
Workshop B 2011. 2011. (Oficina).

39.
XXXI Congresso da Sociedade Brasileira de Computação. 2011. (Congresso).

40.
13th Brazilian Symposium on Formal Methods.Formal Development of a Cardiac Pacemaker: from Specification to Code. 2010. (Simpósio).

41.
22nd IFIP International Conference on Testing Software and Systems. 2010. (Congresso).

42.
4th Brazilian Workshop on Systematic and Automated Software Testing.JCSPUnit: A JUnit extension for testing JCSP programs. 2010. (Oficina).

43.
7th International Colloquium on Theoretical Aspects of Computing. Specification and Verification of a MPI Implementation for a MP-Soc. 2010. (Congresso).

44.
Workshop on Logical and Semantic Framework, with Applications. 2010. (Oficina).

45.
Formal Methods 2009. Formal Specification of a Cardiac Pacing System. 2009. (Congresso).

46.
REFINE 2009.Supporting ArcAngel in ProofPower. 2009. (Oficina).

47.
Simpósio Brasileiro de Métodos Formais. 2009. (Simpósio).

48.
Workshop on Verified Software: Theory, Tools, and Experiments. 2009. (Oficina).

49.
6th IEEE International Conference on Software Engineering and Formal Methods. CRefine: Support for the Circus Refinement Calculus. 2008. (Congresso).

50.
Formal Methods. 2008. (Congresso).

51.
International Refinement Workshop.ArcAngelC: a Refinement Tactic Language for Circus. 2008. (Simpósio).

52.
Logical and Semantic Frameworks and Applications. 2008. (Simpósio).

53.
Simpósio Brasileiro de Métodos Formais. 2008. (Simpósio).

54.
Workshop on Pilot Projects for the Grand Challenge in Verified Software.Modelling the Pacemaker: early results on the pulse generator. 2008. (Oficina).

55.
9th International Conference on Formal Engineering Methods. Automatic Generation of Verified Concurrent Hardware. 2007. (Congresso).

56.
Second Workshop on Logical and Semantic Frameworks, with Applications. 2007. (Oficina).

57.
Simpósio Brasileiro de Métodos Formais. 2007. (Congresso).

58.
XI Simpósio Brasileiro de Linguagens de Programação. 2007. (Simpósio).

59.
3rd International Conference on Graph Transformation. 2006. (Congresso).

60.
First International Symposium on Unifying Theories of Programming.First International Symposium on Unifying Theories of Programming. 2006. (Simpósio).

61.
ICFEM 2006 - 8th International Conference on Formal Engineering Methods. 2006. (Congresso).

62.
Refine 2006 - International Refinement Workshop.Refine 2006 - International Refinement Workshop. 2006. (Oficina).

63.
Simpósio Brasileiro de Métodos Formais. 2006. (Simpósio).

64.
Formal Methods 2006. 2005. (Congresso).

65.
RefineNet Workshop.Unifying Theories in ProofPower-Z. 2005. (Oficina).

66.
25 Years of CSP. 2004. (Encontro).

67.
2nd IEEE International Conference on Formal Engineering and Formal Methods. 2nd IEEE International Conference on Formal Engineering and Formal Methods. 2004. (Congresso).

68.
4th International Conference on Integrated Formal Methods. 2004. (Congresso).

69.
6th International Conference on Formal Engineering Methods - ICFEM04. From Circus to JCSP. 2004. (Congresso).

70.
Communicating Processes Architectures. Communicating Processes Architectures. 2004. (Congresso).

71.
International Conference on Integrated Formal Methods. 2004. (Oficina).

72.
Marktoberdorf Summer School. 2004. (Outra).

73.
RefineNet Workshop. 2004. (Oficina).

74.
SEUJP - CSP.SEUJP - CSP. 2003. (Oficina).

75.
SEUJP - Refinement.SEUJP - Refinement. 2003. (Oficina).

76.
Java Brasil. 2000. (Simpósio).

77.
XIV Simpósio Brasileiro de Engenharia de Software.Simpósio Brasileiro de Engenharia de Software. 2000. (Simpósio).


Organização de eventos, congressos, exposições e feiras
1.
OLIVEIRA, M. V. M.; CACHO, N. A. A. ; Batista, T. V. ; LOPES, F. A. S. ; CAVALCANTE, E. R. S. . 1st IEEE Summer School on Smart Cities. 2017. (Outro).

2.
OLIVEIRA, M. V. M.. XIX Simpósio Brasileiro de Métodos Formais. 2016. (Congresso).

3.
OLIVEIRA, M. V. M.; CAVALHEIRO, S. A. C. ; MUSICANTE, M. A. . I Escola de Informática Teórica e Métodos Formais. 2016. (Outro).

4.
OLIVEIRA, M. V. M.. III Congresso Brasileiro de Software de 2012: Teoria e Prática. 2012. (Congresso).

5.
Batista, T. V. ; MUSICANTE, M. A. ; OLIVEIRA, M. V. M. . XXXI Congresso da Sociedade Brasileira de Computação. 2011. (Congresso).

6.
DEHARBE, D. ; OLIVEIRA, M. V. M. . Workshop on Logical and Semantic Frameworks, with Applications. 2010. (Congresso).

7.
DEHARBE, D. ; OLIVEIRA, M. V. M. . 7th International Colloquium on Theoretical Aspects of Computing. 2010. (Congresso).

8.
OLIVEIRA, M. V. M.. 4th Brazilian Workshop on Systematic and Automated Software Testing. 2010. (Congresso).

9.
OLIVEIRA, M. V. M.. 13th Brazilian Symposium on Formal Methods. 2010. (Congresso).

10.
OLIVEIRA, M. V. M.. 22nd IFIP International Conference on Testing Software and Systems. 2010. (Congresso).

11.
OLIVEIRA, M. V. M.. III Simpósio Brasileiro de Componentes, Arquiteturas e Reutilização de Software. 2009. (Congresso).

12.
OLIVEIRA, M. V. M.; WOODCOCK, J. C. P. . Simpósio Brasileiro de Métodos Formais. 2009. (Congresso).

13.
OLIVEIRA, M. V. M.. Escola Potiguar de Computação e suas Aplicações. 2008. (Outro).

14.
OLIVEIRA, M. V. M.. Simpósio Brasileiro de Linguagens de Programação. 2007. (Congresso).

15.
OLIVEIRA, M. V. M.. Simpósio Brasileiro de Métodos Formais. 2006. (Congresso).

16.
OLIVEIRA, M. V. M.. 3rd International Conference on Graph Transformation. 2006. (Congresso).

17.
OLIVEIRA, M. V. M.. IFM - Integrated Formal Methods. 2004. (Congresso).



Orientações



Orientações e supervisões em andamento
Tese de doutorado
1.
Samuel Licoln Magalhães Barrocas. A Strategy to verify the Code Generation from Circus to Java. Início: 2011. Tese (Doutorado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte. (Orientador).


Orientações e supervisões concluídas
Dissertação de mestrado
1.
Nelson Ion de Oliveira. Um Ambiente Interativo de Apoio ao Ensino de Lógica de Programação nos Cursos Técnicos (EaD) do Instituto Metrópole Digital/UFRN. 2017. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, . Orientador: Marcel Vinicius Medeiros Oliveira.

2.
Dalay Israel de Almeida Pereira. A definir. 2015. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, . Orientador: Marcel Vinicius Medeiros Oliveira.

3.
Madiel de Souza Conserva Filho. Estendendo CRefine para o Suporte de Táticas de Refinamento. 2013. Dissertação (Mestrado em Programa de Pós-Graduação em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. Orientador: Marcel Vinicius Medeiros Oliveira.

4.
Sarah Raquel da Rocha Silva. BTS: uma ferramenta de suporte ao desenvolvimento sistemático de sistemas confiáveis baseados em componentes. 2013. Dissertação (Mestrado em Programa de Pós-Graduação em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. Orientador: Marcel Vinicius Medeiros Oliveira.

5.
Ivan Soares de Medeiros Júnior. Geração Automática de Hardware a partir de Especificações Formais: Estendendo uma Abordagem de Tradução. 2012. Dissertação (Mestrado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, . Orientador: Marcel Vinicius Medeiros Oliveira.

6.
Diego Henrique Oliveira de Souza. Joker: An Animator for Formal Languages. 2011. Dissertação (Mestrado em Programa de Pós-Graduação em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. Orientador: Marcel Vinicius Medeiros Oliveira.

7.
Samuel Lincoln Magalhães Barrocas. JCircus 2.0: Uma extensão da Ferramenta de Tradução de Circus para Java. 2011. Dissertação (Mestrado em Programa de Pós-Graduação em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. Orientador: Marcel Vinicius Medeiros Oliveira.

Tese de doutorado
1.
Madiel de Souza Conserva Filho. Livelock Analysis for Component-Based Systems. 2017. Tese (Doutorado em Sistemas e Computação) - Universidade Federal do Rio Grande do Norte, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. Orientador: Marcel Vinicius Medeiros Oliveira.

Trabalho de conclusão de curso de graduação
1.
Wendell Pamplona Barreto. Especificação e Desenvolvimento do Sistema de Gestão de Produção Multimídia (Gema) para o Instituto Metrópole Digital. 2016. Trabalho de Conclusão de Curso. (Graduação em Engenharia de Software) - Universidade Federal do Rio Grande do Norte. Orientador: Marcel Vinicius Medeiros Oliveira.

2.
Francisco José Silva Macário. Uma Implementação Veri ficada de Abstração CSP. 2015. Trabalho de Conclusão de Curso. (Graduação em Engenharia de Software) - Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: Marcel Vinicius Medeiros Oliveira.

3.
Dalay Israel de Almeida Pereira. Inclusão de Suporte a Metadados a Uma Ferramenta de Suporte Formal ao Desenvolvimento Baseado em Componentes. 2015. Trabalho de Conclusão de Curso. (Graduação em Engenharia de Software) - Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: Marcel Vinicius Medeiros Oliveira.

4.
Artur Oliveira Gomes. Formal Development of a Cardiac Pacemaker: from Specification to Code. 2010. Trabalho de Conclusão de Curso. (Graduação em Ciência da Computação) - Universidade Federal do Rio Grande do Norte. Orientador: Marcel Vinicius Medeiros Oliveira.

5.
Alessandro Cavalcante Gurgel. Suporte ao Cálculo de Refinamentos de Sistemas Concorrentes. 2009. Trabalho de Conclusão de Curso. (Graduação em Engenharia da Computação) - Universidade Federal do Rio Grande do Norte, PRH - Petrobras. Orientador: Marcel Vinicius Medeiros Oliveira.

6.
Luis Celso Dantas Silveira Cruz. Tradutor B-CSP. 2009. Trabalho de Conclusão de Curso. (Graduação em Ciência da Computação) - Universidade Federal do Rio Grande do Norte. Orientador: Marcel Vinicius Medeiros Oliveira.

7.
Ivan Soares de Medeiros Júnior. Especificação e Verificação de uma Implementação MPI para MP-Soc. 2009. Trabalho de Conclusão de Curso. (Graduação em Ciência da Computação) - Universidade Federal do Rio Grande do Norte. Orientador: Marcel Vinicius Medeiros Oliveira.

Iniciação científica
1.
Alessandro Cavalcante Gurgel. Suporte ao Cálculo de Refinamentos de Programas Concorrentes. 2008. Iniciação Científica. (Graduando em Engenharia da Computação) - Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: Marcel Vinicius Medeiros Oliveira.

2.
Artur Oliveira Gomes. Suporte ao Cálculo de Refinamentos de Programas Concorrentes. 2008. Iniciação Científica. (Graduando em Ciência da Computação) - Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: Marcel Vinicius Medeiros Oliveira.

3.
Cristiano Gurgel de Castro. Suporte ao Cálculo de Refinamentos de Programas Concorrentes. 2008. Iniciação Científica. (Graduando em Engenharia da Computação) - Universidade Federal do Rio Grande do Norte, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: Marcel Vinicius Medeiros Oliveira.



Educação e Popularização de C & T



Organização de eventos, congressos, exposições e feiras
1.
OLIVEIRA, M. V. M.. III Congresso Brasileiro de Software de 2012: Teoria e Prática. 2012. (Congresso).




Página gerada pelo Sistema Currículo Lattes em 20/10/2018 às 17:12:01