FELIPE RODRIGUES MONTEIRO SOUSA

Formação complementar

Idiomas

Áreas de atuação

Participação em eventos

Produções bibliográficas

• MONTEIRO, FELIPE R. ; GARCIA, MÁRIO A. P. ; CORDEIRO, LUCAS C. ; DE LIMA FILHO, EDDIE B. . Bounded model checking of C++ programs based on the Qt cross-platform framework. SOFTWARE TESTING VERIFICATION & RELIABILITY , v. 27, p. e1632, 2017.

• MONTEIRO, FELIPE R. ; DA S. ALVES, ERICKSON H. ; SILVA, ISABELA S. ; ISMAIL, HUSSAMA I. ; CORDEIRO, LUCAS C. ; DE LIMA FILHO, EDDIE B. . ESBMC-GPU A Context-Bounded Model Checking Tool to Verify CUDA Programs. SCIENCE OF COMPUTER PROGRAMMING , v. 152, p. 63-69, 2017.

• MONTEIRO, FELIPE R. ; JANUÁRIO, FRANCISCO A.P. ; CORDEIRO, LUCAS C. ; DE LIMA FILHO, EDDIE B. . BMCLua. SOFTWARE ENGINEERING NOTES , v. 42, p. 1-10, 2017.

• PEREIRA, PHILLIPE ; ALBUQUERQUE, HIGO ; DA SILVA, ISABELA ; MARQUES, HENDRIO ; MONTEIRO, Felipe ; FERREIRA, RICARDO ; CORDEIRO, LUCAS . SMT-based context-bounded model checking for CUDA programs. CONCURRENCY AND COMPUTATION-PRACTICE & EXPERIENCE , v. 29, p. e3934, 2016.

• GADELHA, M. Y. R. ; Felipe R. Monteiro ; MORSE, J. ; CORDEIRO, LUCAS C. ; FISCHER, BERND ; NICOLE, D. A. . ESBMC 5.0: An Industrial-Strength C Model Checker. In: 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE), 2018, Montpellier. 2018 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE), 2018. p. 887-890.

• GADELHA, M. Y. R. ; Felipe R. Monteiro ; CORDEIRO, LUCAS C. ; NICOLE, D. A. . Towards Counterexample-guided k-Induction for Fast Bug Detection. In: 25th ACM SIGSOFT International Symposium on the Foundations of Software Engineering (FSE), 2018. 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (ESEC/FSE), 2018.

• MONTEIRO, FELIPE R. ; PEREIRA, PHILLIPE A. ; CORDEIRO, LUCAS C. ; FILHO, CICERO F. F. COSTA ; COSTA, MARLY G. F. . Complementary training programme for electrical and computer engineering students through an industrial-academic collaboration. In: 2016 IEEE Frontiers in Education Conference (FIE), 2016, Eire. 2016 IEEE Frontiers in Education Conference (FIE). p. 1-9.

• GARCIA, MÁRIO A. P. ; Felipe R. Monteiro ; CORDEIRO, L. C. ; DE LIMA FILHO, EDDIE B. . ESBMCQtOM: A Bounded Model Checking Tool to Verify Qt Applications. In: International Symposium on Model Checking Software, 2016, Eindhoven. Model Checking Software. Cham: Springer, 2016. v. 9641. p. 97-103.

• Felipe R. M. Sousa ; CORDEIRO, L. C. ; L. FILHO, E. B. . Verificação de Programas C++ Baseados no Framework Multiplataforma Qt. In: ENCOSIS, 2015, Manaus. IV Encontro Regional de Computação e Sistemas de Informação. Manaus, 2015. v. 4. p. 181-190.

• SOUSA, FELIPE R. M. ; CORDEIRO, LUCAS C. ; DE LIMA FILHO, EDDIE B. . Bounded model checking of C++ programs based on the Qt framework. In: 2015 IEEE 4th Global Conference on Consumer Electronics (GCCE), 2015, Osaka. 2015 IEEE 4th Global Conference on Consumer Electronics (GCCE). p. 179-447.

• RAMALHO, MIKHAIL ; FREITAS, MAURO ; SOUSA, FELIPE ; MARQUES, HENDRIO ; CORDEIRO, LUCAS ; FISCHER, BERND . SMT-Based Bounded Model Checking of C++ Programs. In: 2013 20th IEEE International Conference and Workshops on Engineering of Computer Based Systems (ECBS), 2013, Scottsdale. 2013 20th IEEE International Conference and Workshops on Engineering of Computer Based Systems (ECBS). p. 147.

• SOUSA, F. R. M. ; COSTA, E. A. B. ; CASTRO, THAIS HELENA CHAVES DE . WorldTour: Software para Suporte no Ensino de Crianças Autistas. In: Congresso Brasileiro de Informática na Educação (CBIE 2012), 2012, Rio de Janeiro. 23º Simpósio Brasileiro de Informática na Educação (SBIE), 2012.

• Felipe R. Monteiro ; GARCIA, MÁRIO A. P. ; CORDEIRO, LUCAS C. ; DE LIMA FILHO, EDDIE B. . Bounded Model Checking of C++ Programs based on the Qt Cross-Platform Framework (First-Journal Abstract). In: 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE), 2018, Montpellier. 2018 33rd IEEE/ACM International Conference on Automated Software Engineering (ASE), 2018. p. 953.

• MONTEIRO, FELIPE R. . Bounded model checking of state-space digital systems: the impact of finite word-length effects on the implementation of fixed-point digital controllers based on state-space modeling. In: the 2016 24th ACM SIGSOFT International Symposium, 2016, Seattle. Proceedings of the 2016 24th ACM SIGSOFT International Symposium on Foundations of Software Engineering - FSE 2016. New York: ACM Press. p. 1151-1153.

• SOUSA, F. R. M. ; CASTRO, THAIS HELENA CHAVES DE . WorldTour: Towards an Adaptive Software to Support Children with Autism in Tour Planning, 2012. v. I. p. 368-368.

Outras produções

Projetos de pesquisa

• 2015 - 2016

  Verificação de Controladores Digitais de Ponto Fixo Representados por Espaço de Estados, Descrição: Em sistemas controlados por computador, o computador faz as funções dos componentes eletrônicos nos clássicos sistemas de controle analógico, a computação de erros, bem como a execução de algoritmos de controle. Os controladores digitais são amplamente utilizados pela comunidade de engenharia de controle devido às várias vantagens sobre os controladores analógicos, tais como a melhoria da confiabilidade, sensibilidade, flexibilidade e custo. No entanto, existem algumas desvantagens no uso de controladores digitais, como por exemplo, os erros que são introduzidos durante o processo de quantização. Neste contexto, existem algumas iniciativas para resolver os problemas que aparecem no domínio de tempo discreto, e em particular, os problemas relacionados com o comprimento finito da palavra. Portanto, o cenário mencionado requer uma melhor compreensão e um melhor tratamento dos problemas típicos relacionados aos controladores digitais para que a quantização e os efeitos do comprimento da palavra sejam, potencialmente, reduzidos durante o projeto do controlador digital. Este trabalho visa descrever uma metodologia de verificação, apoiada pelo Digital System Verifier (DSVerifier), que é uma ferramenta para verificar propriedades relacionadas ao overflow, ciclo-limite, restrições temporais, estabilidade e fase mínima na implementação de controladores digitais. Através do DSVerifier, os engenheiros de controle podem verificar que o controlador digital concebido apresenta o desempenho desejado, quando ele é incorporado em um determinado hardware com certas limitações de recursos. Desta forma, este projeto visa ampliar a automação do processo de verificação com o DSVerifier através do suporte à verificação de controladores digitais representados em espaço de estado. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) . , Integrantes: Felipe Rodrigues Monteiro Sousa - Integrante / Lucas Carvalho Cordeiro - Coordenador.

• 2014 - 2014

  FoldSynth: Estudo de uma Plataforma Interativa de Última Geração para Visualização Molecular, Descrição: Através da utilização de um modelo simples de forças moleculares, FoldSynth oferece uma animação do processo de docking e folding em tempo real. Na verdade, FoldSynth é uma plataforma multimídia interativa projetada para ajudar a entender as características de fios moleculares com ênfase em proteínas. Como uma visualização em 3D, a forma de um fio molecular é mostrado flutuando acima de uma matriz 2D que representa restrições de distância, mapa de contato ou outras características do par residual. A visualização 2D também é interativa, e pode ser usada mesmo para criar novas moléculas. Neste trabalho, o FoldSynth é estudado a fim de identificar abordagens para expandir as características de uma versão JavaScript do mesmo com base em outra versão em Java. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) . , Integrantes: Felipe Rodrigues Monteiro Sousa - Integrante / Frederic Fol Leymarie - Coordenador.

• 2012 - 2013

  Verificação Formal de Programas C++ que Usam o Framework Multi-Plataforma Qt, Descrição: Este trabalho de pesquisa tem como objetivo implementar uma estrutura simplificada com a finalidade de verificar a utilização de cada método do framework Qt e integrá-la no verificador ESBMC. Nesta pesquisa, pretende-se verificar de forma automática aplicações reais desenvolvidas na linguagem C++ que utilizem o framework Qt. A metodologia empregada nesta pesquisa pode ser dividia em três etapas principais. Primeiramente, iremos realizar uma revisão da literatura a respeito da teoria de Verificação de Modelos. Nesta etapa, a maioria dos conceitos importantes acerca de Lógica Proposicional, Lógica Temporal Linear (LTL), Lógica de Árvore de Computação (CTL) serão estudados com o intuito de entender o funcionamento do verificador ESBMC. Esta parte contemplará também um estudo aprofundado sobre o framework Qt, onde o acadêmico realizará análises sistemáticas de códigos que utilizam este framework. A partir do conteúdo estudado, nesta etapa será construída uma estrutura simplificada do framework, com as bibliotecas e os métodos mais utilizados. Essa estrutura será montada a partir da implementação das bibliotecas definidas com as assinaturas dos seus métodos e definições de tipos. Finalmente, iremos modelar os métodos definidos na estrutura simplificada, de forma que possa ser checada todas as propriedades do mesmo, e assim validar o seu uso. Vários testes serão realizados nessa etapa para validar o fato de que as implementações desenvolvidas possam ser aplicadas em sistemas reais. Após finalizada a modelagem, todas as implementações serão integradas no nosso verificador de software ESBMC. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (1) . , Integrantes: Felipe Rodrigues Monteiro Sousa - Integrante / Lucas Carvalho Cordeiro - Coordenador., Número de produções C, T & A: 1

• 2011 - 2013

  Verificação Contínua de Programas C++ Empregando SMT-based Bounded Model Checking, Descrição: O objetivo principal deste projeto é estender o verificador de modelos ESBMC para suportar a verificação de programas C++ e depois integrá-lo no processo de engenharia de software do Instituto NOKIA de Tecnologia (INdT) através de práticas de exploração, como o desenvolvimento incremental e testes de regressão. Em particular, pretende-se definir um modelo de objeto para capturar a semântica dos programas C++ e então integrá-lo ao verificador de modelos ESBMC. Depois disso, pretendemos aplicar o conceito de verificação contínua juntamente com ESBMC para verificar aplicações reais em C++. A abordagem de verificação contínua combina ideias existentes de engenharia de software (por exemplo, integração contínua) e verificação formal (por exemplo, verificação de equivalência) visando detectar automaticamente erros de projeto e problemas de integração o mais rápido possível, explorando informações do gerenciamento de configuração de software, sistematicamente focando o esforço de verificação de funções novas ou modificadas. Pretendemos usar verificação de equivalência para determinar se as funções modificadas precisam ser reverificadas formalmente e usar casos de teste existentes para reduzir o espaço de busca para o verificador, combinando assim a verificação dinâmica e estática. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (2) . , Integrantes: Felipe Rodrigues Monteiro Sousa - Integrante / Lucas Carvalho Cordeiro - Coordenador / Mikhail Yasha Ramalho Gadelha - Integrante / Mauro Lopes de Freitas - Integrante / Hendrio Medeiros Marques - Integrante., Número de produções C, T & A: 3

• 2011 - 2012

  Interfaces Adaptativas em Software Imersivo para Crianças com Dificuldades Típicas aos Transtornos do Espectro Autista, Descrição: Trata-se de uma investigação em software imersivo de realidade virtual, desenvolver ambientes virtuais dentro dessas plataformas de acordo com as necessidades de crianças com transtornos do espectro autístico relacionadas à sua socialização e desenvolvimento cognitivo levantadas através de entrevistas com pais, fonoaudiólogos e psicólogos e realizar testes para aprimoramento contínuo das interfaces desenvolvidas. Para isso, serão efetuados testes em software configuráveis, utilizando computadores e tablets com manipulação direta e alto poder de processamento, visando as possibilidades de colaboração em tempo real entre crianças. , Situação: Concluído; Natureza: Pesquisa. , Alunos envolvidos: Graduação: (5) / Mestrado acadêmico: (2) . , Integrantes: Felipe Rodrigues Monteiro Sousa - Integrante / CASTRO, THAIS HELENA CHAVES DE - Coordenador., Número de produções C, T & A: 3

Projetos de desenvolvimento

• 2015 - Atual

  Programa de Formação Complementar CETELI - SAMSUNG de Tecnologias Móveis, Descrição: Financiado pela Samsung Eletrônica da Amazônia Ltda, este projeto tem como objetivo a formação de alunos de graduação e pós-graduação nas áreas de desenvolvimento e teste de dispositivos móveis. O programa é composto por um módulo de treinamento e um de desenvolvimento tecnológico. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (19) / Doutorado: (1) . , Integrantes: Felipe Rodrigues Monteiro Sousa - Integrante / CORDEIRO, LUCAS - Coordenador.

• 2015 - Atual

  Programa de Formação Complementar CETELI - SAMSUNG de Tecnologias Móveis, Descrição: Financiado pela Samsung Eletrônica da Amazônia Ltda., este projeto tem como objetivo a formação de alunos de graduação e pós-graduação nas áreas de desenvolvimento e teste de dispositivos móveis. O programa é composto por um módulo de treinamento e um de desenvolvimento tecnológico, onde os alunos se dividem em equipes para criação de um aplicativo móvel para a plataforma Android. , Situação: Em andamento; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (19) . , Integrantes: Felipe Rodrigues Monteiro Sousa - Integrante / Lucas Carvalho Cordeiro - Coordenador.

• 2015 - 2016

  Programa de Formação Complementar CETELI - SAMSUNG de Tecnologias Móveis, Descrição: Financiado pela Samsung Eletrônica da Amazônia Ltda., este projeto tem como objetivo a formação de alunos de graduação e pós-graduação nas áreas de desenvolvimento e teste de dispositivos móveis. O programa é composto por um módulo de treinamento e um de desenvolvimento tecnológico, onde os alunos se dividem em equipes para criação de um aplicativo móvel para a plataforma Android. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (19) . , Integrantes: Felipe Rodrigues Monteiro Sousa - Integrante / Lucas Carvalho Cordeiro - Coordenador.

• 2015 - 2016

  Programa de Formação Complementar CETELI - SAMSUNG de Tecnologias Móveis, Descrição: Financiado pela Samsung Eletrônica da Amazônia Ltda., este projeto tem como objetivo a formação de alunos de graduação e pós-graduação nas áreas de desenvolvimento e teste de dispositivos móveis. O programa é composto por um módulo de treinamento e um de desenvolvimento tecnológico, onde os alunos se dividem em equipes para criação de um aplicativo móvel para a plataforma Android. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (19) . , Integrantes: Felipe Rodrigues Monteiro Sousa - Integrante / Lucas Carvalho Cordeiro - Coordenador.

• 2015 - 2016

  Programa de Formação Complementar CETELI - SAMSUNG de Tecnologias Móveis, Descrição: Financiado pela Samsung Eletrônica da Amazônia Ltda., este projeto tem como objetivo a formação de alunos de graduação e pós-graduação nas áreas de desenvolvimento e teste de dispositivos móveis. O programa é composto por um módulo de treinamento e um de desenvolvimento tecnológico, onde os alunos se dividem em equipes para criação de um aplicativo móvel para a plataforma Android. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (19) . , Integrantes: Felipe Rodrigues Monteiro Sousa - Integrante / Lucas Carvalho Cordeiro - Coordenador.

• 2015 - 2016

  Programa de Formação Complementar CETELI - SAMSUNG de Tecnologias Móveis, Descrição: Financiado pela Samsung Eletrônica da Amazônia Ltda., este projeto tem como objetivo a formação de alunos de graduação e pós-graduação nas áreas de desenvolvimento e teste de dispositivos móveis. O programa é composto por um módulo de treinamento e um de desenvolvimento tecnológico, onde os alunos se dividem em equipes para criação de um aplicativo móvel para a plataforma Android. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (19) . , Integrantes: Felipe Rodrigues Monteiro Sousa - Integrante / Lucas Carvalho Cordeiro - Coordenador.

• 2015 - 2016

  Programa de Formação Complementar CETELI - SAMSUNG de Tecnologias Móveis, Descrição: Financiado pela Samsung Eletrônica da Amazônia Ltda., este projeto tem como objetivo a formação de alunos de graduação e pós-graduação nas áreas de desenvolvimento e teste de dispositivos móveis. O programa é composto por um módulo de treinamento e um de desenvolvimento tecnológico, onde os alunos se dividem em equipes para criação de um aplicativo móvel para a plataforma Android. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (19) . , Integrantes: Felipe Rodrigues Monteiro Sousa - Integrante / Lucas Carvalho Cordeiro - Coordenador.

• 2015 - 2016

  Programa de Formação Complementar CETELI - SAMSUNG de Tecnologias Móveis, Descrição: Financiado pela Samsung Eletrônica da Amazônia Ltda., este projeto tem como objetivo a formação de alunos de graduação e pós-graduação nas áreas de desenvolvimento e teste de dispositivos móveis. O programa é composto por um módulo de treinamento e um de desenvolvimento tecnológico, onde os alunos se dividem em equipes para criação de um aplicativo móvel para a plataforma Android. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (19) . , Integrantes: Felipe Rodrigues Monteiro Sousa - Integrante / Lucas Carvalho Cordeiro - Coordenador.

• 2017 - 2017

  Google Summer of Code 2017, Descrição: Checker Framework provides a collection of type systems to prevent bugs on Java programs at development time. Although a type system might be useful to prevent certain types of errors, it requires the effort to write all the types, which might be an annoying task for developers. In order to tackle such problem, developers might use a type inference tool to write the types for a program. Particularly, to determine what type should be written for a procedure?s formal parameter, a type inference tool must examine the type of the argument at every call to that procedure. Thus, the type inference process requires a whole-program analysis. In conclusion, the main goal of this project is to create a single type inference tool that will work for any type system available in Checker Framework (e.g., Nullness and Interning Checker).. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (1) . , Integrantes: Felipe Rodrigues Monteiro Sousa - Integrante / Michael Ernst - Coordenador.

• 2015 - 2016

  Programa de Formação Complementar CETELI - SAMSUNG de Tecnologias Móveis, Descrição: Financiado pela Samsung Eletrônica da Amazônia Ltda., este projeto tem como objetivo a formação de alunos de graduação e pós-graduação nas áreas de desenvolvimento e teste de dispositivos móveis. O programa é composto por um módulo de treinamento e um de desenvolvimento tecnológico, onde os alunos se dividem em equipes para criação de um aplicativo móvel para a plataforma Android. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (19) . , Integrantes: Felipe Rodrigues Monteiro Sousa - Integrante / Lucas Carvalho Cordeiro - Coordenador.

• 2017 - 2017

  Google Summer of Code 2017, Descrição: Checker Framework provides a collection of type systems to prevent bugs on Java programs at development time. Although a type system might be useful to prevent certain types of errors, it requires the effort to write all the types, which might be an annoying task for developers. In order to tackle such problem, developers might use a type inference tool to write the types for a program. Particularly, to determine what type should be written for a procedure?s formal parameter, a type inference tool must examine the type of the argument at every call to that procedure. Thus, the type inference process requires a whole-program analysis. In conclusion, the main goal of this project is to create a single type inference tool that will work for any type system available in Checker Framework (e.g., Nullness and Interning Checker).. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (1) . , Integrantes: Felipe Rodrigues Monteiro Sousa - Integrante / Michael Ernst - Coordenador.

• 2015 - 2016

  Programa de Formação Complementar CETELI - SAMSUNG de Tecnologias Móveis, Descrição: Financiado pela Samsung Eletrônica da Amazônia Ltda., este projeto tem como objetivo a formação de alunos de graduação e pós-graduação nas áreas de desenvolvimento e teste de dispositivos móveis. O programa é composto por um módulo de treinamento e um de desenvolvimento tecnológico, onde os alunos se dividem em equipes para criação de um aplicativo móvel para a plataforma Android. , Situação: Concluído; Natureza: Desenvolvimento. , Alunos envolvidos: Graduação: (19) . , Integrantes: Felipe Rodrigues Monteiro Sousa - Integrante / Lucas Carvalho Cordeiro - Coordenador.

Prêmios