Mikhail Yasha Ramalho Gadelha

Bolsista de Doutorado no Exterior do CNPq

  • Endereço para acessar este CV: http://lattes.cnpq.br/5172660162494409
  • Última atualização do currículo em 07/11/2017


Possui graduação em Engenharia de Telecomunicações pela Fundação Centro de Análise Pesquisa e Inovação Tecnológica (Fucapi, 2010) e graduação em Engenharia da Computação pela Universidade Federal do Amazonas (UFAM, 2010), participante de um programa de graduação sanduíche da Universidade do Porto na Universidade de Tecnologia e Economia de Budapeste (2009), mestrado em Engenharia Elétrica na área de concentração em Engenharia da Computação pela Universidade Federal do Amazonas (UFAM, 2013). Atualmente é Engenheiro da Computação e professor assistente na Fundação Centro de Análise Pesquisa e Inovação Tecnológica (Fucapi). Tem experiência nas áreas de Verificação Formal Automatizada, Bounded (and Unbounded) Model Checking, Sistemas Embarcados, TV Digital, Linux e Desenvolvimento de Software em C e C++ para baixo e alto nível. Possui 9 publicações revisadas, incluindo 2 publicação em revista e 7 em conferências/workshops. Possui colaboração em projetos de pesquisa com as universidades de Southampton (Reino Unido) e Stellenbosch (África do Sul). Atuou também em projetos de desenvolvimento de software relacionados à Aplicações Mobile no Instituto Nokia de Desenvolvimento e Set-top Box, sistemas embarcados e industriais na Fucapi. Atualmente é aluno de doutorado na Universidade de Southampton. Bolsista CNPQ. (Texto informado pelo autor)


Identificação


Nome
Mikhail Yasha Ramalho Gadelha
Nome em citações bibliográficas
GADELHA, M. Y. R.;Mikhail Yasha Gadelha;GADELHA, MIKHAIL Y. R.

Endereço


Endereço Profissional
Universidade Federal do Amazonas.
Avenida Rodrigo Otávio
Japiim
69077000 - Manaus, AM - Brasil
Telefone: (92) 33054691


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


2015
Doutorado em andamento em PhD in Computer Science.
University of Southampton, SOUTHAMPTON, Inglaterra.
Orientador: Denis Nicole.
Bolsista do(a): Conselho Nacional de Desenvolvimento Científico e Tecnológico, CNPq, Brasil.
2012 - 2013
Mestrado em Engenharia Elétrica.
Universidade Federal do Amazonas, UFAM, Brasil.
Título: Verificação Baseada em Indução Matemática para Programas C++,Ano de Obtenção: 2013.
Orientador: Lucas Carvalho Cordeiro.
Bolsista do(a): Fundação de Amparo a Pesquisa do Estado do Amazonas, FAPEAM, Brasil.
2006 - 2010
Graduação em Engenharia de Telecomunicações.
Fundação Centro de Análise Pesquisa e Inovação Tecnológica, FUCAPI, Brasil.
Título: Otimização no Algoritmo de Criptografia de Dados utilizando Imagens.
Orientador: Alexandre Duarte da Silva.
2006 - 2010
Graduação em Engenharia da Computação.
Universidade Federal do Amazonas, UFAM, Brasil.
Título: Estudo de Métodos de Criptografia de Dados utilizando Imagens.
Orientador: Marly Guimarães Fernandes Costa.




Atuação Profissional



Universidade Federal do Amazonas, UFAM, Brasil.
Vínculo institucional

2012 - 2013
Vínculo: Prestador de Serviços, Enquadramento Funcional: Desenvolvedor, Carga horária: 25

Vínculo institucional

2008 - 2008
Vínculo: Bolsista, Enquadramento Funcional: Desenvolvedor, Carga horária: 20
Outras informações
Desenvolvedor de aplicativos para dispositivos móveis (Maemo).


Fundação Centro de Análise Pesquisa e Inovação Tecnológica, FUCAPI, Brasil.
Vínculo institucional

2013 - Atual
Vínculo: Colaborador, Enquadramento Funcional: Professor Assistente, Carga horária: 12

Vínculo institucional

2013 - Atual
Vínculo: Colaborador, Enquadramento Funcional: Engenheiro da Computação, Carga horária: 32

Vínculo institucional

2010 - 2011
Vínculo: Colaborador, Enquadramento Funcional: Engenheiro da Computação, Carga horária: 40
Outras informações
Trabalhei TV Digital, desenvolvendo o middleware Ginga para televisões em circulação no mercado atualmente.

Vínculo institucional

2009 - 2010
Vínculo: Bolsista, Enquadramento Funcional: Desenvolvedor, Carga horária: 20
Outras informações
Desenvolvedor de aplicativos para dispositivos móveis (Maemo e MeeGo).


Budapest University of Technology and Economics, BUTE, Hungria.
Vínculo institucional

2009 - 2009
Vínculo: Bolsista, Enquadramento Funcional: Bolsista, Carga horária: 24
Outras informações
Participação no projeto Erasmus Mundus (Universidades Brasil e Europa) sendo bolsista da Universidade do Porto no período de 02/2009 a 06/2009 na Universität Stuttgart, onde realizou graduação Sandwich em Engenharia Elétrica. Durante esse período foi trancada a matrícula nas disciplinas do curso de Engenharia Elétrica da Universidade Federal do Amazonas. Os aprendizados técnico e cultural foram de extrema importância neste projeto, tendo em vista que a Hungria apresenta um alto nível de desenvolvimento tecnológico e cultural.



Projetos de pesquisa


2013 - Atual
Verificação de Propriedades Temporais em Software Embarcado usando as Teorias do Módulo da Satisfatibilidade

Projeto certificado pelo(a) coordenador(a) Lucas Carvalho Cordeiro em 03/01/2014.
Descrição: Nossa dependência no funcionamento correto de sistemas embarcados está aumentando cada vez mais. Tais sistemas são usados em um amplo espectro de aplicações tais como sistemas de controle de airbag, telefones celulares e set-top boxes. Estes sistemas estão se tornando cada vez mais complexos e solicitam processadores de vários núcleos com memória compartilhada escalável para atender a crescente demanda do poder computacional. Desta maneira, a confiabilidade dos sistemas (distribuídos) embarcados é um assunto chave no desenvolvimento de sistemas. O objetivo principal deste projeto de pesquisa é desenvolver métodos para verificação de modelos de software embarcado contra propriedades de vivacidade especificadas como fórmulas em lógica temporal de tempo linear (Linear-time Temporal Logic, LTL), a qual estende a lógica proposicional incluindo operadores temporais. Em especial, será utilizada a técnica de verificação de modelos limitada (Bounded Model Checking, BMC) baseada nas teorias do módulo da satisfatibilidade (satisfiability modulo theories, SMT). A ideia desta técnica é checar a negação de uma dada propriedade a uma dada profundidade. A profundidade é definida atribuindo um limite no número de chaveamento de contextos, número de iterações dos laços e profundidades das funções recursivas. Para alcançar os objetivos deste projeto de pesquisa, será investigado em que extensão as noções estabelecidas dos algoritmos para verificação de modelo de LTL podem ser aplicadas ao contexto da verificação de modelo limitada. As fórmulas LTL serão então convertidas em condições de segurança que sejam equivalentes para execução de programas limitados através da tradução de operadores de tempo futuro em código que registre a história do evento. Como primeiro passo para tratar LTL temporizado, as anotações do tempo de execução do pior caso (WCET) serão compiladas para variáveis temporizadas, que podem ser usadas como propriedades de segurança, e serão então estendidas para tratar a LTL não temporizada. Os algoritmos desenvolvidos neste projeto de pesquisa, serão integrados no nosso verificador de código ESBMC (Efficient SMT-based Context-Bounded Model Checker), e será então investigado sua extensão para sistemas embarcados escritos em ANSI-C (linguagem comumente usada em software embarcado) e SystemC (que é uma linguagem de descrição de hardware baseada em C++ amplamente usada na indústria). O resultado final desta pesquisa é então assegurar a corretude lógica e temporal do software embarcado em televisores, set-top boxes e aparelhos celulares, que são sistemas comumente produzidos no pólo industrial de Manaus.
Situação: Em andamento; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (0) / Especialização: (0) / Mestrado acadêmico: (1) / Mestrado profissional: (0) / Doutorado: (6) .
Integrantes: Mikhail Yasha Ramalho Gadelha - Integrante / Waldir Sabino - Integrante / Vicente Lucena - Integrante / Lucas Carvalho Cordeiro - Coordenador / Bernd Fischer - Integrante / Jeremy Morse - Integrante / Denis Nicole - Integrante.Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
2011 - 2013
Continuous Verification of C++ Programs Using SMT-based Bounded Model Checking

Projeto certificado pela empresa INSTITUTO NOKIA DE TECNOLOGIA em 18/09/2013.
Descrição: The main objective of this project is first to extend the ESBMC model checker to support the verification of C++ programs and then integrate it into the software engineering process of INdT by exploiting practices such as incremental development and regression tests. In particular, we aim to define an object model to capture the semantics of the C++ programs and then integrate it into the ESBMC model checker. After that, we aim to apply the continuous verification concept together with ESBMC to verify realistic C++ applications. The continuous verification approach combines existing ideas of software engineering, (e.g., continuous integration) and formal verification (e.g., equivalence checking) communities and it aims to automatically detect design errors and integration problems as quickly as possible by exploiting information from the software configuration management (SCM) system, systematically focusing the verification effort on new or modified functions. We aim to use equivalence checking to determine whether modified functions need to be re-verified formally and use existing test cases to reduce the search space for the model checker, thus combining dynamic and static verification (we use the term dynamic to denote that the program is executed and its actual and expected outputs observed and static to denote that a mathematical model of the program is analyzed).
Situação: Concluído; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (2) .
Integrantes: Mikhail Yasha Ramalho Gadelha - Integrante / Lucas Carvalho Cordeiro - Coordenador / Felipe Sousa - Integrante / Hendrio Marques - Integrante / Bruno Savino - Integrante.
Número de produções C, T & A: 1
2011 - Atual
SMT-Based Bounded Model Checking Timed LTL Properties for Embedded Software

Projeto certificado pelo(a) coordenador(a) Lucas Carvalho Cordeiro em 18/09/2013.
Descrição: Our overall research aim is to develop methods for SMT-based bounded model checking embedded software against liveness properties specified as timed LTL formulas. We will first investigate to which extent the established notions of and algorithms for LTL model checking transfer to a bounded model checking context. We will then convert LTL formulas into safety conditions that are equivalent for bounded program executions, by translating future-time operators into code that records the event history. As first step to handling timed LTL, we will compile WCET annotations to timer variables that can be used in safety properties, and then extend this to the untimed LTL handling. We will integrate the developed algorithms into our ESBMC model checker, and investigate its extension to SystemC.
Situação: Em andamento; Natureza: Pesquisa.
Alunos envolvidos: Mestrado acadêmico: (1) Doutorado: (2) .
Integrantes: Mikhail Yasha Ramalho Gadelha - Integrante / Lucas Carvalho Cordeiro - Coordenador / Bernd Fischer - Integrante / Jeremy Morse - Integrante / Raimundo da Silva Barreto - Integrante / Denis Nicole - Integrante.


Áreas de atuação


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


Idiomas


Português
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.
Inglês
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.


Prêmios e títulos


2010
Qt Ambassador, Nokia.


Produções



Produção bibliográfica
Artigos completos publicados em periódicos

1.
GADELHA, MIKHAIL Y. R.2017 GADELHA, MIKHAIL Y. R.; ISMAIL, HUSSAMA I. ; CORDEIRO, LUCAS C. . Handling loops in bounded model checking of C programs via k-induction. International Journal on Software Tools for Technology Transfer, v. 19, p. 97-114, 2017.

2.
ABREU, RENATO B.2016ABREU, RENATO B. ; GADELHA, MIKHAIL Y. R. ; CORDEIRO, LUCAS C. ; DE LIMA FILHO, EDDIE B. ; DA SILVA, WALDIR S. . Bounded model checking for fixed-point digital filters. JOURNAL OF THE BRAZILIAN COMPUTER SOCIETY (ONLINE), v. 22, p. 1-20, 2016.

3.
GADELHA, M. Y. R.2013GADELHA, M. Y. R.; COSTA FILHO, C. F. F. ; COSTA, M. G. F. . Optimizations of a Cryptographic Method Using Gray Scale Digital Images. Journal of Internet Technology and Secured Transactions, v. 2, p. 141-146, 2013.

4.
FREITAS, M.2012FREITAS, M. ; VALENZUELA, V. ; GADELHA, M. Y. R. ; CORDEIRO, L. C. ; SABINO, W. ; LUCENA, V. . Distributed Extension of the Hybrid PRS System using Video Processing to Command a Robot via Bluetooth. International Journal of Computer Science and Network Security, v. 12, p. 29-35, 2012.

Trabalhos completos publicados em anais de congressos
1.
GADELHA, M. Y. R.; CORDEIRO, L. C. ; NICOLE, D. . Encoding floating-points using the SMT theory in ESBMC: An empirical evaluation over the SV-COMP benchmarks. In: XX Brazilian Symposium on Formal Methods, 2017, Recife. SBMF'17, 2017.

2.
MORSE, J. ; GADELHA, M. Y. R. ; CORDEIRO, L. C. ; NICOLE, D. ; FISCHER, B. . ESBMC v1.22 (Competition Contribution). In: 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2014, Grenoble. Proceedings of 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2014.

3.
GADELHA, M. Y. R.; FREITAS, M. ; SOUSA, F. ; MARQUES, H. ; CORDEIRO, L. C. ; FISCHER, B. . SMT-Based Bounded Model Checking of C++ Programs. In: ECBS'13, 2013, Phoenix. IEEE International Conference and Workshops on the Engineering of Computer Based Systems, 2013. p. 147-156.

4.
FREITAS, M. ; Mikhail Yasha Gadelha ; CORDEIRO, L. C. ; SABINO, W. ; Eddie B. L. Filho . Verificação De Propriedades De Filtros Digitais Implementados Com Aritmética De Ponto Fixo. In: XXXI Simpósio Brasileiro de Telecomunicações, 2013, Fortaleza. SBrT'13, 2013.

5.
GADELHA, M. Y. R.; CORDEIRO, L. C. ; Cavalcante, A. L. D. ; LUCENA, V. . Verificação Baseada em Indução Matemática para Programas C/C++. In: III Simpósio Brasileiro de Engenharia de Sistemas Computacionais, 2013, Niterói/RJ. SBESC'13, 2013.

6.
GADELHA, M. Y. R.; COSTA FILHO, C. F. F. ; COSTA, M. G. F. . Proposal of a Cryptography Method Using Gray Scale Digital Images. In: International Conference for Internet Technology and Secured Transactions, 2012, Inglaterra. International Conference for Internet Technology and Secured Transactions Proceedings, 2012. v. 1. p. 331-335.

7.
SILVA, J. B. ; GADELHA, M. Y. R. ; CORDEIRO, L. C. ; SABINO, W. . Sistema de Medição de Temperatura Integrado a TV Digital. In: 12o. Congresso Nacional de Iniciação Científica (Conic-Semesp), 2012, São Paulo. 12o. Congresso Nacional de Iniciação Científica (Conic-Semesp), 2012.

8.
GADELHA, M. Y. R.; REPOLHO, H. C. R. ; ALMEIDA, N. R. ; PICANCO JUNIOR, E. T. . Modelagem de um Sistema de Tráfego. In: I Escola Regional de Informática ? ERIN 2009, 2009, Manaus. Escola Regional de Informática, 2009. v. 1. p. 1-9.

Apresentações de Trabalho
1.
GADELHA, M. Y. R.. Ubuntu. 2010. (Apresentação de Trabalho/Conferência ou palestra).


Produção técnica
Programas de computador sem registro
1.
GADELHA, M. Y. R.. TweeGo. 2010.



Bancas



Participação em bancas de trabalhos de conclusão
Trabalhos de conclusão de curso de graduação
1.
JUNIOR, A.; GADELHA, M. Y. R.; GADELHA, I.. Participação em banca de SABRINA OURO PAPES NUNES.ANÁLISE DO DESEMPENHO DE REDE DE SENSORES SEM FIO APLICADA AO MONITORAMENTO ANIMAL. 2013. Trabalho de Conclusão de Curso (Graduação em Engenharia de Computação) - Fundação Centro de Análise Pesquisa e Inovação Tecnológica.

2.
GADELHA, M. Y. R.; JUNIOR, A.; LUCAS, W.. Participação em banca de HUSSAMA IBRAHIM ISMAIL.SIMULADOR DE TÉCNICAS DE ESCALONAMENTO de SISTEMAS de TEMPO REAL. 2013. Trabalho de Conclusão de Curso (Graduação em Engenharia de Computação) - Fundação Centro de Análise Pesquisa e Inovação Tecnológica.





Página gerada pelo Sistema Currículo Lattes em 19/12/2018 às 7:29:52