Pedro de Carvalho Gomes

Has Doctorate (Teknologie doktorsexamen. 2015) and doctoral Licentiate (Teknologie Licentiatsexamen, 2012) in Computer Science from KTH Royal Institute of Technology. Has Master (2010) and Bachelor (2003) in Computer Science from UFMG Federal University of Minas Gerais. Has experience in Computer Science, focusing on Analysis of Algorithms and Computational Complexity, acting on the following subjects: static analysis, software verification, program models, formal semantics and compositional verification.

Informações coletadas do Lattes em 27/09/2025

Acadêmico

Formação acadêmica

Doutorado em Doctoral Program in Computer Science

2010 - 2015

Royal Institute Of Technology
Título: Automatic Extraction of Program Models for Formal Software Verification
Orientador: Dilian Gurov
Coorientador: Mads Dam. Palavras-chave: Software Verification; static analysis; Program Models; Petri Nets; compositional verification; Concurrency. Grande área: Ciências Exatas e da TerraGrande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação / Especialidade: Linguagem Formais e Autômatos. Grande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodologia e Técnicas da Computação / Especialidade: Verificação Formal. Setores de atividade: Atividades dos serviços de tecnologia da informação.

Doutorado em Doctoral Licentiate

2010 - 2012

Royal Institute Of Technology
Título: Sound Modular Extraction of Control Flow Graphs from Java Bytecode
Orientador: Dilian Gurov
Coorientador: Mads Dam. Palavras-chave: Software Verification; static analysis; Program Models; compositional verification.Grande área: Ciências Exatas e da TerraSetores de atividade: Pesquisa e desenvolvimento científico.

Mestrado em Ciências da Computação

2008 - 2010

Universidade Federal de Minas Gerais
Título: Verification of Symmetric Models Using Semiautomatic Abstractions,Ano de Obtenção: 2010
Sérgio Vale de Aguiar Campos.Bolsista do(a): Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPq, Brasil. Palavras-chave: verificação; model checking; verificação formal; p2p.Grande área: Ciências Exatas e da TerraGrande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação / Especialidade: Linguagem Formais e Autômatos. Grande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodologia e Técnicas da Computação / Especialidade: Verificação Formal. Setores de atividade: Pesquisa e desenvolvimento científico.

Graduação em Ciência da Computação

1999 - 2003

Universidade Federal de Minas Gerais
Título: Detecção de Informação Redundante em Máquinas de Busca
Orientador: Nivio Ziviani

Idiomas

Inglês

Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.

Espanhol

Compreende Bem, Fala Bem, Lê Razoavelmente, Escreve Razoavelmente.

Português

Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.

Suéco

Compreende Razoavelmente, Fala Razoavelmente, Lê Razoavelmente, Escreve Razoavelmente.

Áreas de atuação

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Teoria da Computação/Especialidade: Análise de Algoritmos e Complexidade de Computação.

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

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Sistemas de Computação/Especialidade: Software Básico.

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Sistemas de Computação/Especialidade: Arquitetura de Sistemas de Computação.

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação.

Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Matemática da Computação/Especialidade: Modelos Analíticos e de Simulação.

Organização de eventos

de Carvalho Gomes, Pedro ; SOLEIMANIFARD, S. ; CANO, G. R. . 2nd Doctoral Retreat in the Computer Science program at CSC / KTH (DRinCS). 2014. (Congresso).

de Carvalho Gomes, Pedro ; WENNER, C. ; MEENA, R. . 1st Doctoral Retreat in the Computer Science program at CSC / KTH (DRINCS). 2012. (Congresso).

Participação em eventos

Forum Internacional do Software Livre. 2004. (Congresso).

Orientou

Attilio Picoco

Modular Extraction of Control-Flow Graphs from Java Bytecode; 2012; Dissertação (Mestrado em Master Program) - Royal Institute of Technology,; Orientador: Pedro de Carvalho Gomes;

Produções bibliográficas

Amighi, Afshin ; GOMES, Pedro de Carvalho ; Gurov, Dilian ; Huisman, Marieke . Provably correct control flow graphs from Java bytecode programs with exceptions. International Journal on Software Tools for Technology Transfer (Print) , v. N/A, p. 1-32, 2015.
BORGES, ALEX ; GOMES, PEDRO ; NACIF, JOSÉ ; MANTINI, RODRIGO ; ALMEIDA, JUSSARA M. ; CAMPOS, SÉRGIO . Characterizing SopCast client behavior. Computer Communications , v. 35, p. 1004-1016, 2012.
Carvalho Gomes, Pedro ; Picoco, Attilio ; Gurov, Dilian . Sound Control Flow Graph Extraction from Incomplete Java Bytecode Programs. In: Stefania Gnesi; Arend Rensink. (Org.). Lecture Notes in Computer Science. 1ed.: Springer Berlin Heidelberg, 2014, v. 8411, p. 215-229.
Amighi, Afshin ; C. Gomes, Pedro ; Gurov, Dilian ; Huisman, Marieke . Sound Control-Flow Graph Extraction for Java Programs with Exceptions. In: George Eleftherakis, Mike Hinchey, Mike Holcombe. (Org.). Lecture Notes in Computer Science. 1ed.: Springer Berlin Heidelberg, 2012, v. 7504, p. 33-47.
VIEIRA, ALEX BORGES ; DA SILVA, ANA PAULA COUTO ; HENRIQUE, FRANCISCO ; GONCALVES, GLAUBER ; de Carvalho Gomes, Pedro . SopCast P2P live streaming. In: the 4th ACM Multimedia Systems Conference, 2013, Oslo. Proceedings of the 4th ACM Multimedia Systems Conference on - MMSys '13. New York: ACM Press, 2013. p. 125.
de Carvalho Gomes, Pedro ; VIEIRA, ALEX BORGES . Verification of P2P live streaming systems using symmetry-based semiautomatic abstractions. In: 2012 International Conference on High Performance Computing & Simulation (HPCS), 2012, Madrid. 2012 International Conference on High Performance Computing & Simulation (HPCS). p. 343.
VIEIRA, ALEX BORGES ; GOMES, PEDRO ; ROCHA, MARCUS ; ALMEIDA, JUSSARA ; CAMPOS, SERGIO . A behaviour model of the SopCast users. In: the XV Brazilian Symposium, 2009, Fortaleza. Proceedings of the XV Brazilian Symposium on Multimedia and the Web - WebMedia '09. New York: ACM Press, 2009. p. 1.

Outras produções

AMIGHI, A. ; de Carvalho Gomes, Pedro ; GUROV, D. ; HUISMAN, M. . Provably Correct Control-Flow Graphs from Java programs with Exceptions.. 2012. (Relatório de pesquisa).

de Carvalho Gomes, Pedro ; PICOCO, A. ; GUROV, D. . Sound Extraction of Control-Flow Graphs from open Java Bytecode Systems.. 2012. (Relatório de pesquisa).

Projetos de pesquisa

2008 - 2010

Verificação automática de Sistemas Industriais de Larga Escala, Descrição: O projeto de pesquisa tem como objetivo o desenvolvimento de técnicas e metodologias que possibilitem a verificação automática da correção de sistemas industriais altamente complexos utilizando ferramentas de Model Checking.. , Situação: Em andamento; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) / Especialização: (0) / Mestrado acadêmico: (1) / Mestrado profissional: (0) / Doutorado: (0) . , Integrantes: Pedro de Carvalho Gomes - Coordenador., Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Bolsa.

Histórico profissional

Endereço profissional

Royal Institute of Technology, School of Computer Science and Communication, Theoretical Computer Science department. , Lindstedtsvägen 3, KTH Main Campus, 10044 - Stockholm, - Suécia, Telefone: (0046) 87906853, URL da Homepage:

Experiência profissional

2013 - Atual

Royal Institute Of Technology

Vínculo: , Enquadramento Funcional: Estudande de doutorado, Carga horária: 40, Regime: Dedicação exclusiva.

2010 - 2013

Royal Institute Of Technology

Vínculo: Bolsista, Enquadramento Funcional: Estudande de doutorado, Carga horária: 40, Regime: Dedicação exclusiva.

2008 - 2010

Universidade Federal de Minas Gerais

Vínculo: Bolsista de Mestrado, Enquadramento Funcional: Mestrando em Ciência da Computação, Carga horária: 40

2005 - 2006

Ericsson Telecomunicações - Matriz

Vínculo: Colaborador, Enquadramento Funcional: Analista de Telecomunicações Pleno, Carga horária: 40

2006 - 2008

Telemar Norte/Leste SA

Vínculo: Colaborador, Enquadramento Funcional: Analista de Sistemas Pleno, Carga horária: 40

2003 - 2005

Fundação para Inovações Tecnológicas

Vínculo: Colaborador, Enquadramento Funcional: Engenheiro d Software Junior, Carga horária: 40

Atividades

09/2004 - 06/2005
Pesquisa e desenvolvimento , Sede Recife, .,Linhas de pesquisa
10/2003 - 09/2004
Pesquisa e desenvolvimento , Fundação Para Inovações Tecnológicas, .,Linhas de pesquisa

2009 - 2009

Fundação Universidade de Itaúna

Vínculo: Professor vistante, Enquadramento Funcional: Professor Auxiliar, Carga horária: 4

Atividades

02/2009 - 07/2009
Ensino, Ciências Contábeis, Nível: Graduação,Disciplinas ministradas, Introdução à Computação

2001 - 2003

Akwan Information Technologies

Vínculo: Estagiário, Enquadramento Funcional: , Carga horária: 20

Atividades

10/2002 - 08/2003
Estágios , Akwan Information Technologies, .,Estágio realizado, Desenvolvimento de sistemas de busca.
09/2001 - 10/2002
Estágios , Akwan Information Technologies, .,Estágio realizado, Projeto Computador Popular.

2001 - 2001

Avati Segurança Digital Avançada

Vínculo: Funcionário, Enquadramento Funcional: , Carga horária: 30

2002 - 2002

Colégio Técnico de Minas Gerais

Vínculo: Professor substituto, Enquadramento Funcional: , Carga horária: 0

Atividades

04/2002 - 08/2002
Ensino,,Disciplinas ministradas, Introdução a Sistemas Operacionais com ênfase em Linux

2000 - 2001

Prointernet do Brasil

Vínculo: Contrato de Estágio, Enquadramento Funcional: Estágiário, Carga horária: 30

Atividades

08/2000 - 02/2001
Estágios , Prointernet do Brasil, .,Estágio realizado, Estágio com desenvolvedor e administrador de sistemas Unix e Linux.
05/2000 - 07/2000
Estágios , Prointernet do Brasil, .,Estágio realizado, Estágio como analista de suporto.