A behaviour model of the SopCast users. - Alex Borges Vieira; Pedro de Carvalho Gomes; Marcus Vinicius de Melo Rocha; Jussara M. Almeida; Sérgio Vale Aguiar Campos (WebMedia, 2009)

Verification of P2P live streaming systems using symmetry-based semiautomatic abstractions. - Pedro de Carvalho Gomes; Sérgio Vale Aguiar Campos; Alex Borges Vieira (HPCS, 2012)

Sound Control-Flow Graph Extraction for Java Programs with Exceptions. - Afshin Amighi; Pedro de Carvalho Gomes; Dilian Gurov; Marieke Huisman (SEFM, 2012)

Characterizing SopCast client behavior. - Alex Borges Vieira; Pedro de Carvalho Gomes; José Augusto Miranda Nacif; Rodrigo Mantini; Jussara M. Almeida; Sérgio Vale Aguiar Campos (Comput. Commun., 2012)

SopCast P2P live streaming: live session traces and analysis. - Alex Borges Vieira; Ana Paula Couto da Silva; Francisco Henrique; Glauber D. Gonçalves; Pedro de Carvalho Gomes (MMSys, 2013)

Sound Control Flow Graph Extraction from Incomplete Java Bytecode Programs. - Pedro de Carvalho Gomes; Attilio Picoco; Dilian Gurov (FASE, 2014)

Automatic Extraction of Program Models for Formal Software Verification. - Pedro de Carvalho Gomes (2015)

Specification and Verification of Synchronization with Condition Variables. - Pedro de Carvalho Gomes; Dilian Gurov; Marieke Huisman (FTSCS, 2016)

Provably correct control flow graphs from Java bytecode programs with exceptions. - Afshin Amighi; Pedro de Carvalho Gomes; Dilian Gurov; Marieke Huisman (Int. J. Softw. Tools Technol. Transf., 2016)

Specification and verification of synchronization with condition variables. - Pedro de Carvalho Gomes; Dilian Gurov; Marieke Huisman; Cyrille Artho (Sci. Comput. Program., 2018)