Juliano Manabu Iyoda

Possui graduação e mestrado em Ciência da Computação pela Universidade Federal de Pernambuco (1997,2000) e doutorado em Ciência da Computação pela Universidade de Cambridge (2007). Tem experiência na área de Engenharia de Software com ênfase em Metodos Formais e Testes.
(Texto informado pelo autor)

Última atualização do currículo em 28/11/2011
Endereço para acessar este CV:
http://lattes.cnpq.br/0005349558315095

Dados pessoais
NomeJuliano Manabu Iyoda
Nome em citações bibliográficasIYODA, J. M.;IYODA, J;Iyoda, Juliano
SexoMasculino
Endereço profissionalUniversidade Federal de Pernambuco, Centro de Informática.
Centro de Informática, UFPE
Cidade Universitária
50732-970 - Recife, PE - Brasil

Formação acadêmica/Titulação
2002 - 2006Doutorado em Ciência da Computação .
University of Cambridge, CAM, Inglaterra.
Título: Translating HOL Functions to Hardware, Ano de Obtenção: 2007.
Orientador: Michael John Caldwell Gordon.
Bolsista do(a): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior .
Palavras-chave: Provador de Teorema; Sintese de hardware; HOL; Verificacao Formal.
1998 - 2000Mestrado em Ciência da Computação .
Universidade Federal de Pernambuco, UFPE, Brasil.
Título: ParTS: uma Ferramenta de Suporte ao Particionamento Hardware/Software, Ano de Obtenção: 2000.
Orientador: Augusto Cézar Alves Sampaio.
Bolsista do(a): Conselho Nacional de Desenvolvimento Científico e Tecnológico ,CNPq ,Brasil .
Palavras-chave: Transformacoes algebricas; Hardware-Software co-design; Particionamento hardware-software.
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodos Formais / Especialidade: Metodos Formais Aplicado à Hardware Software Co Design.
Setores de atividade: Industria Eletro-Eletrônica.
1993 - 1997Graduação em Ciência da Computação .
Universidade Federal de Pernambuco, UFPE, Brasil.

Formação complementar
2000 - 2001 Extensão universitária em Ciencia da Computacao.
United Nations University International Institute For Software Technology.

Atuação profissional
Qualiti Assessoria e Consultoria S/A, QUALITI, Brasil.
Vínculo institucional
2007 - 2007 Vínculo: Colaborador, Enquadramento Funcional: Consultor em Engenharia de Processos, Regime: Dedicação exclusiva.
Vínculo institucional
2001 - 2002 Vínculo: Colaborador, Enquadramento Funcional: Engenheiro de Processos, Regime: Dedicação exclusiva.
Atividades
08/2001 - 08/2002Conselhos, Comissões e Consultoria, .
Cargo ou função
Engenheiro de Processos.
United Nations University International Institute For Software Technology, UNU/IIST, Macau.
Vínculo institucional
2000 - 2001 Vínculo: Outro, Enquadramento Funcional: Outro (Fellow), Carga horária: 35, Regime: Dedicação exclusiva.
Outras informações Como fellow, desenvolvi um trabalho de pesquisa utilizando métodos formais aplicado ao processo de síntese de hardware sob orientação do Prof. He Jifeng (pesquisador senior).
Atividades
5/2000 - 7/2001Pesquisa e desenvolvimento .
Linhas de pesquisa
Métodos formais aplicado ao projeto de hardware
Universidade Federal de Pernambuco, UFPE, Brasil.
Vínculo institucional
2009 - Atual Vínculo: Servidor Público, Enquadramento Funcional: Professor Adjunto, Regime: Dedicação exclusiva.
Vínculo institucional
2007 - 2008 Vínculo: Bolsista recém-doutor, Enquadramento Funcional: Professor Visitante, Regime: Dedicação exclusiva.
Vínculo institucional
1996 - 1997 Vínculo: Outro, Enquadramento Funcional: Outro (aluno de iniciação científica), Carga horária: 20, Regime: Dedicação exclusiva.
Atividades
2011 - 2013Atividades de Participação em Projeto, Centro de Informática, .
Projetos de pesquisa
Verificação de Modelos Voltados para Requisitos de Sistemas Aviônicos
3/1996 - 11/1997Treinamentos ministrados , Centro de Ciências Exatas e da Natureza, Departamento de Informática.
Treinamentos ministrados
Iniciação científica
Net Informática Ltda, NETINFORMATICA, Brasil.
Vínculo institucional
1994 - 1995 Vínculo: Outro, Enquadramento Funcional: Outro (estagiário), Carga horária: 12
Atividades
3/1994 - 10/1995Estágios .
Estágio realizado
Programação em Clipper e SQL.

Linhas de Pesquisa
1. Métodos formais aplicado ao projeto de hardware
Objetivos: Aplicar técnicas formais de desenvolvimento para obter produtos corretos e confiáveis..
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodos Formais / Especialidade: Metodos Formais Aplicado Ao Projeto de Hardware.
Setores de atividade: Industria Eletro-Eletrônica.
Palavras-chave: Projeto de hardware.

Projetos de Pesquisa
2010 - 2012Verificação de Modelos Voltados para Requisitos de Sistemas Aviônicos
Descrição: Requisitos para sistemas aviônicos são descritos usualmente por dois artefatos: um documento de requisitos em linguagem natural e um modelo formal (tipicamente, um diagrama Simulink). Neste projeto, propomos dois objetivos complementares: a tradução de requisitos escritos em linguagem natural controlada (um subconjunto não-ambíguo de linguagem natural) para propriedades em lógica temporal; e a geração de propriedades em lógica temporal a partir de um diagrama Simulink. O primeiro objetivo permite verificarmos de forma 100% automática se um modelo (traduzido de Simulink) satisfaz uma propriedade (traduzida de linguagem natural controlada). O segundo objetivo oferece ao engenheiro projetista uma lista de propriedades que o diagrama Simulink por ele proposto satisfaz. Este feedback pode revelar falhas de projeto ainda na fase de requisitos. Este projeto conta com o apoio da Embraer Empresa Brasileira de Aeronáutica S.A..
Situação: Em andamento; Natureza: Pesquisa.
Alunos envolvidos: Mestrado acadêmico ( 2) .
Integrantes: Augusto César Alves Sampaio - Integrante / Alexandre Cabral Mota - Integrante / Márcio Lopes Cornélio - Integrante / Flávia de Almeida Barros - Integrante / André Luís Ribeiro Didier - Integrante / Diego Machado Dias - Integrante / Juliano Manabu Iyoda - Coordenador.
Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro..

Áreas de atuação
1. Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodos Formais / Especialidade: Metodos Formais Aplicado Ao Projeto de Hardware.
2. Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodos Formais / Especialidade: Metodos Formais Aplicado à Hardware Software Co Design.

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


Produção em C,T & A
Produção bibliográfica
Artigos completos publicados em periódicos
1. Perna, Juan ; Woodcock, Jim ; Sampaio, Augusto ; Iyoda, Juliano . Correct hardware synthesis. Acta Informatica, v. 48, p. 363-396, 2011.
2.   Takaki, Mitsuo ; Cavalcanti, Diego ; Gheyi, Rohit ; Iyoda, Juliano ; d Amorim, Marcelo ; Prudêncio, Ricardo B. C. . Randomized constraint solvers: a comparative study. Innovations in Systems and Software Engineering (Print), v. --, p. -----, 2010.
3.   Konrad Slind ; Scott Owens ; IYODA, J. M. ; Mike Gordon . Proof producing synthesis of arithmetic and cryptographic hardware. Formal Aspects of Computing, v. 19, p. 343-362, 2007.
Trabalhos completos publicados em anais de congressos
1.   DIAS, D. M. ; Iyoda, Juliano . Behavioural Preservation in Fault Tolerant Patterns. In: Simpósio Brasileiro de Métodos Formais (SBMF), 2011, São Paulo. Anais do Simpósio Brasileiro de Métodos Formais (Lecture Notes in Computer Science), 2011. v. 7021. p. 156-171.
2. Breno Miranda ; Iyoda, Juliano ; MEIRA, S. R. L. . Test Case Recommender: um sistema de recomendação para alocação automática de testes baseada no perfil do testador. In: IV Brazilian Workshop on Systematic and Automated Software Testing (SAST), 2010, Natal-RN. Anais do IV Brazilian Workshop on Systematic and Automated Software Testing (SAST), 2010.
3.   Mitsuo Takaki ; Diego Cavalcanti ; Rohit Gheyi ; IYODA, J. M. ; Marcelo d'Amorim ; Ricardo Prudêncio . Comparative Study of Randomized Constraint Solvers for Random-Symbolic Testing. In: First NASA Formal Methods Symposium (NFM), 2009, Moffet Field, CA, USA. Proceedings of the First NASA Formal Methods Symposium (NFM), 2009.
4. Juliana Mafra ; Breno Miranda ; IYODA, J ; Augusto Sampaio . Test Case Selector: Uma Ferramenta para Seleção de Testes. In: Brazilian Workshop on Systematic and Automated Software Testing, 2009, Gramado-RS. Anais do Brazilian Workshop on Systematic and Automated Software Testing, 2009.
5.   Lucas Lima ; Eduardo Aranha ; IYODA, J ; Augusto Sampaio . Test Case Prioritization Based on Data Reuse: An Experimental Study. In: Empirical Software Engineering and Measurement (ESEM), 2009, Lake Buena Vista-FL. Proceedings of the 3rd Empirical Software Engineering and Measurement (ESEM), 2009.
6. Falcà o, Flà via ; Iyoda, Juliano ; Sampaio, Augusto . Multiple Synchrony in MSC. In: Simpósio Brasileiro de Métodos Formais (SBMF), 2009, Salvador - BA. Anais do Simpósio Brasileiro de Métodos Formais (Electronic Notes in Theoretical Computer Science). v. 240. p. 149-166.
7. Lucas Lima ; IYODA, J. M. ; Augusto Sampaio . A Permutation Technique for Test Case Prioritization in a Black-box Environment. In: Brazilian Workshop on Systematic and Automated Software Testing, 2008, Campinas - SP. Brazilian Workshop on Systematic and Automated Software Testing, 2008.
8. GORDON, M ; IYODA, J ; OWENS, S ; SLIND, K . Automatic Formal Synthesis of Hardware from Higher Order Logic. In: Fifth International Workshop on Automated Verification of Critical Systems, 2006, Coventry - Inglaterra. Proceedings of AVoCS 2005 (Electronic Notes in Theoretical Computer Science). Amsterdam : Elsevier Science Publishers B. V., 2005. v. 145. p. 27-43.
9. IYODA, J. M. ; He Jifeng . Towards an Algebraic Synthesis of Verilog. In: First International Conference on Engineering of Reconfigurable Systems and Algorithms, 2001, Las Vegas. Engineering of Reconfigurable Systems and Algorithms (ERSA'01), 2001.
10. IYODA, J. M. ; Augusto Sampaio ; Leila Silva . ParTS: A Partitioning Transformation System. In: World Congress on Formal Methods (FM'99), 1999, Toulouse. FM'99 Formal Methods, 1999. v. 1709. p. 1400-1419.
11. Leila Silva ; Augusto Sampaio ; Edna Barros ; IYODA, J. M. . An Algebraic Approach to Combining Processes in a Hardware/Software Partitioning Environment. In: Algebraic Methodology and Software Technology, 1999, Manaus-AM, Brazil. 7th Algebraic Methodology and Software Technology. Berlin : Springer Verlag, 1998. v. 1548. p. 308-324.
12. IYODA, J. M. ; Augusto Sampaio ; Leila Silva . ParTS: Partitioning Transformation System. In: Simpósio Brasileiro de Engenharia de Software (SBES), 1998, Maringá - PR. 12o Simpósio Brasileiro de Engenharia de Software - Caderno de Ferramentas, 1998. p. 67-73.
Resumos expandidos publicados em anais de congressos
1. Mike Gordon ; IYODA, J. M. ; Scott Owens ; Konrad Slind . A Proof-Producing Hardware Compiler for a Subset of Higher Order Logic. In: 18th International Conference on Theorem Proving in Higher Order Logics, TPHOLs2005, 2005, Oxford. Emerging Trends - Proceedings of th 18th International Conference on Theorem Proving in Higher Order Logics: TPHOLs 2005, 2005. p. 59-75.
Resumos publicados em anais de congressos
1. Konrad Slind ; Scott Owens ; Mike Gordon ; IYODA, J. M. . Proof Producing Synthesis of Arithmetic and Cryptographic Hardware. In: Designing Correct Circuits 2006, 2006, Vienna. Design Correct Circuits 2006, 2006.
Demais tipos de produção bibliográfica
1. IYODA, J. M. . Translating HOL Functions to Hardware 2006 (Tese de Doutorado).
2. IYODA, J. M. ; He Jifeng . Towards an Algebraic Synthesis of Verilog. Macau 2001 (Relatório Técnico).
3. IYODA, J. M. ; He Jifeng . A Prolog Prototype for the Synthesis of Verilog. Macau 2001 (Relatório Técnico).
4. IYODA, J. M. . ParTS: Uma Ferramenta de Suporte ao Particionamento Hardware/Software. Recife 2000 (Tese de Mestrado).
Produção técnica
Softwares sem registro de patente
1. IYODA, J. M. . ParTS: A Partitioning Transformation System. 2000.
Trabalhos técnicos
1. Iyoda, Juliano . Coordenador do Convênio de Cooperação com a Morpho E-Docs. 2011.

Bancas
Participação em bancas examinadoras
Dissertações
1. Alexandre Mota; Cristiano Ferraz; Iyoda, Juliano. Participação em banca de Thiers Garretti Ramos Sousa. Verificando a corretude de geradores automáticos de código. 2010. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal de Pernambuco.
2. Cristine Gusmão; Sérgio Soares; Iyoda, Juliano. Participação em banca de Juliana de Albuquerque Gonçalves Saraiva. Avaliação de Impacto de Programação Orientada a Aspectos sob Arquiteturas de Software em Camadas. 2010. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal de Pernambuco.
3. Gheyi, Rohit; VASCONCELOS, A. M. L.; Iyoda, Juliano. Participação em banca de Juliana Nereida Dantas Mafra. Test Case Selector: Uma Ferramenta para Seleção de Testes. 2010. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal de Pernambuco.
4. Iyoda, Juliano; VASCONCELOS, A. M. L.; Cristine Gusmão. Participação em banca de Diana Rúbia Rodrigues Ricardo. Proposta de Processo para Testes Exploratórios Aderente ao TMMI Nível 2. 2010. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal de Pernambuco.
5. Iyoda, Juliano; MACHADO, P. D. L.; FIGUEIREDO, J. C. A.. Participação em banca de Francisco Gomes de Oliveira Neto. Uma Avaliação e Investigação Experimental de Técnicas de Re-Teste Seletivo para Teste de Regressão Baseado em Especificação. 2010. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal de Campina Grande.
6. Alexandre Mota; Iyoda, Juliano; DROGUETT, E. A. L.. Participação em banca de Adriano José Oliveira Gomes. Systematic Model-Based Safety Assessment via Probabilistic Model Checking. 2010. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.
7. IYODA, J. M.; Alexandre Mota; Márcio Cornélio. Participação em banca de Gláucia Peres. A Black-box Testing Technique for the Detection of Crashes Based on Automated Test Scenarios. 2009. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal de Pernambuco.
8. Renato Corrêa; Flávia Barros; Iyoda, Juliano. Participação em banca de Leonardo de Souza Lima. Class-Test: Classificação Automática de Testes para Auxílio à Criação de Suítes de Teste. 2009. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal de Pernambuco.
9. Iyoda, Juliano; Renato Corrêa; Adriano Lorena. Participação em banca de Mitsuo Takaki. Busca meta-Heurística para Resolução de CSP em Teste de Software. 2009. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal de Pernambuco.
Teses de doutorado
1. Augusto Sampaio; Paulo Borba; Cristiano Ferraz; Álvaro Moreira; Iyoda, Juliano. Participação em banca de Cristiano Bertolini. Evaluation of GUI Testing Techniques for System Crashing: From Real to Model-Based Controlled Experiments. 2010. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.
2. Marcelo d'Amorim; Marco Túlio Valente; Sérgio Soares; Uirá Kulesza; Iyoda, Juliano. Participação em banca de Alberto Costa Neto. Specifying Design Rules in Aspect-Oreinted Systems. 2009. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.
3. Ricardo Massa; Márcio Cornélio; Jones Albuquerque; Roberto Barros; Iyoda, Juliano. Participação em banca de Adalberto Cajueiro de Farias. Abstraction of Infinite and Communicating CSPZ Processes. 2009. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco.
4. Augusto Sampaio; Alexandre Mota; Marcel Oliveira; Ana Cristina Melo; IYODA, J. 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. Iyoda, Juliano; JERON, T.; SIMAO, A. S.. Participação em banca de Sidney de Carvalho Nogueira. Test Generation and Compositional Conformance Verification with Input-Outpout CSP Models. 2010. Exame de qualificação (Doutorando em Ciências da Computação) - Universidade Federal de Pernambuco.
2. Marcelo d'Amorim; Marco Túlio Valente; Iyoda, Juliano. Participação em banca de Alberto Costa Neto. Specifying Design Rules in Aspect-Oriented Systems. 2009. Exame de qualificação (Doutorando em Ciências da Computação) - Universidade Federal de Pernambuco.
3. Paulo Borba; Cristiano Ferraz; Iyoda, Juliano. Participação em banca de Cristiano Bertolini. A Formal Framework of GUI Exploration for Effective System Crashing. 2009. Exame de qualificação (Doutorando em Ciências da Computação) - Universidade Federal de Pernambuco.
4. Ana Cristiana Melo; Paulo Borba; Iyoda, Juliano. Participação em banca de Rodrigo Teixeira Ramos. Systematic Development of Trustworthy Component-Based Systems. 2009. Exame de qualificação (Doutorando em Ciências da Computação) - Universidade Federal de Pernambuco.
Trabalhos de Conclusão de Curso de graduação
1. Marcelo d'Amorim; Iyoda, Juliano. Participação em banca de Sérgio Barza. Desenho e implementação de um dynamic forward slicer utilizando BCEL. 2011. Trabalho de Conclusão de Curso (Graduação em Ciência da Computação) - Universidade Federal de Pernambuco.
Participação em bancas de comissões julgadoras
Concurso público
1. Eduardo Tavares; Everson Feitosa; Iyoda, Juliano. Membro da Banca Examinadora do Concurso para Professor Assistente para Unidade Acadêmica de Garanhuns / UFRPE. 2010. Universidade Federal Rural de Pernambuco.

Eventos
Participação em eventos
1. Brasilian Symposium on Formal Methods (SBMF).Multi-Synchrony in MSC. 2008. (Simpósio).

Orientações
Orientações em andamento
Dissertação de mestrado
1. Breno Alexandro Ferreira de Miranda. Recommender Systems for Manual Testing. Início: 2011. Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco. (Orientador).
2. Webster Silva Campêlo Junior. Mineração de Dados de Testes. Início: 2010. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal de Pernambuco. (Orientador).
3. Diego Machado Dias. Métodos Formais em Sistemas Aviônicos. Início: 2010. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal de Pernambuco, Fundação de Amparo à Ciência e Tecnologia do Estado de Pernambuco. (Orientador).
Tese de doutorado
1. Lucas Albertins de Lima. Uma Estratégia para Verificação e Teste de Aplicações IMA. Início: 2011. Tese (Doutorado em Ciências da Computação) - Universidade Federal de Pernambuco. (Orientador).
Supervisões e orientações concluídas
Dissertação de mestrado
1. Renata Bezerra e Silva de Araújo. Extração Automática de Modelo CSP a Partir de Casos de Uso. 2011. Dissertação (Mestrado em Pós-Graduação em Ciência da Computação) - Universidade Federal de Pernambuco, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: Juliano Manabu Iyoda.
2. Lucas Albertins de Lima. Test Case Prioritization for Black-Box Environments. 2009. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal de Pernambuco, . Co-Orientador: Juliano Manabu Iyoda.
3. Juliana Nereida Dantas Mafra. Test Case Selection for a Black-box environment. 2009. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal de Pernambuco, . Orientador: Juliano Manabu Iyoda.
4. Flávia Mérylyn Carneiro Falcão. Multi-Sincronização em Message Sequence Charts. 2008. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco, . Co-Orientador: Juliano Manabu Iyoda.
Página gerada pelo Sistema Currículo Lattes em 09/02/2012 às 17:51:00