Lucas Carvalho Cordeiro

Bolsista de Produtividade em Pesquisa do CNPq - Nível 2 (***)

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


Possui graduação em Engenharia Elétrica pela Universidade Federal do Amazonas (UFAM) em 2004, participando de um programa de graduação sanduíche da CAPES na Universidade de Stuttgart (Alemanha) em 2003, mestrado em Informática na área de concentração em Engenharia da Computação pela UFAM em 2007, doutorado em Ciência da Computação pela Universidade de Southampton (Inglaterra) em 2011 e estágio pós-doutoral na área de Verificação e Síntese Formal de Sistemas Ciber-físicos pela Universidade de Oxford (Inglaterra) de 2016 a 2018. Atualmente trabalha como Senior Lecturer (Professor Associado) pela Universidade de Manchester (Inglaterra), além de atuar como membro permanente nos Programas de Pós-Graduação em Engenharia Elétrica (PPGEE) e em Informática (PPGI) da UFAM. Tem experiência nas áreas de verificação e síntese formal automatizada, teorias do módulo da satisfatibilidade, teste automatizado e sistemas ciber-físicos & embarcados. Desde o término do seu doutorado em 2011, atuou como coordenador do curso de graduação em Engenharia Elétrica da UFAM de 2011 até 2015, coordenador e investigador principal em 8 projetos de pesquisa e desenvolvimento (P&D) com financiamento do CNPq, FAPEAM, Royal Society (Reino Unido), British Council (Reino Unido), Newton Fund (Reino Unido) e INdT, além de participar como pesquisador em 6 projetos de P&D com financiamento da CAPES, FAPEAM, FINEP, EPSRC (Reino Unido) e Samsung. Possui 97 publicações revisadas, incluindo 24 artigos em periódicos especializados, 73 artigos em conferências/workshops e 1 capítulo de livro, h-index de 17, dois prêmios de "Best Paper" (SBESC'15 e SAC'08), um prêmio de "Distinguished Paper" (ICSE'11), além de 20 premiações na competição internacional de verificação de software (SV-COMP 2012-2018). Lecionou um conjunto de 10 disciplinas nos cursos de graduação em Engenharia Elétrica, Engenharia da Computação e Sistemas de Informação, além de 5 disciplinas em cursos de pós-graduação em Engenharia Elétrica e Ciência da Computação. Co-orientou 1 tese de doutorado, orientou 9 dissertações de mestrado, 14 trabalhos de conclusão de curso, 6 iniciações científicas e 10 estágios supervisionados. Tem trabalhado como revisor para periódicos científicos relevantes, assim como participado do comitê de programa de conferências científicas internacionais relevantes da sua área de atuação. Possui colaboração em projetos de pesquisa com as universidades de Oxford, Cambridge, Southampton, Bristol, Stellenbosch, Universidade Federal de Minas Gerais e Universidade Federal de Viçosa. Atuou também em projetos de desenvolvimento de software relacionados à telefonia móvel, set-top box e análise de programs nas empresas Siemens/BenQ, CTPIM/NXP e Diffblue, respectivamente. (Texto informado pelo autor)


Identificação


Nome
Lucas Carvalho Cordeiro
Nome em citações bibliográficas
CORDEIRO, L. C.;Cordeiro, Lucas;Cordeiro, L.;Cordeiro, Lucas Carvalho;CORDEIRO, LUCAS C.

Endereço


Endereço Profissional
University of Manchester, School of Computer Science.
Kilburn Building
Oxford Rd, M139PL
OX13QD - Manchester, - Grã-Bretanha
Telefone: (44) 7393451110
URL da Homepage: https://ssvlab.github.io/lucasccordeiro/


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


2008 - 2011
Doutorado em Ciências da Computação.
University of Southampton, SOUTHAMPTON, Inglaterra.
Título: SMT-Based Bounded Model Checking for Multi-threaded Software in Embedded Systems, Ano de obtenção: 2011.
Orientador: Bernd Fischer.
Bolsista do(a): Overseas Research Students Awards Scheme, ORSAS, Inglaterra.
Palavras-chave: Embedded Software; Real-Time Software; Formal Verification; Bounded Model Checking.
Grande área: Ciências Exatas e da Terra
Grande Área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Metodologia e Técnicas da Computação.
2006 - 2007
Mestrado em Informática.
Universidade Federal do Amazonas, UFAM, Brasil.
Título: TXM: Uma Metodologia de Desenvolvimento de HW/SW Ágil para Sistemas Embarcados,Ano de Obtenção: 2007.
Orientador: Raimundo da Silva Barreto.
Palavras-chave: Sistemas Embarcados; Hardware e Software Codesign; Desenvolvimento de Software Ágil; Projeto Baseado em Plataforma.
Grande área: Ciências Exatas e da Terra
Setores de atividade: Informática.
2000 - 2004
Graduação em Engenharia Elétrica.
Universidade Federal do Amanzonas, UFAM, Brasil.
Título: Developing Real-Time Applications with LEGO Mindstorms.
Orientador: Peter Göhner.
1997 - 2000
Curso técnico/profissionalizante em Técnico em eletrônica.
Instituto Federal de Educação, Ciência e Tecnologia do Amazonas, IFAM, Brasil.
1999 - 1999
Ensino Médio (2º grau).
Colégio Objetivo do Amazonas, OBJETIVO, Brasil.


Pós-doutorado


2016 - 2018
Pós-Doutorado.
University of Oxford, OX, Inglaterra.
Grande área: Ciências Exatas e da Terra


Formação Complementar


2008 - 2008
Aplicações Interativas para TV digital (Ginga). (Carga horária: 20h).
Fundação Rede Amazônica, FRA, Brasil.
2007 - 2007
STB225 Digital TV Platform. (Carga horária: 120h).
NXP Semiconductors, NXP, Estados Unidos.
2007 - 2007
Middleware for Digital TV Platform. (Carga horária: 80h).
NXP Semiconductors, NXP, Inglaterra.
2006 - 2006
Ambientação em Programação C++ para Windows. (Carga horária: 24h).
Embedded Systems Technologies, ESYSTECH, Brasil.
2006 - 2006
Agile Planning and Estimation,. (Carga horária: 16h).
Object Mentor, OM, Estados Unidos.
2006 - 2006
Certified Scrum Master. (Carga horária: 16h).
Object Mentor, OM, Estados Unidos.
2005 - 2005
CMMI - Capability Maturity Model Integration. (Carga horária: 24h).
Integrated System Diagnostics Brasil, ISD BRASIL, Brasil.
2005 - 2005
CMT ? Developer Training. (Carga horária: 16h).
Siemens Com Mobile Devices, R&D, Alemanha.
2005 - 2005
Techniques and Tools for Development on Linux. (Carga horária: 32h).
Conectiva S.A., CONECTIVA, Brasil.
2005 - 2005
Administração de Sistemas Linux. (Carga horária: 30h).
Conectiva S.A., CONECTIVA, Brasil.
2004 - 2005
Proficiency In English Level Advanced. (Carga horária: 150h).
Instituto de Idiomas Yázigi, YÁZIGI, Brasil.
2004 - 2005
Alemão Nível Médio. (Carga horária: 180h).
Centro Suiço de Ensino, CSE, Brasil.
2004 - 2004
Desenvolvimento de Aplicações em J2ME usando CLDC. (Carga horária: 36h).
Qualiti Software Processes, QSP, Brasil.
2004 - 2004
Introduction to Embedded Linux. (Carga horária: 16h).
Conectiva S.A., CONECTIVA, Brasil.
2003 - 2004
Studienbegleitkurs Deutsch als Fremdsprache. (Carga horária: 90h).
Universität Stuttgart, UNI STUTTGART, Alemanha.
2003 - 2003
Intensivkurs Deutsch als Fremdsprache. (Carga horária: 140h).
Universität Stuttgart, UNI STUTTGART, Alemanha.
2002 - 2002
Projeto de Sistemas Digitais usando FPGA. (Carga horária: 40h).
Universidade Federal do Amanzonas, UFAM, Brasil.
2000 - 2001
Proficiency In English Level Pre-Intermediate. (Carga horária: 105h).
Instituto de Idiomas Yázigi, YÁZIGI, Brasil.
1998 - 2000
General Proficiency In English Level Elementary. (Carga horária: 100h).
Instituto de Idiomas Yázigi, YÁZIGI, Brasil.


Atuação Profissional



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

2015 - Atual
Vínculo: Servidor Público, Enquadramento Funcional: Professor Adjunto III, Carga horária: 40, Regime: Dedicação exclusiva.

Vínculo institucional

2013 - 2015
Vínculo: Servidor Público, Enquadramento Funcional: Professor Adjunto II, Carga horária: 40, Regime: Dedicação exclusiva.

Vínculo institucional

2009 - 2011
Vínculo: Servidor Público, Enquadramento Funcional: Professor Assistente, Carga horária: 40, Regime: Dedicação exclusiva.

Vínculo institucional

2004 - 2004
Vínculo: Bolsista, Enquadramento Funcional: Bolsista, Carga horária: 20
Outras informações
Produção e Uso da Biomassa para fins Energéticos

Vínculo institucional

2002 - 2003
Vínculo: Bolsista, Enquadramento Funcional: Bolsista, Carga horária: 20
Outras informações
Levantamento do sistema de Ar-Condicionado na Universidade Federal do Amazonas

Vínculo institucional

2001 - 2002
Vínculo: Bolsista, Enquadramento Funcional: Bolsista, Carga horária: 20
Outras informações
Estudo das Características do Solo de Manaus para Sistemas de Aterramento Ótimo

Vínculo institucional

2001 - 2001
Vínculo: Bolsista, Enquadramento Funcional: Bolsista, Carga horária: 20
Outras informações
Redução de Custo e Gerenciamento de Energia

Atividades

08/2011 - Atual
Ensino, Engenharia Elétrica, Nível: Pós-Graduação

Disciplinas ministradas
Algoritmos para Automação e Sistemas - PGENE538
Projeto e Análise de Algoritmos - PGENE533
Sistemas de Tempo Real - PGENE503
Verificação de Software e Sistemas - PGENE549
Estudo Especial - PGENE525
09/2009 - Atual
Ensino, Engenharia da Computação, Nível: Graduação

Disciplinas ministradas
Arquitetura de Sistemas Digitais - FTL065
Programação Avançada - FTL057
Programação em Tempo Real - FTL066
Projeto de Final de Curso I - FTL068
Redes de Computadores - FTL085
Laboratório de Arquitetura de Sistemas Digitais - FTL067
11/2002 - 11/2002
Treinamentos ministrados , Faculdade de Tecnologia, Departamento de Eletricidade.

Treinamentos ministrados
Desenvolvimento de Software de Controle para Dispositivos remoto

University of Manchester, MANCHESTER, Inglaterra.
Vínculo institucional

2018 - Atual
Vínculo: Servidor Público, Enquadramento Funcional: Senior Lecturer, Carga horária: 35


University of Oxford, OX, Inglaterra.
Vínculo institucional

2016 - 2018
Vínculo: , Enquadramento Funcional: Estágio Pós-doutoral, Carga horária: 37, Regime: Dedicação exclusiva.


BenQ Eletroeletrônica S.A, BENQ MOBILE, Brasil.
Vínculo institucional

2006 - 2007
Vínculo: Colaborador, Enquadramento Funcional: Engenheiro de Software Embarcado, Carga horária: 44, Regime: Dedicação exclusiva.
Outras informações
Análise de requisitos, projeto, implementação, integração e manutenção de projetos de sistemas embarcados. Concepção e integração de sistemas operacionais de tempo-real em arquiteturas ARM, desenvolvimento de ?class drivers? para aplicação USB e interface homem-máquina.

Atividades

01/2007 - 03/2007
Pesquisa e desenvolvimento , Grupo de Desenvolvimento de Hardware, .


Siemens Eletroeletrônica S.A - P&D Manaus, SIEMENS, Brasil.
Vínculo institucional

2005 - 2006
Vínculo: Celetista, Enquadramento Funcional: Feature Leader, Carga horária: 44, Regime: Dedicação exclusiva.
Outras informações
Planejamento e rastreamento de projeto focado em funcionalidades do software. As atividades mais significantes são: definição de pacote de trabalho e planejamento de projeto (schedule, dependências e gerenciamento de risco). Além disso, coordenação de entrega dos pacotes de trabalho dos parceiros e rastreamento de bugs no software.

Vínculo institucional

2005 - 2005
Vínculo: Celetista, Enquadramento Funcional: Software Configuration and Build Manager, Carga horária: 44, Regime: Dedicação exclusiva.
Outras informações
Planejamento de gerência de configuração de software, gerência de mudança, release e versão, gerência de build e processo de rastreamento de bugs do projeto XMPM para geração 75 e 85 de telefones celulares. Além disso, foi desenvolvido durante o projeto o processo de aprimoramento de arquitetura do XMPM com o propósito de coletar, avaliar e realizar as solicitações de mudança na arquitetura.

Vínculo institucional

2004 - 2004
Vínculo: Estágio, Enquadramento Funcional: Estagiário, Carga horária: 30
Outras informações
Conceituação do sistema operacional Linux, Enhanced Message Service (EMS) e comandos AT para comunicação com o celular. Abordagem prática de Java Native Interface (JNI) para telefones celulares da Siemens e revisão de documentos técnicos dos parceiros.

Atividades

08/2005 - 06/2006
Pesquisa e desenvolvimento , Siemens P&D, .


Universität Stuttgart, UNI STUTTGART, Alemanha.
Vínculo institucional

2003 - 2004
Vínculo: Bolsista, Enquadramento Funcional: Bolsista, Carga horária: 40, Regime: Dedicação exclusiva.
Outras informações
Participação no projeto UniBrAl (Universidades Brasil e Alemanha) sendo bolsista da CAPES no período de 03/2003 a 02/2004 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 Alemanha apresenta um alto nível de desenvolvimento tecnológico e cultural.

Atividades

11/2003 - 02/2004
Estágios , Institut für Automatisierungs- und Softwaretechnik - IAS, .

Estágio realizado
Programção de micro-controlador e desenvolvimento de circuitos condicionadores de sinais.
03/2003 - 02/2004
Pesquisa e desenvolvimento , Institut für Automatisierungs- und Softwaretechnik - IAS, .


Telecomunicações do Amazonas S/A, TELEMAR, Brasil.
Vínculo institucional

1999 - 2000
Vínculo: Estagiário, Enquadramento Funcional: Coordenador de Manutenção, Carga horária: 30
Outras informações
Programação de assinantes digitais das centrais telefônicas da NEC. Manutenção corretiva em Unidades de Linha Estendida nas centrais NEAX61BR e NEAX61BR/SIGMA. Observaram-se as configurações principais de uma central telefônica e equipamentos de terminal, redes de comunicação e o relacionamento entre funções e serviços tais como fornecimento de conexões, transporte e armazenamento de informações e gerenciamento de rede.

Atividades

12/1999 - 09/2000
Estágios .

Estágio realizado
Centrais Telefônicas.

ACE Engenharia, ACE, Brasil.
Vínculo institucional

1996 - 1997
Vínculo: Estagiário, Enquadramento Funcional: Técnico de Manutenção, Carga horária: 20
Outras informações
Manutenção de computadores e desenvolvimento de software para gerenciamento de estoque com o uso das ferramentas Clipper e Delphi. A experiência serviu para o entendimento da arquitetura do PC AT, a familiaridade com lógica e técnicas de programação, assim como a programação orientada a objetos.

Atividades

02/1996 - 11/1997
Estágios .

Estágio realizado
Manutenção de microcomputadores e programação comercial.

Centro de Ciências, Tecnologia e Inovação do Pólo Industrial de Manaus, CTPIM, Brasil.
Vínculo institucional

2007 - 2008
Vínculo: Colaborador, Enquadramento Funcional: Pesquisador, Carga horária: 44, Regime: Dedicação exclusiva.
Outras informações
Desenvolvimento do driver Linux para o tuner DVB-T e ISDB-T na plataforma digital STB225 (Set-top Box). Migração da aplicação do tuner ATSC de um produto anterior para a plataforma STB225. Concepção e implementação dos testes unitários e funcionais para os devices drivers do Linux através do uso de framework de teste e shell scripts (automação de testes). Porte de um middleware para IPTV e desenvolvimento de aplicações de software para plataforma STB225.


Escola Superior Batista do Amazonas, ESBAM, Brasil.
Vínculo institucional

2007 - 2008
Vínculo: Colaborador, Enquadramento Funcional: Professor, Carga horária: 12
Outras informações
Professor do Curso de Sistemas de Informação

Atividades

02/2008 - 08/2008
Ensino, Sistemas de Informação, Nível: Graduação

Disciplinas ministradas
Algoritmos e Estruturas de Dados II
Algoritmos e Lógica de Programação
Pesquisa Operacional
08/2007 - 11/2007
Ensino, Sistemas de Informação, Nível: Graduação

Disciplinas ministradas
Engenharia de Software I

University of Southampton, SOUTHAMPTON, Inglaterra.
Vínculo institucional

2008 - 2011
Vínculo: Colaborador, Enquadramento Funcional: Doutorando, Carga horária: 44, Regime: Dedicação exclusiva.

Vínculo institucional

2010 - 2010
Vínculo: Colaborador, Enquadramento Funcional: Teaching Assistant, Carga horária: 8



Linhas de pesquisa


1.
Pattern Languages of Programming
2.
Engenharia de Software para Sistemas em Tempo Real
3.
Real-Time Software
4.
Embedded Agile Methodology
5.
Platform-Based Design
6.
Hardware/Software Co-Design


Projetos de pesquisa


2018 - Atual
Pesquisa e Desenvolvimento de Métodos Algorítmicos para Verificação de Software Embarcado em Veículos Aéreos Não Tripulados usando Aprendizagem de Máquina
Descrição: O objetivo principal deste projeto de pesquisa é propor e avaliar um método algorítmico para a prova de corretude de VANTs, escritos em linguagens de programação como C/C++, através de técnicas de SMT, indução matemática, invariantes, interpretação abstrata e aprendizagem de máquina. Em especial, será demonstrada uma forma de detectar problemas no projeto de VANTs, levando-se em consideração aspectos de implementação das regras de aprendizado e raciocínio, além de propriedades específicas das linguagens de programação C/C++..
Situação: Em andamento; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (2) / Doutorado: (4) .
Integrantes: Lucas Carvalho Cordeiro - Coordenador / Waldir Sabino da Silva Junior - Integrante / IURY VALENDE DE BESSA - Integrante / Alessandro Bezerra Trindade - Integrante / Vicente Ferreira de Lucena Júnior - Integrante / CHAVES FILHO, JOAO EDGAR - Integrante / Marco Antônio Pinheiro de Cristo - Integrante.Financiador(es): Fundação de Amparo a Pesquisa do Estado do Amazonas - Auxílio financeiro.
2018 - Atual
Aumentando a Confiabilidade de Sistemas Industriais através da Verificação Formal de Aplicações de Software para Indústria 4.0
Descrição: O tema deste projeto é extremamente pertinente para o Polo Industrial de Manaus (PIM), principal força motriz da economia do Amazonas e de Manaus, cidade sede da UFAM. Os resultados desta pesquisa deverão ser integrados em um modelo técnico que simule conceitos e definições de Indústria 4.0. Este modelo será útil para confirmar as hipóteses de pesquisa, ajudará a transferir tecnologia para a indústria local, e alavancará novas abordagens de pesquisa a serem desenvolvidas na UFAM. Em resumo, o projeto contribuirá para que os pesquisadores envolvidos se alinhem com o estado da arte de um dos temas mais relevantes da indústria moderna e permitir que as indústrias do PIM integrem conceitos da vanguarda da manufatura mundial..
Situação: Em andamento; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (2) / Doutorado: (3) .
Integrantes: Lucas Carvalho Cordeiro - Coordenador / IURY VALENDE DE BESSA - Integrante / Vicente Ferreira de Lucena Júnior - Integrante / TRINDADE, ALESSANDRO B. - Integrante / CHAVES FILHO, JOAO EDGAR - Integrante / Tayana Uchôa Conte - Integrante.Financiador(es): Fundação de Amparo a Pesquisa do Estado do Amazonas - Auxílio financeiro.
2017 - Atual
Fomento à Produção Científica do Grupo de Pesquisa em Verificação de Software e Sistemas
Descrição: O objetivo principal deste projeto é viabilizar a publicação de artigos científicos qualificados sobre temas de interesse do grupo proponente, em especial, temas relacionados aos métodos algorítmicos para prova de corretude de sistemas embarcados com aplicações em sistemas de controle, processamento digital de sinais e engenharia biomédica, utilizando técnicas das teorias do módulo da satisfatibilidade e indução matemática. Tais temas estão sendo investigados nos últimos anos pelos professores e pesquisadores participantes ativos dos Programas de Pós-Graduação em Engenharia Elétrica (PPGEE) e em Informática (PPGI) da Universidade Federal do Amazonas (UFAM). O projeto conta ainda com a cooperação de professores atuantes nos programas de pós-graduação de áreas afins que trabalham na Universidade Federal de Minas Gerais (UFMG) e Universidade Federal do Rio de Janeiro (UFRJ)..
Situação: Em andamento; Natureza: Pesquisa.
2016 - 2017
DSVerifier: A Bounded Model Checking Tool to Verify Digital Systems with Uncertainties
Descrição: Digital controllers are widely used by the control engineering community because of various advantages over analog controllers such as improved reliability, sensitivity, flexibility, and cost. However, there are disadvantages in the use of digital controllers, e.g., errors that are introduced during the quantization process. In this context, there are some initiatives to solve problems that appear in the discrete-time domain; in particular, problems related to the finite word-length (FWL) effects. For this project, a bounded model checking tool for verifying closed-loop digital control systems with uncertainties is proposed, named ?Digital System Verifier? (DSVerifier). DSVerifier checks the stability and performance of digital systems considering FWL effects. This project will provide the software library support, which is needed for CBMC, to verify common closed-loop associations of digital control systems (series and feedback), check typical properties of digital control systems (overflow and limit cycle), and verify stability and quantization noise for uncertain plant models, considering unknown parameters and FWL effects. We aim to disseminate our work via Mathworks, the leading vendor in the domain..
Situação: Concluído; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (1) / Doutorado: (2) .
Integrantes: Lucas Carvalho Cordeiro - Coordenador / João Edgar Chaves Filho - Integrante / IURY VALENDE DE BESSA - Integrante / Hussama Ibrahim Ismail - Integrante / Felipe Rodrigues Monteiro Sousa - Integrante / Daniel Kroening - Integrante / Lennon Chaves - Integrante.Financiador(es): Agency for funding research in engineering and the physical sciences - Outra.
2016 - Atual
DSVerifier-Aided Verification Applied to Control Software in Unmanned Aerial Vehicles
Descrição: Este projeto tem como objetivo financiar a visita do Prof. Dr. Michael Tautschnig da Queen Mary University of London para trabalhar no desenvolvimento de métodos algorítmicos para verificação de modelos baseados em prova de corretude por indução matemática, invariantes e interpretação abstrata, com o intuito de aplicá-los na verificação de software de controle embarcado em Veículos Aéreos Não Tripulados (VANTs)..
Situação: Em andamento; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (2) / Doutorado: (3) .
Integrantes: Lucas Carvalho Cordeiro - Coordenador / Eddie Batista de Lima Filho - Integrante / FILHO, JOAO EDGAR CHAVES - Integrante / IURY VALENDE DE BESSA - Integrante / Hussama Ibrahim Ismail - Integrante / Michael Tautsching - Integrante.Financiador(es): Conselho Nacional das Fundações Estaduais de Amparo à Pesquisa - Auxílio financeiro.
2014 - 2015
Verificação de Programas C/C++ Baseados em Processadores de Vários Núcleos
Descrição: O principal objetivo deste projeto consiste em pesquisar, implementar e validar técnicas de verificação estática de código para checar propriedades relacionadas à corrida de dados, bloqueio fatal, estouro aritmético e de vetores, divisão por zero e segurança de ponteiros de kernels de unidades de processamento gráfico (GPU, do inglês Graphics Processing Units). Serão considerados kernels desenvolvidos usando as linguagens de programação OpenCL e CUDA. A validação deste projeto terá como objetivo demonstrar a eficiência e eficácia, das técnicas propostas, para verificar um amplo conjuntos de programas CUDA e OpenCL para GPU kernels..
Situação: Concluído; Natureza: Pesquisa.
2014 - 2015
Verificação de Hardware e Software Baseada em Indução Matemática para Sistemas Embarcados
Descrição: Neste projeto será tratada uma abordagem para verificação de modelos baseada em prova de corretude por indução matemática para programas C/C++. Esta técnica será investigada para tratar da prova de programas que envolvem concorrência (tipicamente encontrado em sistemas que contém vários núcleos de processamento) e manipulação da memória heap (tipicamente encontrado em sistemas operacionais). Os algoritmos desenvolvidos neste projeto serão implementados utilizando a ferramenta Efficient SMT-Based Context-Bounded Model Checker (ESBMC), que é um verificador de modelos estado da arte, o qual se baseia em teorias de satisfatibilidade de fórmulas proposicionais e lógica de primeira ordem. Vale ressaltar que este projeto será validado através de técnicas formais e experimentais, as quais serão conduzidas com o intuito de mostrar que a abordagem proposta pode ser utilizada para verificar uma grande quantidade de aplicações, que vão desde casos simples a aplicações embarcadas comerciais mais complexas. Sendo assim, o principal resultado deste projeto consistirá em mostrar que a abordagem proposta, implementada através de uma ferramenta computacional, será capaz de verificar aplicações reais, e que tal ferramenta será mais eficiente do que outros verificadores, no que tange a verificação de sistemas embarcados. Neste sentido, pretende-se implementar a abordagem proposta e mostrar que a mesma encontra um maior número de erros, além de suportar um maior número de funcionalidades das linguagens C/C++, quando comparado com outras ferramentas (comerciais ou acadêmicas) disponíveis. Além disso, a abordagem proposta deverá ser o mais flexível possível, possibilitando a extensão da mesma para outras linguagens de programação (por exemplo, Java), e deverá também ser capaz de provar por indução matemática diversas propriedades inerentes não somente às linguagens C/C++ (tais como, overflow aritmético e divisão por zero) mas como também inerentes ao próprio sistema embarcado (tais como, estabilidade e ruídos)..
Situação: Concluído; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (4) / Mestrado acadêmico: (3) .
Integrantes: Lucas Carvalho Cordeiro - Coordenador / VicenteFerreira Lucena Júnior - Integrante / Waldir Sabino da Silva Junior - Integrante / Eddie Batista de Lima Filho - Integrante / Celso Barbosa Carvalho - Integrante / André Luiz Duarte Cavalcante - Integrante / Patrícia Nascimento Pena - Integrante.Financiador(es): Fundação de Amparo a Pesquisa do Estado do Amazonas - Auxílio financeiro.
Número de produções C, T & A: 5
2014 - 2015
Verificação de Modelos Limitada Baseado nas Teorias do Módulo da Satisfatibilidade para Programas Multi-tarefa
Descrição: Devido às limitações físicas, novos aumentos no poder de computação não podem mais ser alcançados por processadores mais rápidos, mas apenas por hardware concorrente, que vão desde processadores com vários núcleos individuais a grandes clusters Linux. Programação Concorrente experimenta, assim, um interesse renovado, mas a construção de sistemas confiáveis de software concorrentes ainda é um problema difícil. Esta proposta de projeto trata deste problema em particular. Em especial, propõem-se três objetivos na verificação de sistemas concorrentes com o intuito de garantir a sua confiabilidade: (1) Explorar a concorrência onipresente, para acelerar a verificação baseada em lógica, em particular verificação de modelos simbólica baseada em SAT/SMT, de sistemas de software grandes e distribuídos. (2) Aproveitar a estrutura de alto nível de programas para quebrar a análise e verificação de sistemas concorrentes em tarefas independentes, que possam ser resolvidas simultaneamente, com interfaces mínimas entre essas tarefas. (3) Empregar métodos dinâmicos de análise para detectar defeitos de concorrência e projetar algoritmos para mostrar os caminhos do código que apresentam esses defeitos..
Situação: Concluído; Natureza: Pesquisa.
Alunos envolvidos: Mestrado acadêmico: (1) Doutorado: (2) .
Integrantes: Lucas Carvalho Cordeiro - Coordenador / Jeremy Morse - Integrante / Denis Nicole - Integrante / FISCHER, BERND - Integrante / Mikhail Yasha Ramalho Gadelha - Integrante.Financiador(es): British Council - Cooperação.
Número de produções C, T & A: 6
2013 - 2016
Verificação de Propriedades Temporais em Software Embarcado usando as Teorias do Módulo da Satisfatibilidade
Descrição: 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: Concluído; Natureza: Pesquisa.
Alunos envolvidos: Mestrado acadêmico: (1) Doutorado: (1) .
Integrantes: Lucas Carvalho Cordeiro - Coordenador / VicenteFerreira Lucena Júnior - Integrante / Jeremy Morse - Integrante / Denis Nicole - Integrante / Waldir Sabino da Silva Junior - Integrante / Mikhail Yasha Ramalho Gadelha - Integrante.Financiador(es): Conselho Nacional de Desenvolvimento Científico e Tecnológico - Auxílio financeiro.
Número de produções C, T & A: 14 / Número de orientações: 6
2013 - 2015
Investigação de Técnicas Modernas de Desenvolvimento de Software para Automação Industrial visando Sustentabilidade Energética e Interação Eficaz com o Usuário
Descrição: Novas áreas da Ciência da Computação, Eletrônica, e da Engenharia da Computação, como Automação Industrial, Engenharia Biomédica, Engenharia de Software, etc., já provaram ser de fundamental importância para a sociedade nos tempos atuais e futuros, e vêm exigindo uma crescente e contínua atualização dos profissionais envolvidos tanto no ensino e na pesquisa quanto na aplicação de novas soluções tecnológicas para tais temas. Neste aspecto em particular as universidades alemãs podem contribuir com as brasileiras, uma vez que aquelas têm grande experiência na transferência de tecnologia para sua indústria e já vem investigando os temas citados há muito tempo. A subárea a ser trabalhada neste projeto engloba temas promissores e desafiantes ligados a uma importante área da Ciência da Computação e da Engenharia da Computação: o Desenvolvimento de Software para Sistemas de Automação Industrial. Das missões de pesquisa acrescentarão uma experiência internacional importante para nosso grupo de trabalho. Os professores envolvidos poderão comparar os temas investigados pelas duas instituições e adotar técnicas e metodologias que sejam adaptáveis para a realidade brasileira. Os temas de pesquisa que estarão relacionados a este projeto dizem respeito ao desenvolvimento de software para automação industrial utilizando técnicas modernas. Em particular serão estudadas novas formas de interface com usuário para sistemas de automação industrial, e mecanismos baseados em software para otimização de energia para estes mesmos sistemas. O objetivo é, juntamente com a Universidade Parceira, investigar o que existe de mais modernos nestes temas e construir modelos de processo que possam servir de exemplos de aplicação tanto em Manaus como em Stuttgart. O intercâmbio aqui proposto vai permitir um aprendizado da experiência alemã na formação de profissionais em automação industrial e principalmente colocará o grupo proponente em contato com as linhas de pesquisa de uma das mais importantes universidades alemães nesta área do conhecimento..
Situação: Concluído; Natureza: Pesquisa.
2013 - 2015
Pesquisa e Desenvolvimento de Serviços Digitais para Acompanhamento de Prescrições Médicas baseados em Ambientes Inteligentes
Descrição: O problema a ser tratado neste projeto de pesquisa envolve a identificação de novos serviços e aplicações de AmI relacionados à saúde e ao bem estar do ser humano, particularmente no que diz respeito à administração de medicamentos. Isso envolve a concepção, implementação e validação de serviços digitais interativos. O objetivo será propor soluções inovadoras que façam uso de dispositivos eletrônicos convencionais para ajudar a manter a saúde e a qualidade de vida de pessoas com alguma deficiência física ou de idosos. Para tanto, será necessário estudar as tecnologias envolvidas na construção dos Ambientes Inteligentes e desenvolver dispositivos (hardware e software) que permitam aprimorar os serviços a serem ofertados aos pacientes. Será implementada uma prova de conceito para ajudar pacientes a tomarem remédios no horário correto segundo uma prescrição médica. Esse sistema utilizará telefones celulares, tablets, e/ou TV Digital interativa como interface com o paciente. Será construído ainda um dispositivo eletrônico capaz de identificar qual remédio será tomado pelo paciente. Um sistema de software inteligente supervisionará o ato de tomar remédio visando minimizar eventuais erros.
Situação: Concluído; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (2) / Mestrado acadêmico: (2) / Doutorado: (1) .
Integrantes: Lucas Carvalho Cordeiro - Integrante / VicenteFerreira Lucena Júnior - Coordenador / Waldir Sabino da Silva Junior - Integrante / Victor Valenzuela - Integrante / Vandermi João da Silva - Integrante / Claudio Eduardo Marques Gomes - Integrante.
2012 - 2017
Pesquisa e Desenvolvimento de Tecnologias de Base para Ambientes Inteligentes Industriais
Descrição: Neste projeto, um grupo de professores do Programa de Pós-Graduação em Engenharia Elétrica da UFMG interessados em temas relacionados aos ambientes inteligentes realizará ações conjuntas com um grupo de professores do Mestrado em Engenharia Elétrica da UFAM. O projeto terá duração de 4 anos. O objetivo geral do projeto é estabelecer uma parceria de pesquisa e desenvolvimento entre grupos de professores, de forma que os colegas da UFAM, com o suporte dos colegas da UFMG, consigam alavancar temas de interesse para a região, conquistar mais alunos de mestrado em Manaus e alcançar níveis de produção científica que permitam a consolidação do programa da UFAM. Especificamente pretende-se investigar, identificar e propor novas abordagens científicas e tecnológicas que viabilizem a construção de Ambientes Inteligentes com aplicação na Indústria. Esses estudos se concentrarão principalmente em sistemas de controle modernos e no desenvolvimento sistemas de software para aplicações de inteligência artificial. Os temas investigados estão distribuídos em cinco linhas de pesquisa que caracterizam atualmente o Programa de Pós-Graduação em Engenharia Elétrica da UFAM e que poderão se beneficiar das áreas de competência no Programa de Pós-Graduação em Engenharia Elétrica da UFMG: Os temas investigados serão agrupados em dois conjuntos principais: a) Sistemas de Controle, Automação Industrial e Robótica b) Desenvolvimento de Software para Sistemas de Tempo Real e Inteligência Artificial Aplicada..
Situação: Concluído; Natureza: Pesquisa.
2011 - 2013
Continuous Verification of C++ Programs Using SMT-based Bounded Model Checking
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: Lucas Carvalho Cordeiro - Coordenador / Mikhail Ramalho - Integrante / Bruno Savino - Integrante / Andrey Bessa - Integrante / Felipe Rodrigues - Integrante / Mauro Freitas - Integrante.Financiador(es): Instituto Nokia de Tecnologia - Bolsa.
Número de produções C, T & A: 4 / Número de orientações: 1
2011 - 2013
SMT-Based Bounded Model Checking Timed LTL Properties for Embedded Software
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: Concluído; Natureza: Pesquisa.
Alunos envolvidos: Mestrado acadêmico: (1) Doutorado: (5) .
Integrantes: Lucas Carvalho Cordeiro - Integrante / Raimundo da Silva Barreto - Integrante / Jeremy Morse - Integrante / Denis Nicole - Integrante / FISCHER, BERND - Coordenador / Mikhail Yasha Ramalho Gadelha - Integrante.Financiador(es): Royal Society - Cooperação.
Número de produções C, T & A: 3 / Número de orientações: 1
2008 - 2010
NOTOS: New algOrithm for LTL mOdel checking with Satisfiability
Descrição: Boolean Satisfiability (SAT) is the paradigmatic NP-complete decision problem. Besides its theoretical interest, SAT finds a vast number of applications in a large number of areas, including system validation by model checking. Over the last decade the area of SAT algorithms has witnessed a remarkable evolution. From an essentially academic curiosity in the early 90s, SAT technology has made great strides, and is now extensively used in a large number of practical applications. The evolution of SAT technology has been marked by a number of key ideas, which have shaped the organisation of current state of the art SAT solvers. Model checking is an essential technique for system validation and, arguably, it is one of the most successful applications of SAT solver technology. The improvements made to SAT solvers motivated their usage in model checking. The first uses of SAT were for Bounded Model Checking (BMC), a potentially incomplete form of model checking. More recent work has addressed completeness issues, in the form of Unbounded Model Checking (UMC). The use of SAT in model checking has yielded remarkable performance gains in different settings, having motivated the widespread offering, by most Electronic Design Automation (EDA) vendors, of commercial tools using SAT-based model checking. Nevertheless, the utilisation of SAT in publicly available robust model checkers is still scarce, the most well-known example being NuSMV. However, in NuSMV SAT is solely used for incomplete forms of bounded model checking. The dissemination of a publicly available SAT-based model checker will enable further research work on SAT-based model checking, and will provide a comparison framework for alternative model checking strategies. Moreover, model checking is a hard computational problem, and the ever increasing complexity of the systems to be verified motivates the development of new effective techniques. The NOTOS project will conduct innovative research on a number of topics.
Situação: Concluído; Natureza: Pesquisa.
Alunos envolvidos: Mestrado acadêmico: (1) Doutorado: (2) .
Integrantes: Lucas Carvalho Cordeiro - Integrante / João Paulo Marques-Silva - Integrante / FISCHER, BERND - Coordenador.Financiador(es): Agency for funding research in engineering and the physical sciences - Remuneração.
Número de produções C, T & A: 3 / Número de orientações: 2
2008 - 2010
COCONUT: A Correct-by-Construction Workbench for Design and Verification of Embedded Systems.
Descrição: The COCONUT project is intended to propose a modelling and verification flow to enhance and speed-up embedded platform?s design and configuration with particular regard to application fields related to mixed continuous/discrete models, like for example networked multimedia and sensor network management. The embedded platform market is converging on a limited but more powerful set of embedded platforms, mainly due to increasing design cost which requires higher production volume. Differentiation among effective platform configurations is thus a key advantage for a platform user to approach the market with innovative solutions. Design and verification of such a kind of embedded platforms are two highly related problems which are still mainly faced by using unrelated methodologies. The proposed project is thus focused on a tight integration of design and verification throughout all refinement steps of an embedded platform design, from specifications to logic synthesis and software compilation. The complexity of both platform design and platform configuration requires an innovative design and verification flow able to effectively reduce the number of design errors and design recycles. This is a key factor for increasing system development productivity while achieving predictable system properties. Moreover, an incremental and hierarchical verification strategy is fundamental to manage the huge complexity of this embedded platform that cannot be verified in the whole at a structural level such as RTL. Even at TLM the platform modelling would be difficult due to the presence of complex networks and continuous-time information. As a result, the addition of hybrid automata to SystemC TLM models will be proposed for tackling the modelling complexity. In both platform design and platform configuration, this very abstracted platform description requires correct-by-construction refinements and/or automatic verification of manual refinements, to translate, without design error.
Situação: Concluído; Natureza: Pesquisa.
Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (2) / Doutorado: (2) .
Integrantes: Lucas Carvalho Cordeiro - Integrante / João Paulo Marques-Silva - Coordenador / John Colley - Integrante / Paulo J. Matos - Integrante / Rob Quigley - Integrante.Financiador(es): European Commission - Bolsa.
Número de produções C, T & A: 9


Projetos de desenvolvimento


2013 - 2016
Pesquisa e formação de recursos humanos, em nível de graduação e pós-graduação, nas áreas deautomação industrial, software para dispositivos móveis e TV Digital
Descrição: Projeto iniciado em setembro de 2013, com término previsto para setembro de 2016 e financiamento no valor de R$ 7.190.549,47. Os objetivos desse projeto são: treinamento de recurso humanos em nível de graduação e pós-graduação; Condução de atividades em Desenvolvimento e Pesquisa Tecnológica (P&D) e Instalação de uma estrutura física para o P&D. No tocante a formação de recursos humanos em nível de graduação pretende-se, ao longo dos três anos, formar entre 90 e 120 alunos, através de projetos de extensão, nas áreas de automação industrial, TV Digital e Dispositivos Móveis. No tocante a formação de recursos humanos em nível de pós-graduação, pretende-se formar entre 12 e 16 mestres no Programa de Pós-Graduação em Engenharia Elétrica. Tanto os alunos de graduação como os alunos de pós-graduação receberão bolsas pagas pela Samsung. As atividades de Pesquisa previstas no projeto serão conduzidas nos trabalhos de dissertação de mestrado. No que tange a infra-estrutura física está previsto a expansão da área física do CETELI em 50%, com a construção de um segundo prédio de 900m2. Nesse novo prédio os seguintes ambientes serão disponibilizados: 5 ambientes de projetos, 2 salas de aula, sala de reunião, sala de convivência, salas de alunos e salas de professores. Além de construir o prédio, a empresa Samsung aparelhará todos os ambientes. Destaca-se o aparelhamento de três laboratórios voltados a formação de recursos humanos e pesquisa: laboratório de automação industrial, laboratório de TV digital e laboratório de dispositivos móveis..
Situação: Concluído; Natureza: Desenvolvimento.
Alunos envolvidos: Técnico de nível médio: (21) Graduação: (99) / Mestrado acadêmico: (16) .
Integrantes: Lucas Carvalho Cordeiro - Integrante / VicenteFerreira Lucena Júnior - Integrante / Waldir Sabino da Silva Junior - Integrante / FILHO, JOAO EDGAR CHAVES - Integrante / Marly Guimarães Fernandes Costa - Integrante / Cícero Ferreira Fernandes Costa Filho - Coordenador / André Luiz Duarte Cavalcante - Integrante.Financiador(es): Samsung Eletrônica da Amazônia - Auxílio financeiro.
Número de produções C, T & A: 5 / Número de orientações: 1
2012 - 2016
Arquitetura para uma Cadeira de Rodas Integrada em um Ambiente Inteligente
Descrição: O objetivo geral do projeto é a concepção e o desenvolvimento de uma arquitetura para integração de equipamentos de mobilidade (e.g., cadeira de rodas) em um ambiente inteligente. Com esta proposta, usuários portadores de necessidades especiais poderão interagir com sua cadeira de rodas e com um ambiente inteligente, composto por um sistema automatizado utilizando a tecnologia da televisão digital, a partir de sinais biológicos coletados. Para isso, destacamos alguns pontos importantes: Deve haver uma interface entre o usuário cadeirante e seu equipamento de mobilidade e entre este e o sistema de automação residencial/de escritório/industrial, que permita ao usuário incluir-se socialmente, em casa ou no trabalho. A interface entre o cadeirante e o equipamento de mobilidade (i.e., cadeira de rodas) deve ser tal que nenhum ou pouco esforço por parte do usuário é requerido para o seu uso. Algum treinamento pode ser necessário, mas não deve significar uma completa modificação de hábitos ou estilo de vida. A interface entre o equipamento de mobilidade e uma rede TIC (tecnologia de informação e comunicação) deve ser aberta e padronizada para que os sistemas possam interoperar autonomamente, sem grandes interferências do usuário ou administradores do sistema. Um ambiente inteligente deve ser capaz de entender o contexto de limitações de mobilidade de uma cadeira de rodas quando inserida no ambiente. Este projeto será realizado em parceria com duas grandes universidades brasileiras, a Universidade Federal do Rio Grande do Sul através do grupo do professor Carlos Eduardo Pereira, e a Universidade Federal do Espírito Santo através do grupo do professor Teodiano Freire Bastos Filho. Estão previstas orientações conjuntas de alunos de doutorado, mestrado, e de iniciação científica..
Situação: Concluído; Natureza: Desenvolvimento.
Alunos envolvidos: Graduação: (6) / Mestrado acadêmico: (3) / Doutorado: (2) .
Integrantes: Lucas Carvalho Cordeiro - Integrante / VicenteFerreira Lucena Júnior - Coordenador / Waldir Sabino da Silva Junior - Integrante / FILHO, JOAO EDGAR CHAVES - Integrante / Carlos Eduardo Pereira - Integrante / André Luiz Duarte Cavalcante - Integrante / Teodiano Freire Bastos Filho - Integrante.Financiador(es): Financiadora de Estudos e Projetos - Outra.
2004 - 2006
linuX Mobile Phone Manager
Descrição: Este projeto visa o desenvolvimento de um software para o sistema operacional Linux responsável pelo controle de acesso ao celular, gerenciamento de informações pessoais (PIM), short message service (SMS), acesso a internet via GPRS e sincronização de dados entre o telefone celular e PC. Além disso, o sistema de arquivo do celular é montado no PC possibilitando o software de acessar músicas, filmes e figuras. O usuário também é capaz de modificar as propriedades do celular tais como: língua, som e tipo de toque. A comunicação entre o PC e celular pode ser estabelecida usando cabo serial, USB ou bluetooth..
Situação: Concluído; Natureza: Desenvolvimento.
Alunos envolvidos: Graduação: (1) / Especialização: (2) / Mestrado acadêmico: (2) / Mestrado profissional: (1) / Doutorado: (0) .
Integrantes: Lucas Carvalho Cordeiro - Integrante / Dario André Louzado - Integrante / Cassiano Otávio Becker - Integrante / Ana Heloísa Bastos - Coordenador / Juliano João Bazzo - Integrante / Fabio Higa - Integrante.Financiador(es): BenQ Eletroeletrônica S.A - P&D Manaus - Auxílio financeiro.
Número de produções C, T & A: 2
2004 - 2004
Aquisição de Dados de Processo de um Gasogênio à Carvão Vegetal para Geração de Energia Elétrica
Descrição: O projeto visa o desenvolvimento de um sistema de aquisição de dados no processo de gaseificação em um gaseificador de leito fixo a carvão vegetal para acionamento do motor de combustão interna, visando a geração de força motriz, com potência no eixo do motor na faixa de 5 a 15 Hp. O gaseificador é do tipo co-corrente com injeção central de ar. Deste modo, o sistema monitora a unidade de gaseificação, sistema de purificação e resfriamento e sistema de conversão da energia final. A arquitetura do software é baseada na infra-estrutura Model-View-Controller tendo o MySQL como base de dados. Deste modo, o software monitora as variáveis de processo tensão e corrente nos terminais do gerador síncrono trifásico assim como temperatura e pressão entre cada processo do sistema. Além disso, o sistema monitora a umidade relativa do ar. A partir dos dados mensurados pelos sensores, o software é capaz de processar, armazenar e extrair as informações de um banco de dados com o propósito de analisar o desempenho do equipamento..
Situação: Concluído; Natureza: Desenvolvimento.
Alunos envolvidos: Graduação: (1) / Mestrado acadêmico: (1) / Doutorado: (2) .
Integrantes: Lucas Carvalho Cordeiro - Integrante / Omar Seye - Integrante / Rubem Cesar rodriguez Souza - Integrante / Eyde Cristianne Saraiva dos Santos - Coordenador.Financiador(es): Fundação de Amparo a Pesquisa do Estado do Amazonas - Bolsa.
Número de produções C, T & A: 2
2001 - 2002
Estudos das Características do Solo de Manaus para Determinação de Sistemas de Aterramento Ótimo
Descrição: O presente trabalho faz uma abordagem generalizada sobre sistemas de aterramento, tomando-se como estudos de casos, um determinado arranjo de malha de aterramento de rede de distribuição aérea de energia elétrica, da concessionária local, analisando-se os valores típicos de resistividade do solo, valores de resistência de aterramento simulados e os valores reais encontrados, após a implementação da malha. Finaliza-se com observações obtidas em campo, dos valores de resistência de aterramento do sistema de distribuição e dos valores verificados nas instalações do consumidor..
Situação: Concluído; Natureza: Desenvolvimento.
Alunos envolvidos: Graduação: (5) / Mestrado acadêmico: (3) / Doutorado: (1) .
Integrantes: Lucas Carvalho Cordeiro - Integrante / Nilton Souza Campelo - Coordenador / Fernando César Rodriguez Souza - Integrante / Aurélio Calheiros de Melo Júnior - Integrante / Elaine da Paz - Integrante / Diógenes Santos da Paz Júnior - Integrante / A.F. Aragão - Integrante / Elenildo Oliveira da Silva - Integrante.Financiador(es): Manaus Energia S.A. - Auxílio financeiro.
Número de produções C, T & A: 6


Outros Projetos


2013 - 2015
UNIBRAL 2013 - Técnicas Modernas de Desenvolvimento de Automação Industrial visando Sustentabilidade Energética e Interação Eficaz com o Usuário

Projeto certificado pelo(a) coordenador(a) Mikhail Yasha Ramalho Gadelha em 07/11/2017.
Descrição: Projeto de cooperação acadêmica entre a Universidade Federal do Amazonas e a Universität Stuttgart da Alemanha que contempla o intercâmbio de alunos de graduação.
Situação: Concluído; Natureza: Outra.
Alunos envolvidos: Graduação: (8) / Doutorado: (6) .
Integrantes: Lucas Carvalho Cordeiro - Integrante / Waldir Sabino da Silva Junior - Integrante / Cícero Ferreira Fernandes Costa Filho - Integrante / Vicente Ferreira de Lucena Júnior - Coordenador / Peter Göhner - Integrante / Nasser Jazdi - Integrante.Financiador(es): Coordenação de Aperfeiçoamento de Pessoal de Nível Superior - Auxílio financeiro.


Revisor de periódico


2008 - 2008
Periódico: IEEE Software
2010 - 2010
Periódico: LNCS Transactions on Computational Science
2011 - 2011
Periódico: The Journal of Systems and Software
2011 - 2011
Periódico: Formal Methods in System Design
2014 - 2014
Periódico: Computer Journal (Print)
2015 - 2017
Periódico: Design Automation For Embedded Systems (Dordrecht. Online)
2016 - 2016
Periódico: International Journal of Computational Science and Engineering
2016 - Atual
Periódico: Formal Aspects of Computing
2016 - Atual
Periódico: Science of Computer Programming (Print)
2016 - 2016
Periódico: Philosophical Transactions of the Royal Society of London, Series A: Mathem
2017 - 2017
Periódico: Journal of Computer Science and Technology
2017 - Atual
Periódico: ACM COMPUTING SURVEYS
2017 - Atual
Periódico: IEEE TRANSACTIONS ON RELIABILITY
2018 - Atual
Periódico: IEEE Transactions on Dependable and Secure Computing


Á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: Engenharia de Software.
2.
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 em Tempo Real.
3.
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Verificação Formal Automatizada de Sistemas de Hardware e Software.
4.
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Verificação Formal Automatizada de Sistemas de Hardware e Software/Especialidade: Procedimentos de Decisão.
5.
Grande área: Ciências Exatas e da Terra / Área: Ciência da Computação / Subárea: Sistemas Embarcados.


Idiomas


Inglês
Compreende Bem, Fala Bem, Lê Bem, Escreve Bem.
Alemão
Compreende Razoavelmente, Fala Razoavelmente, Lê Razoavelmente, Escreve Razoavelmente.


Prêmios e títulos


2018
One silver and two bronze medals in the 7th Intl. Competition on Software Verification (SV-COMP) at the 24th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'18), European Joint Conference on Theory and Practice of Software (ETAPS).
2017
One silver and one bronze medals in the 6th Intl. Competition on Software Verification (SV-COMP) at the 23rd Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'17), European Joint Conference on Theory and Practice of Software (ETAPS).
2016
One gold and one silver medals in the 5th Intl. Competition on Software Verification (SV-COMP) at the 22nd Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'16), European Joint Conference on Theory and Practice of Software (ETAPS).
2016
Bolsa de Produtividade em Pesquisa (PQ) - Nível 2, Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq).
2016
Post-Doctoral Research Fellowship, University of Oxford, UK.
2015
Two gold and two bronze medals in the 4th Intl. Competition on Software Verification (SV-COMP) at the 21st Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'15), European Joint Conference on Theory and Practice of Software (ETAPS).
2015
Best paper award in the V Brazilian Symposium on Computing Systems Engineering (SBESC): Track on Embedded Systems, Brazilian Computer Society (SBC).
2014
One gold medal in the 3rd Intl. Competition on Software Verification (SV-COMP) at the 20th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'14), European Joint Conference on Theory and Practice of Software (ETAPS).
2013
Two silver and three bronze medals in the 2nd Intl. Comp. on Software Verification (SV-COMP) at the 19th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'13), European Joint Conference on Theory and Practice of Software (ETAPS).
2012
Two gold and one bronze medals in the 1st Intl. Competition on Software Verification (SV-COMP) at the 18th Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS'12), European Joint Conference on Theory and Practice of Software (ETAPS).
2011
Distinguished paper award in the 33rd International Conference on Software Engineering (ICSE'11), ACM Special Interest Group on Software Engineering (SIGSOFT).
2008
Best paper award in the 23rd ACM Symposium on Applied Computing (SAC): Track on Real-Time Systems, ACM Special Interest Group on Applied Computing (SIGAPP).
2008
ORSAS Graduate Fellowship, Overseas Research Students Awards Scheme (ORSAS).


Produções



Produção bibliográfica
Citações

SCOPUS
Total de trabalhos:68
Total de citações:509
Cordeiro, Lucas Carvalho / http://www.scopus.com/authid/detail.url?authorId=24328704500  Data: 30/11/2017

Outras
Total de trabalhos:98
Total de citações:1128
cordeiro-lucas / http://scholar.google.com/scholar?num=100&hl=en&lr=&q=cordeiro-lucas&btnG=Search&as_subj=eng  Data: 30/11/2018

Artigos completos publicados em periódicos

1.
CHAVES, L.2018 CHAVES, L. ; BESSA, I. V. ; ISMAIL, H. I. ; FRUTUOSO, A. ; CORDEIRO, L. C. ; Lima Filho, E. B. . DSVerifier-Aided Verification Applied to Attitude Control Software in Unmanned Aerial Vehicles. IEEE TRANSACTIONS ON RELIABILITY, v. 67, p. 1420-1441, 2018.

2.
FARIAS, A. O.2018FARIAS, A. O. ; QUEIROZ, G. A. C. ; BESSA, IURY V. ; MEDEIROS, R. L. P. ; CORDEIRO, L. C. ; PALHARES, R. M. . Sim3Tanks: A Benchmark Model Simulator for Process Control and Monitoring. IEEE Access, v. 6, p. 62234-62254, 2018.

3.
Trindade, A. B.2017Trindade, A. B. ; DEGELO, R. F. ; SANTOS, E. G. ; ISMAIL, H. I. ; SILVA, H. C. ; CORDEIRO, L. C. . Multi-Core Model Checking and Maximum Satisfiability Applied to Hardware-Software Partitioning. International Journal of Embedded Systems, v. 9, p. 570-582, 2017.

4.
BESSA, IURY2017 BESSA, IURY ; ISMAIL, HUSSAMA ; PALHARES, REINALDO ; Cordeiro, Lucas ; CHAVES FILHO, JOAO EDGAR . Formal Non-Fragile Stability Verification of Digital Control Systems with Uncertainty. IEEE Transactions on Computers (Print), v. 66, p. 1-1, 2017.

5.
ALVES, E. H. S.2017ALVES, E. H. S. ; CORDEIRO, L. C. ; BATISTA FILHO, E. L. . A Method to Localize Faults in Concurrent C Programs. JOURNAL OF SYSTEMS AND SOFTWARE, v. 132, p. 336-352, 2017.

6.
MONTEIRO, FELIPE R.2017MONTEIRO, 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.

7.
LUCENA FILHO, W. C.2017LUCENA FILHO, W. C. ; CORDEIRO, L. C. ; SILVA JUNIOR, W. S. ; Carvalho, C. B. . A Power Control and Anticolision Mechanism for RFID Systems. IEEE Latin America Transactions, v. 15, p. 1933-1940, 2017.

8.
SOUSA, F. R. M.2017SOUSA, F. R. M. ; JANUARIO, F. A. P. ; CORDEIRO, L. C. ; Lima Filho, E. B. . BMCLua. SOFTWARE ENGINEERING NOTES, v. 42, p. 1-10, 2017.

9.
ARAUJO, R.2017ARAUJO, R. ; ALBUQUERQUE, H. ; BESSA, I. V. ; CORDEIRO, L. C. ; CHAVES FILHO, J. E. . Counterexample guided inductive optimization based on satisfiability modulo theories. SCIENCE OF COMPUTER PROGRAMMING, v. 151, p. 1-38, 2017.

10.
SOUSA, F. R. M.2017SOUSA, F. R. M. ; ALVES, E. H. S. ; SILVA, I. ; ISMAIL, H. I. ; CORDEIRO, L. C. ; Lima Filho, E. B. . ESBMC-GPU A Context-Bounded Model Checking Tool to Verify CUDA Programs. SCIENCE OF COMPUTER PROGRAMMING, p. 63-69, 2017.

11.
CORDEIRO, L. C.2016CORDEIRO, L. C.; Lima Filho, E. B. . SMT-Based Context-Bounded Model Checking for Embedded Systems: Challenges and Future Trends. Software Engineering Notes, v. 3, p. 1-6, 2016.

12.
BESSA, IURY V.2016BESSA, IURY V. ; ISMAIL, HUSSAMA I. ; CORDEIRO, LUCAS C. ; FILHO, JOÃO E. C. . Verification of fixed-point digital controllers using direct and delta forms realizations. Design Automation for Embedded Systems, v. 20, p. 95-126, 2016.

13.
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.

14.
PEREIRA, PHILLIPE2016PEREIRA, 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. 1-20, 2016.

15.
GADELHA, M. Y. R.2015GADELHA, M. Y. R. ; ISMAIL, H. I. ; CORDEIRO, L. C. . Handling Loops in Bounded Model Checking of C Programs via k-Induction. International Journal on Software Tools for Technology Transfer (Print), v. 19, p. 97-114, 2015.

16.
TRINDADE, ALESSANDRO B.2015TRINDADE, ALESSANDRO B. ; CORDEIRO, LUCAS C. . Applying SMT-based verification to hardware/software partitioning in embedded systems. Design Automation for Embedded Systems, v. 20, p. 1-19, 2015.

17.
MORSE, J.2014MORSE, J. ; CORDEIRO, L. C. ; NICOLE, D. ; FISCHER, BERND . Applying symbolic bounded model checking to the 2012 RERS greybox challenge. International Journal on Software Tools for Technology Transfer (Print), v. 16, p. 519-529, 2014.

18.
ROSA, R. E. V. S.2013ROSA, R. E. V. S. ; LUCENA JUNIOR, V. F. ; CORDEIRO, L. C. ; CHAVES FILHO, J. E. . Dynamic and automated product derivation for consumer electronics software applications. IEEE Transactions on Consumer Electronics, v. 59, p. 883-891, 2013.

19.
Morse, Jeremy2013Morse, Jeremy ; Cordeiro, Lucas ; Nicole, Denis ; FISCHER, BERND . Model checking LTL properties over ANSI-C programs with bounded traces. SOFTWARE AND SYSTEMS MODELING, v. 14, p. 65-81, 2013.

20.
2Freitas, M.2012Freitas, M. ; Valenzuela, V. ; Gadelha, M. ; SILVA JUNIOR, W. S. ; CORDEIRO, L. C. ; LUCENA JUNIOR, V. F. . A 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.

21.
Cordeiro, Lucas2012 Cordeiro, Lucas; FISCHER, BERND ; MARQUES-SILVA, JOAO . SMT-Based Bounded Model Checking for Embedded ANSI-C Software. IEEE Transactions on Software Engineering, v. 38, p. 957-974, 2012.

22.
3CORDEIRO, L. C.2008CORDEIRO, L. C.; MAR, C. A. A. ; VALENTIN, E. B. ; Cruz, F. T. ; PATRICK, D. O. ; BARRETO, R. S. ; LUCENA JUNIOR, V. F. . An agile development methodology applied to embedded control software under stringent hardware constraints. Software Engineering Notes, v. 33, p. 1, 2008.

23.
4CORDEIRO, L. C.2007CORDEIRO, L. C.; BARRETO, R. S. ; BARCELOS, R. F. ; OLIVEIRA, M. ; LUCENA JUNIOR, V. F. ; MACIEL, P. . TXM: an agile HW/SW development methodology for building medical devices. Software Engineering Notes, v. 32, p. 1, 2007.

24.
5CORDEIRO, L. C.2004CORDEIRO, L. C.; A.C. de Melo Junior ; D.S. Paz Jr. ; E.C. da Paz ; F.C.R Souza ; J.T.D. Alkmin ; A.F. Aragão ; N.S. Campelo . Mapas de isorresistividades elétricas aparentes do solo superficial da cidade de Manaus. Revista Brasileira de Geociências, 2004.

Capítulos de livros publicados
1.
Rocha, H. ; ISMAIL, H. I. ; CORDEIRO, L. C. ; BARRETO, R. S. . Model Checking Embedded C Software Using k-Induction and Invariants. In: Markus Winterholer; Djones Lettnin. (Org.). Embedded Software Verification and Debugging. 1ed.: Springer, 2017, v. 1, p. 159-182.

Trabalhos completos publicados em anais de congressos
1.
CHAVES, L. ; BESSA, I. V. ; CORDEIRO, L. C. ; KROENING, DANIEL . DSValidator: An Automated Counterexample Reproducibility Tool for Digital Systems. In: 21st ACM International Conference on Hybrid Systems: Computation and Control, 2018, Porto, Portugal. HSCC'18. Washington: ACM, 2018. p. 253-258.

2.
MENEZES, R. ; Rocha, H. ; CORDEIRO, L. C. ; BARRETO, R. S. . Map2Check using LLVM and KLEE. In: 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2018, Thessaloniki, Greece. TACAS'18. Heidelberg: Springer, 2018. v. 10806. p. 437-441.

3.
CORDEIRO, L. C.; KESSELI, PASCAL ; KROENING, DANIEL ; SCHRAMMEL, P. ; TRTIK, M. . JBMC: A Bounded Model Checking Tool for Verifying Java Bytecode. In: 30th International Conference on Computer Aided Verification, 2018, Oxford, UK. CAV'18. Heidelberg: Springer, 2018. v. 10981. p. 183-190.

4.
GADELHA, M. Y. R. ; SOUSA, F. R. M. ; MORSE, J. ; CORDEIRO, L. C. ; FISCHER, BERND ; NICOLE, D. . ESBMC 5.0: An Industrial-Strength C Model Checker. In: 33rd IEEE/ACM International Conference on Automated Software Engineering, 2018, Montpellier, France. ASE'18. USA: ACM, 2018. p. 888-891.

5.
GADELHA, M. Y. R. ; SOUSA, F. R. M. ; CORDEIRO, L. C. ; NICOLE, D. . Towards Counterexample-guided k-Induction for Fast Bug Detection. In: 26th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2018, Lake Buena Vista, Florida. ESEC/FSE'18, 2018. p. 1-5.

6.
ABATE, ALESSANDRO ; BESSA, IURY ; CATTARUZZA, DARIO ; Cordeiro, Lucas ; DAVID, CRISTINA ; KESSELI, PASCAL ; KROENING, DANIEL . Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants. In: the 20th International Conference, 2017, Pittsburgh. Proceedings of the 20th International Conference on Hybrid Systems: Computation and Control - HSCC '17, 2017. p. 197-206.

7.
ROCHA, W. ; Rocha, H. ; ISMAIL, H. I. ; CORDEIRO, L. C. ; FISCHER, BERND . DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs. In: 23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2017, Uppsala, Sweden. TACAS'17. Germany: Springer, 2017. v. 10206. p. 360-364.

8.
ABATE, A. ; BESSA, IURY ; CATTARUZZA, D. ; CORDEIRO, L. C. ; DAVID, C. ; KESSELI, P. ; KROENING, D. ; POLGREEN, E. . Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants. In: 29th International Conference on Computer-Aided Verification, 2017, Heidelberg. CAV'17. Germany: Springer, 2017. v. 10426. p. 462-482.

9.
CHAVES, LENNON ; BESSA, IURY ; Cordeiro, Lucas ; KROENING, DANIEL ; LIMA, EDDIE . Verifying digital systems with MATLAB. In: the 26th ACM SIGSOFT International Symposium, 2017, Santa Barbara. Proceedings of the 26th ACM SIGSOFT International Symposium on Software Testing and Analysis - ISSTA 2017. New York: ACM Press, 2017. p. 388-391.

10.
MELLO, D. ; Freitas, M. ; CORDEIRO, L. C. ; SILVA JUNIOR, W. S. ; BESSA, I. V. ; Lima Filho, E. B. ; CLAVIER, L. . Verification of Magnitude and Phase Responses in Fixed-Point Digital Filters. In: XXXV Simpósio Brasileiro de Telecomunicações e Processamento de Sinais, 2017, São Pedro, SP. SBrT'17. São Pedro, SP: Sociedade Brasileira de Telecomunicações (SBrT), 2017. p. 1184-1188.

11.
ARAUJO, R. ; RIBEIRO, A. ; BESSA, I. V. ; CORDEIRO, L. C. ; CHAVES FILHO, J. E. . Counterexample Guided Inductive Optimization Applied to Mobile Robots Path Planning. In: 14rd Latin American Robotics Symposium, 2017, Curitiba, Parana. LARS. Washington: IEEE, 2017. p. 1-8.

12.
ABATE, ALESSANDRO ; BESSA, IURY V. ; CATTARUZZA, D. ; CHAVES, L. ; CORDEIRO, L. C. ; DAVID, C. ; KESSELI, P. ; KROENING, D. ; POLGREEN, E. . DSSynth: An Automated Digital Controller Synthesis Tool for Physical Plants. In: 32nd IEEE/ACM International Conference on Automated Software Engineering, 2017, Illinois, USA. ASE'17, 2017. p. 919-924.

13.
AMOEDO, D. ; MELO, W. ; CORDEIRO, L. C. ; Lima Filho, E. B. ; SILVA JUNIOR, W. S. ; Carvalho, C. B. . Classificação Automática de Modulações Mono e Multiportadoras utilizando Método de Extração de Características e Classificadores SVM. In: XXXV Simpósio Brasileiro de Telecomunicações e Processamento de Sinais, 2017, São Pedro, SP. SBrT'17. São Pedro, SP: Sociedade Brasileira de Telecomunicações (SBrT), 2017. p. 393-397.

14.
ALBUQUERQUE, H. ; ARAUJO, R. ; Bessa, I. ; CORDEIRO, L. C. ; Lima Filho, E. B. . OptCE: A Counterexample-Guided Inductive Optimization Solver. In: XX Brazilian Symposium on Formal Methods, 2017, Recife. SBMF'17. Heidelberg: Springer, 2017. v. 10623. p. 125-141.

15.
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. Heidelberg: Springer, 2017. v. 10623. p. 91-106.

16.
CAVALCANTE, T. R. F. ; BESSA, I. V. ; CORDEIRO, L. C. . Planning and Evaluation of UAV Mission Planner for Intralogistics Problems. In: VII Brazilian Symposium on Computing Systems Engineering, 2017, Curitiba, Paraná. SBESC'17, 2017. p. 9-16.

17.
PEREIRA, PHILLIPE ; ALBUQUERQUE, HIGO ; MARQUES, HENDRIO ; SILVA, ISABELA ; CARVALHO, CELSO ; Cordeiro, Lucas ; SANTOS, VANESSA ; FERREIRA, RICARDO . Verifying CUDA programs using SMT-based context-bounded model checking. In: the 31st Annual ACM Symposium, 2016, Pisa. Proceedings of the 31st Annual ACM Symposium on Applied Computing - SAC '16. New York: ACM Press. p. 1648-1653.

18.
Rocha, H. ; CORDEIRO, L. C. ; BARRETO, R. S. . Hunting Memory Bugs in C Programs with Map2Check (Competition Contribution). In: 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2016, Eindhoven, The Netherlands. TACAS, 2016. v. 9636. p. 934-937.

19.
GARCIA, M. A. P. ; SOUSA, F. R. M. ; CORDEIRO, L. C. ; Lima Filho, E. B. . ESBMCQtOM: A Bounded Model Checking Tool to Verify Qt Applications. In: 23rd International SPIN symposium on Model Checking of Software, 2016, Eindhoven, Netherlands. SPIN, 2016. v. 9641. p. 97-103.

20.
Pereira, P. A. ; SOUSA, F. R. M. ; CORDEIRO, L. C. ; Costa Filho, C. F. F. ; Costa, M. G. F. . Complementary Training Programme for Electrical and Computer Engineering Students Through an Industrial-Academic Collaboration. In: 46th Annual Frontiers in Education (FIE) Conference, 2016, Erie. FIE, 2016. p. 1-9.

21.
ARAUJO, RODRIGO ; BESSA, IURY ; Cordeiro, Lucas Carvalho ; FILHO, JOAO EDGAR CHAVES . SMT-based Verification Applied to Non-convex Optimization Problems. In: 2016 VI Brazilian Symposium on Computing Systems Engineering (SBESC), 2016, João Pessoa. 2016 VI Brazilian Symposium on Computing Systems Engineering (SBESC). p. 1-8.

22.
SOUZA, A. S. ; JANUARIO, F. A. P. ; CORDEIRO, L. C. . Verificação de Programas Multi-Threads Baseados no Framework Multiplataforma Qt. In: IV Encontro Regional de Engenharia, 2016, Manaus, Brasil. ENCOENG'16, 2016. p. 131-140.

23.
OLIVEIRA, RODRIGO R. ; CORDEIRO, LUCAS C. ; DE LUCENA, VICENTE F. . Hardware reconfiguration based on broadcasted digital TV signal. In: 2015 IEEE International Conference on Consumer Electronics (ICCE), 2015, Las Vegas. 2015 IEEE International Conference on Consumer Electronics (ICCE). p. 596-626.

24.
Rocha, H. ; BARRETO, R. S. ; CORDEIRO, L. C. . Memory Management Test-Case Generation of C Programs using Bounded Model Checking. In: 13th International Conference on Software Engineering and Formal Methods, 2015, York, UK. SEFM, 2015. v. 9276. p. 251-267.

25.
ISMAIL, H. I. ; BESSA, I. V. ; CORDEIRO, L. C. ; CHAVES FILHO, J. E. ; Lima Filho, E. B. . DSVerifier: A Bounded Model Checking Tool for Digital Systems. In: 22nd International SPIN Symposium on Model Checking of Software, 2015, Stellenbosch, South Africa. SPIN 2015, 2015. v. 9232. p. 126-131.

26.
Rodrigues, F. ; CORDEIRO, L. C. ; Lima Filho, E. B. . Verificação de Programas C++ Baseados no Framework Multiplataforma Qt. In: IV Encontro Regional de Computação e Sistemas de Informação, 2015, Manaus, Brasil. ENCOSIS, 2015. p. 181-190.

27.
LIMA, M. S. ; SILVA, E. S. ; CORDEIRO, L. C. . Verificação de Modelos Aplicada aos Filtros Espaciais em Processamento Digital de Imagens. In: IV Encontro Regional de Computação e Sistemas de Informação, 2015, Manaus, Brasil. ENCOSIS, 2015. p. 136-145.

28.
Rodrigues, F. ; CORDEIRO, L. C. ; Lima Filho, E. B. . Bounded Model Checking of C++ Programs Based on the Qt Framework. In: 2015 IEEE 4th Global Conference on Consumer Electronics, 2015, Osaka, Japan. GCCE, 2015. p. 179-180.

29.
TRINDADE, ALESSANDRO ; ISMAIL, HUSSAMA ; Cordeiro, Lucas . Applying Multi-core Model Checking to Hardware-Software Partitioning in Embedded Systems. In: 2015 Brazilian Symposium on Computing Systems Engineering (SBESC), 2015, Foz do Iguacu. 2015 Brazilian Symposium on Computing Systems Engineering (SBESC). p. 102-105.

30.
ALVES, ERICKSON H. DA S. ; CORDEIRO, LUCAS C. ; FILHO, EDDIE B. DE LIMA . Fault Localization in Multi-threaded C Programs Using Bounded Model Checking. In: 2015 Brazilian Symposium on Computing Systems Engineering (SBESC), 2015, Foz do Iguacu. 2015 Brazilian Symposium on Computing Systems Engineering (SBESC). p. 96-101.

31.
ROCHA, HERBERT ; ISMAIL, HUSSAMA ; Cordeiro, Lucas ; BARRETO, RAIMUNDO . Model Checking Embedded C Software Using k-Induction and Invariants. In: 2015 Brazilian Symposium on Computing Systems Engineering (SBESC), 2015, Foz do Iguacu. 2015 Brazilian Symposium on Computing Systems Engineering (SBESC). p. 90-95.

32.
Pereira, P. A. ; ALBUQUERQUE, H. ; MARQUES, H. ; SILVA, I. ; SANTOS, V. ; Carvalho, C. B. ; FERREIRA, R. S. ; CORDEIRO, L. C. . Verificação de Kernels em Programas CUDA usando Bounded Model Checking. In: XV Simpósio de Sistemas Computacionais de Alto Desempenho, 2015, Florianópolis/SC. WSCAD-SSC, 2015. p. 24-35.

33.
MORSE, J. ; RAMALHO, M. ; CORDEIRO, L. C. ; NICOLE, D. ; FISCHER, BERND . ESBMC v1.22 (Competition Contribution). In: 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2014, Grenoble, França. TACAS'14, 2014. v. 8413. p. 405-407.

34.
BESSA, I. V. ; Abreu, R. B. ; CORDEIRO, L. C. ; FILHO, JOAO EDGAR CHAVES . SMT-based bounded model checking of fixed-point digital controllers. In: 40th Annual Conference of the IEEE Industrial Electronics Society, 2014, Dallas, USA. IECON'14, 2014. p. 295-301.

35.
ROSA, RICARDO E. V. DE S. ; CORDEIRO, LUCAS C. ; LUCENA JUNIOR, VICENTE F. DE . A secondary screen architecture to accurately capture viewers' interactions in an iTV environment. In: 2014 IEEE 3rd Global Conference on Consumer Electronics (GCCE), 2014, Tokyo. 2014 IEEE 3rd Global Conference on Consumer Electronics (GCCE). p. 264-265.

36.
JANUARIO, FRANCISCO A. P. ; CORDEIRO, LUCAS C. ; LUCENA, VICENTE F. DE ; LIMA FILHO, EDDIE B. DE . BMCLua: Verification of Lua programs in digital TV interactive applications. In: 2014 IEEE 3rd Global Conference on Consumer Electronics (GCCE), 2014, Tokyo. 2014 IEEE 3rd Global Conference on Consumer Electronics (GCCE). p. 707-708.

37.
Trindade, A. B. ; CORDEIRO, L. C. . Aplicando Verificação de Modelos para o Particionamento de Hardware/Software. In: IV Simpósio Brasileiro de Engenharia de Sistemas Computacionais, 2014, Manaus, Brasil. SBESC'14, 2014. p. 1-6.

38.
JANUARIO, F. A. P. ; CORDEIRO, L. C. ; Lima Filho, E. B. ; LUCENA JUNIOR, V. F. . BMCLua: Verificação de Programas Lua em Aplicações Interativas de TV Digital. In: IV Simpósio Brasileiro de Engenharia de Sistemas Computacionais, 2014, Manaus, Brasil. SBESC'14, 2014. p. 1-6.

39.
BESSA, IURY VALENTE DE ; ISMAIL, HUSSAMA IBRAHIM ; Cordeiro, Lucas Carvalho ; FILHO, JOAO EDGAR CHAVES . Verification of Delta Form Realization in Fixed-Point Digital Controllers Using Bounded Model Checking. In: 2014 Brazilian Symposium on Computing Systems Engineering (SBESC), 2014, Manaus. 2014 Brazilian Symposium on Computing Systems Engineering. p. 49-54.

40.
MORSE, J. ; CORDEIRO, L. C. ; NICOLE, D. ; FISCHER, BERND . Handling Unbounded Loops with ESBMC 1.20 (Competition Contribution). In: 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2013, Rome, Italy. TACAS'13, 2013. v. 7795. p. 619-622.

41.
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-156.

42.
JANUARIO, F. A. P. ; CORDEIRO, L. C. ; Lima Filho, E. B. . Verificação de Códigos Lua Utilizando BMCLua. In: XXXI Simpósio Brasileiro de Telecomunicações, 2013, Fortaleza. SBrT'13, 2013. p. 1-5.

43.
Abreu, R. B. ; CORDEIRO, L. C. ; Lima Filho, E. B. . Verifying Fixed-Point Digital Filters using SMT-Based Bounded Model Checking. In: XXXI Simpósio Brasileiro de Telecomunicações, 2013, Fortaleza. SBrT'13, 2013. p. 1-5.

44.
Freitas, M. ; GADELHA, M. Y. R. ; CORDEIRO, L. C. ; SILVA JUNIOR, W. S. ; Lima Filho, E. B. . 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. p. 1-5.

45.
GADELHA, M. Y. R. ; CORDEIRO, L. C. ; Cavalcante, A. L. D. ; LUCENA JUNIOR, V. F. . 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. p. 1-6.

46.
da Silva, V. J. ; CORDEIRO, L. C. ; LUCENA JUNIOR, V. F. . Verificação de Aplicações AmI Usando Java PathFinder. In: III Simpósio Brasileiro de Engenharia de Sistemas Computacionais, 2013, Niterói/RJ. SBESC'13, 2013. p. 1-6.

47.
COHEN, DAVID ; VALENTIN, EDUARDO ; Barreto, R. S. ; OLIVEIRA, HORACIO ; Cordeiro, Lucas . A car racing based strategy for the Dynamic Voltage and Frequency Scaling technique. In: 2012 IEEE 21st International Symposium on Industrial Electronics (ISIE), 2012, Hangzhou. 2012 IEEE International Symposium on Industrial Electronics. p. 774-779.

48.
Rocha, H. ; BARRETO, R. S. ; CORDEIRO, L. C. ; Dias-Neto, A. C. . Understanding Programming Bugs in ANSI-C Software Using Bounded Model Checking Counter-Examples. In: 9th International Conference on Integrated Formal Methods, 2012, Pisa, Italy. iFM'12, 2012. v. 7321. p. 128-142.

49.
CORDEIRO, L. C.; Morse, Jeremy ; Nicole, Denis ; FISCHER, BERND . Context-Bounded Model Checking with ESBMC 1.17 (Competition Contribution). In: 18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, 2012, Rome, Italy. TACAS'12, 2012. v. 7214. p. 534-537.

50.
Lima, F. S. ; CORDEIRO, L. C. ; Souza, R. C. R. . Sistema de Monitoramento a Distância para Unidade de Célula a Combustível. In: VIII Congresso Brasileiro de Planejamento Energético, 2012, Curitiba. SBPE'12, 2012.

51.
Cordeiro, Lucas; FISCHER, BERND . Verifying multi-threaded software using smt-based context-bounded model checking. In: Proceeding of the 33rd international conference, 2011, Waikiki. Proceeding of the 33rd international conference on Software engineering - ICSE '11. New York: ACM Press. p. 331-340.

52.
MORSE, J. ; CORDEIRO, L. C. ; NICOLE, D. ; FISCHER, BERND . Context-Bounded Model Checking of LTL Properties for ANSI-C Software. In: 9th International Conference on Software Engineering and Formal Methods, 2011, Montevideo, Uruguay. SEFM'11, 2011. p. 302-317.

53.
DE LUCENA, VICENTE FERREIRA ; DE QUEIROZ NETO, JOSE PINHEIRO ; FILHO, JOAO EDGAR CHAVES ; DA SILVA, WALDIR SABINO ; Cordeiro, Lucas Carvalho . Gift young engineers: An extra-curricular initiative for updating computer and electrical engineering courses. In: 2011 Frontiers in Education Conference (FIE), 2011, Rapid City. 2011 Frontiers in Education Conference (FIE). p. 1-6.

54.
Barreto, R. S. ; Cordeiro, Lucas ; FISCHER, BERND . Verifying Embedded C Software with Timing Constraints Using an Untimed Bounded Model Checker. In: 2011 Brazilian Symposium on Computing System Engineering (SBESC), 2011, Florianopolis. 2011 Brazilian Symposium on Computing System Engineering. p. 89-100.

55.
CALDAS, R. B. ; BARRETO, R. S. ; CORDEIRO, L. C. ; Campos, S. . A Formal Method for Modeling, Verification and Synthesis of Embedded Reactive Systems. In: IADIS International Conference APPLIED COMPUTING 2011, 2011, Rio de Janeiro, Brazil. AC'11, 2011. p. 379-386.

56.
CORDEIRO, L. C.; FISCHER, BERND ; MARQUES-SILVA, J. P. . Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking. In: 17th IEEE International Conference and Workshops on Engineering of Computer-Based Systems, 2010, Oxford. ECBS'10, 2010. p. 160-169.

57.
Cordeiro, Lucas. SMT-based bounded model checking for multi-threaded software in embedded systems. In: the 32nd ACM/IEEE International Conference, 2010, Cape Town. Proceedings of the 32nd ACM/IEEE International Conference on Software Engineering - ICSE '10. New York: ACM Press. v. 2. p. 373-376.

58.
CORDEIRO, L. C.; FISCHER, BERND . Bounded Model Checking of Multi-threaded Software using SMT solvers. In: 8th International Workshop on Satisfiability Modulo Theories, 2010, Edinburgh. SMT'10, 2010.

59.
Rocha, H. ; CORDEIRO, L. C. ; BARRETO, R. S. ; Netto, José . Exploiting Safety Properties in Bounded Model Checking for Test Cases Generation of C Programs. In: 4th Brazilian Workshop on Systematic and Automated Software Testing, 2010, Natal. SAST'10, 2010. p. 121-130.

60.
Cordeiro, Lucas; FISCHER, BERND ; CHEN, HUAN ; MARQUES-SILVA, JOAO . Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints, 2009. p. 396-403.

61.
Cordeiro, Lucas; FISCHER, BERND ; MARQUES-SILVA, JOAO . SMT-Based Bounded Model Checking for Embedded ANSI-C Software. In: 2009 24th IEEE/ACM International Conference on Automated Software Engineering (ASE), 2009, Auckland. 2009 IEEE/ACM International Conference on Automated Software Engineering. p. 137-148.

62.
CRUZ, FABIANO ; Barreto, R. S. ; Cordeiro, Lucas . Towards a model-driven engineering approach for developing embedded hard real-time software. In: the 2008 ACM symposium, 2008, Fortaleza. Proceedings of the 2008 ACM symposium on Applied computing - SAC '08. New York: ACM Press. p. 308-314.

63.
TEOFILO, MAURO ; Cordeiro, Lucas ; Barreto, R. S. ; PEREIRA, JOSE RAIMUNDO ; MARDEM, AYRES ; FREITAS, PEDRO . Mandos: A User Interaction Method in Embedded Applications for Mobile Telephony. In: , 2008, Sainte Luce. . p. 271-276.

64.
CRUZ, FABIANO ; Barreto, R. S. ; Cordeiro, Lucas ; MACIEL, PAULO . ezRealtime: A Domain-Specific Modeling Tool for Embedded Hard Real-Time Software Synthesis. In: 2008 Design, Automation and Test in Europe, 2008, Munich. 2008 Design, Automation and Test in Europe. p. 1510-1515.

65.
Cordeiro, Lucas; MAR, CARLOS ; VALENTIN, EDUARDO ; CRUZ, FABIANO ; PATRICK, DANIEL ; Barreto, R. S. ; LUCENA, VICENTE . A Platform-Based Software Design Methodology for Embedded Control Systems: An Agile Toolkit. In: 2008 15th Annual IEEE International Conference on Engineering of Computer Based Systems (ECBS), 2008, Belfast. 15th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ecbs 2008). p. 408-417.

66.
CORDEIRO, L. C.; BARRETO, R. S. ; OLIVEIRA, M. . Towards a Semiformal Development Methodology for Embedded Systems. In: 3rd Intenational Conference on Evaluation of Novel Approaches to Software Engineering, 2008, Funchal, Madeira ? Portugal. ENASE'2008. Funchal, Madeira, Portugal: Institute for Systems and Technologies of Information, Control and Communication, 2008. p. 5-12.

67.
Cordeiro, Lucas; Barreto, R. S. ; BARCELOS, RAFAEL ; OLIVEIRA, MEUSE ; LUCENA, VICENTE ; MACIEL, PAULO . Agile Development Methodology for Embedded Systems: A Platform-Based Design Approach. In: 14th Annual IEEE International Conference and Workshops on the Engineering of ComputerBased Systems (ECBS'07), 2007, Tucson. 14th Annual IEEE International Conference and Workshops on the Engineering of Computer-Based Systems (ECBS'07). p. 195-202.

68.
CORDEIRO, L. C.; Becker, C. O. ; BARRETO, R. S. . Applying Scrum and Organizational Patterns to Multi Site Software Development. In: 6th Latin American Conference on Pattern Languages of Programming, 2007, Porto de Galinhas, Brazil. SugarLoafPlop'07, 2007. p. 46-67.

69.
CORDEIRO, L. C.; Louzado, D. A. . Aplicando Padrões de Gerência de Configuração de Software em Projetos Geograficamente Distribuídos. In: 5º Conferência Latino-Americana em Linguagem de Padrões para Programação, 2005, Campos do Jordão. Pattern Applications, 2005. p. 207-221.

70.
J.T.D. Alkmin ; A.C. de Melo Junior ; E.C. da Paz ; N.S. Campelo ; F.C.R Souza ; CORDEIRO, L. C. ; CARVALHO, J. S. ; A.F. Aragão . Comparação entre mapas de isorresistividades elétricas aparentes do solo superficial de Manaus, a partir de séries de dados completos e estatísticos. In: I Simpósio Regional da Sociedade Brasileira de Geofísica, 2004, São Paulo. SBGf, 2004.

71.
J.T.D. Alkmin ; A.C. de Melo Junior ; F.C.R Souza ; N.S. Campelo ; CORDEIRO, L. C. ; E.C. da Paz ; A.F. Aragão . Malhas de Aterramento do Sistema Elétrico da Manaus Energia: um Estudo de Caso. In: II Congresso de Inovação Tecnológica em Energia Elétrica, 2003, Salvador. II Congresso de Inovação Tecnológica em Energia Elétrica, 2003.

Resumos publicados em anais de congressos
1.
Gadelha, M. ; MORSE, J. ; CORDEIRO, L. C. ; NICOLE, D. . Using clang as a Frontend on a Formal Verification Tool. In: European LLVM Developers Meeting, 2018, Bristol, UK. EuroLLVM. Bristol: LLVM, 2018. p. 1-1.

2.
ABATE, ALESSANDRO ; Bessa, I. ; CATTARUZZA, D. ; CORDEIRO, L. C. ; DAVID, CRISTINA ; KESSELI, P. ; KROENING, DANIEL ; POLGREEN, E. . Safe, Automated and Formal Synthesis of Digital Controllers for Continuous Plants. In: 7th Workshop on Synthesis, 2018, Oxford. SYNT'18, 2018. p. 1-1.

3.
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 (journal-first abstract). In: the 33rd ACM/IEEE International Conference, 2018, Montpellier. Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering - ASE 2018. New York: ACM Press, 2018. p. 954.

4.
N.S. Campelo ; Seye, O. ; SANTOS, E. C. S. ; AZEVEDO, C. ; GUIMARAES, E. L. ; CAJUEIRO, D. J. ; LAU, J. ; CORDEIRO, L. C. ; PINHEIRO, S. C. ; CABRAL, E. M. . Melhoramento do processo produtivo de cerâmica estrutural como ação mitigadora para estabilização ou redução adicional nas emissões de gases do efeito estufa. In: XIII Congresso de Iniciação Científica da Universidade Federal do Amazonas, 2004, Manaus. UFAM, 2004.

5.
J.T.D. Alkmin ; A.F. Aragão ; A.C. de Melo Junior ; F.C.R Souza ; CORDEIRO, L. C. ; E.C. da Paz ; D.S. Paz Jr. ; N.S. Campelo . Projeto de arranjos de aterramento ótimo, para proteção de sistemas de distribuição de energia elétrica, da concessionária Manaus Energia S.A., na cidade de Manaus. In: Encontro Nacional sobre Eficiência Energética em Pesquisa e Desenvolvimento, 2004, Florianópolis. ., 2004.

6.
CORDEIRO, L. C.; A.F. Aragão ; A.C. de Melo Junior ; D.S. Paz Jr. ; E.C. da Paz ; F.C.R Souza ; J.T.D. Alkmin ; N.S. Campelo ; SILVA, E. O. . Estudo das características do solo de Manaus para determinação de sistemas de aterramento ótimo. In: XII Congresso de Iniciação Científica da Universidade Federal do Amazonas, 2003, Manaus. UFAM, 2003.

Artigos aceitos para publicação
1.
CORDEIRO, L. C.; KROENING, DANIEL ; SCHRAMMEL, P. . Benchmarking of Java Verification Tools at the Software Verification Competition (SV-COMP). SOFTWARE ENGINEERING NOTES, 2018.

Apresentações de Trabalho
1.
CHAVES, L. ; Bessa, I. ; CORDEIRO, L. C. ; KROENING, D. ; Lima Filho, E. B. . Verifying digital systems with MATLAB. 2017. (Apresentação de Trabalho/Simpósio).

2.
ABATE, ALESSANDRO ; BESSA, IURY ; CATTARUZZA, D. ; CORDEIRO, L. C. ; DAVID, C. ; KESSELI, P. ; KROENING, DANIEL ; POLGREEN, E. . DSSynth: An Automated Digital Controller Synthesis Tool for Physical Plants. 2017. (Apresentação de Trabalho/Congresso).

3.
CORDEIRO, L. C.. Software Model Checking in Embedded Systems. 2016. (Apresentação de Trabalho/Outra).

4.
CORDEIRO, L. C.. Verifying CUDA Programs using SMT-Based Context-Bounded Model Checking. 2016. (Apresentação de Trabalho/Congresso).

5.
ISMAIL, H. I. ; Bessa, I. ; CORDEIRO, L. C. ; Lima Filho, E. B. ; CHAVES FILHO, J. E. . DSVerifier: A Bounded Model Checking Tool for Digital Systems. 2015. (Apresentação de Trabalho/Simpósio).

6.
MORSE, J. ; Gadelha, M. ; CORDEIRO, L. C. ; NICOLE, D. . ESBMC 1.22 (Competition Contribution). 2014. (Apresentação de Trabalho/Conferência ou palestra).

7.
JANUARIO, F. A. P. ; CORDEIRO, L. C. ; Lima Filho, E. B. ; LUCENA JUNIOR, V. F. . BMCLua: Verification of Lua Programs in Digital TV Interactive Applications. 2014. (Apresentação de Trabalho/Congresso).

8.
MORSE, J. ; CORDEIRO, L. C. ; NICOLE, D. . Handling Unbounded Loops with ESBMC 1.20. 2013. (Apresentação de Trabalho/Conferência ou palestra).

9.
CORDEIRO, L. C.. Model Checking Embedded Systems. 2013. (Apresentação de Trabalho/Seminário).

10.
CORDEIRO, L. C.; MORSE, J. ; NICOLE, D. . Context-Bounded Model Checking with ESBMC 1.17. 2012. (Apresentação de Trabalho/Conferência ou palestra).

11.
CORDEIRO, L. C.. Verifying Multi-threaded Software using SMT-based Context-Bounded Model Checking. 2011. (Apresentação de Trabalho/Conferência ou palestra).

12.
CORDEIRO, L. C.; MARQUES-SILVA, J. P. . Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking. 2010. (Apresentação de Trabalho/Conferência ou palestra).

13.
CORDEIRO, L. C.. Bounded Model Checking of Multi-threaded Software using SMT solvers. 2010. (Apresentação de Trabalho/Seminário).

14.
CORDEIRO, L. C.. SMT-Based Bounded Model Checking for Multi-threaded Software in Embedded Systems. 2010. (Apresentação de Trabalho/Simpósio).

15.
CORDEIRO, L. C.; MARQUES-SILVA, J. P. . SMT-Based Bounded Model Checking for Embedded ANSI-C Software. 2010. (Apresentação de Trabalho/Seminário).

16.
CORDEIRO, L. C.; CHEN, H. ; MARQUES-SILVA, J. P. . Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints. 2009. (Apresentação de Trabalho/Conferência ou palestra).

17.
CORDEIRO, L. C.. Uma Metodologia de Desenvolvimento de HW/SW Ágil para Sistemas Embarcados. 2007. (Apresentação de Trabalho/Conferência ou palestra).

18.
CORDEIRO, L. C.. Metodologia de Desenvolvimento Ágil Scrum: O Caso XMPM. 2006. (Apresentação de Trabalho/Conferência ou palestra).

19.
CORDEIRO, L. C.; Louzado, D. A. . Aplicando Padrões de Gerência de Configuração de Software em Projetos Geograficamente Distribuídos. 2005. (Apresentação de Trabalho/Conferência ou palestra).


Produção técnica
Programas de computador sem registro
1.
CORDEIRO, L. C.; MARQUES-SILVA, J. P. . Efficient SMT-Based Bounded Model Checker (ESBMC). 2009.

2.
CORDEIRO, L. C.; SOUSA, C. A. G. ; NING, C. H. ; Becker, C. O. ; Louzado, D. A. ; Zimmermann, E. E. ; HIGA, F. S. ; CARVALHO, J. R. H. ; BAZZO, J. J. ; TOMASELLI, M. . linuX Mobile Phone Manager. 2005.

3.
CORDEIRO, L. C.. Sistema de Aquisição de Dados Baseado em PC de um Gasogênio à Carvão Vegetal. 2004.

4.
CORDEIRO, L. C.; Seye, O. ; N.S. Campelo ; Souza, R. C. R. . Software para gerenciamento de documentação de projetos. 2003.

5.
CORDEIRO, L. C.; Albuquerque, A. T. ; Guedes, R. A. M. . Projeto Substituição de Lâmpadas no Setor Residencial. 2002.

6.
CORDEIRO, L. C.; J.T.D. Alkmin ; Souza, R. C. R. . Software para Cálculo de Demanda Contratada Ótima na Indústria. 2002.

Produtos tecnológicos
1.
CORDEIRO, L. C.; de Araújo Jr., J.T ; Oliveira, D. P. . Real-Time Programming with ADA95. 2003.

2.
CORDEIRO, L. C.. Placa de aquisição de sinais para controle de processos industriais. 2002.

Processos ou técnicas
1.
CORDEIRO, L. C.; Louzado, D. A. . Bug Tracking Process for XMPM Project. 2005.

2.
CORDEIRO, L. C.; Zimmermann, E. E. ; Louzado, D. A. . Architecture Improvement Process for XMPM Project. 2005.

3.
CORDEIRO, L. C.; Becker, C. O. ; Louzado, D. A. . SCM/BM Activities Guidelines for XMPM Project. 2005.

Trabalhos técnicos
1.
CORDEIRO, L. C.. Sub-revisor de artigos - XXII Congresso Brasileiro de Automática. 2018.

2.
CORDEIRO, L. C.. Revisor de artigos - VIII Workshop de Teses e Dissertações do CBSoft (WTDSoft 2018). 2018.

3.
CORDEIRO, L. C.. Revisor de artigos - 8th Latin-American Symposium on Dependable Computing (LADC). 2018.

4.
CORDEIRO, L. C.. Sub-revisor de artigos - 12th International Symposium on Empirical Software Engineering and Measurement. 2018.

5.
CORDEIRO, L. C.. Revisor de artigos - 34th ACM/SIGAPP Symposium on Applied Computing. 2018.

6.
CORDEIRO, L. C.. Revisor de artigos - VIII Brazilian Symposium on Computing Systems Engineering. 2018.

7.
CORDEIRO, L. C.. Revisor de artigos - 6th Intl. Competition on Software Verification (SVCOMP) held at TACAS 2017. 2017.

8.
CORDEIRO, L. C.. Revisor de artigos - 24th International SPIN Symposium on Model Checking of Software. 2017.

9.
CORDEIRO, L. C.. Revisor de artigos - 10th International Workshop on Numerical Software Verification. 2017.

10.
CORDEIRO, L. C.. Revisor de artigos - VII Workshop de Teses e Dissertações do CBSoft (WTDSoft 2017). 2017.

11.
CORDEIRO, L. C.. Revisor de artigos - 38th International Conference on Software Engineering (ICSE). 2016.

12.
CORDEIRO, L. C.. Revisor de artigos - 5th Intl. Competition on Software Verification (SVCOMP) held at TACAS 2016. 2016.

13.
CORDEIRO, L. C.. Revisor de artigos - International Conference on Management Engineering, Software Engineering and Service Sciences. 2016.

14.
CORDEIRO, L. C.; BECKER, L. B. ; MUELLER, I. ; GODOY, F. . Comitê julgador da IV Competição Intel de Sistemas Embarcados. 2016.

15.
CORDEIRO, L. C.. Revisor de artigos - VI Brazilian Symposium on Computing Systems Engineering. 2016.

16.
CORDEIRO, L. C.. Revisor de artigos - 22nd International SPIN Workshop on Model Checking of Software (SPIN). 2015.

17.
CORDEIRO, L. C.. Sub-revisor de artigos - XXXIII Simpósio Brasileiro de Telecomunicações (SBrT). 2015.

18.
CORDEIRO, L. C.. Sub-revisor de artigos - XII Simpósio Brasileiro de Automação Inteligente (SBAI). 2015.

19.
CORDEIRO, L. C.. Sub-revisor de artigos - 30th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2015.

20.
NACIF, J. A. ; MATTOS, J. C. B. ; CORDEIRO, L. C. . Comitê julgador da III Competição Intel de Sistemas Embarcados. 2015.

21.
CORDEIRO, L. C.. Revisor de artigos - 3rd Intl. Competition on Software Verification (SVCOMP) held at TACAS 2014. 2014.

22.
CORDEIRO, L. C.. Sub-revisor de artigos - 26th International Conference on Computer Aided Verification (CAV). 2014.

23.
CORDEIRO, L. C.. Revisor de artigos - 2nd Intl. Competition on Software Verification (SVCOMP) held at TACAS 2013. 2013.

24.
CORDEIRO, L. C.. Sub-revisor de artigos - 28th IEEE/ACM International Conference on Automated Software Engineering (ASE). 2013.

25.
CORDEIRO, L. C.. Sub-revisor de artigos - 40th IEEE International Symposium on Multiple-Valued Logic. 2010.

26.
CORDEIRO, L. C.. Developing Real Time Applications with LEGO Mindstorms. 2003.


Demais tipos de produção técnica
1.
CORDEIRO, L. C.. Programação C++. 2008. .

2.
CORDEIRO, L. C.. Introdução à Ciência da Computação. 2007. (Curso de curta duração ministrado/Outra).

3.
CORDEIRO, L. C.. Aquisição de Dados de Processo de um Gasogênio à Carvão Vegetal para Geração de Energia Elétrica. 2004. (Relatório de pesquisa).

4.
CORDEIRO, L. C.; Pessoa Jr., J. X. . Controle de Posição de Esteira sem uso de Sensor beaseado em Processador Digital de Sinais. 2004. (Relatório de pesquisa).

5.
CORDEIRO, L. C.; de Araújo Jr., J.T . Development of a Bluetooth-based communication and control infrastructure for LEGO Robots. 2003. (Relatório de pesquisa).

6.
CORDEIRO, L. C.; A.C. de Melo Junior ; D.S. Paz Jr. ; E.C. da Paz ; F.C.R Souza ; J.T.D. Alkmin ; N.S. Campelo ; A.F. Aragão . Estudo das características do solo de Manaus para determinação de sistemas de aterramento ótimo. 2002. (Relatório de pesquisa).

7.
CORDEIRO, L. C.; Maduro, F.R . Redução de custo e gerenciamento de energia na Universidade do Amazonas. 2001. (Relatório de pesquisa).

Demais trabalhos
1.
CORDEIRO, L. C.. Projeto e implementação de um software de controle para limpador de pára-brisa baseado no uC 8051. 2004 (Resumo) .

2.
CORDEIRO, L. C.; Oliveira, D. P. ; de Araújo Jr., J.T . Programming a Siemens S7 PLC - Conveyor (Production Movement). 2003.

3.
CORDEIRO, L. C.. Interface de Aquisição e Controle de Dados Padrão ISA. 2002 (Resumo) .



Bancas



Participação em bancas de trabalhos de conclusão
Mestrado
1.
Dias-Neto, A. C.; CORDEIRO, L. C.; VINCENZI, A. M. R.. Participação em banca de Jonathas Silva dos Santos. Insumos para a Utilização do Critério de Teste Baseado em Erros Aplicações Móveis. 2016. Dissertação (Mestrado em Informática) - Universidade Federal do Amazonas.

2.
AMORIM, M. B.; CORDEIRO, L. C.; TEIXEIRA, L. M.. Participação em banca de Paulo de Barros e Silva Filho. Static Analysis of Implicit Control Flow: Resolving Java Reflection and Android Intents. 2016. Dissertação (Mestrado em Ciências da Computação) - Universidade Federal de Pernambuco.

3.
Lettnin, D. V.; CORDEIRO, L. C.; SILVA, K. R. G.; MORAES, R.. Participação em banca de Rogério Paludo. Metodologia para Verificação Funcional Antecipada de Software Embarcado Combinando Plataformas Virtuais e Verificação Formal. 2016. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal de Santa Catarina.

4.
Cavalcante, A. L. D.; Netto, J. F. M.; CORDEIRO, L. C.. Participação em banca de Hiram Carlos Costa Amaral. Sistema Inteligente Ágil de Processo Evolutivo-SIAPE: Um Protótipo Brasileiro de Sistemas EPS. 2016. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas.

5.
CORDEIRO, L. C.; Pena, P. N.; Costa Filho, C. F. F.. Participação em banca de Alessandro Bezerra Trindade. Aplicando Verificação Formal Baseada nas Teorias do Módulo da Satisfabilidade para o Particionamento de Hardware/Software em Sistemas Embarcados. 2015. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas.

6.
CORDEIRO, L. C.; Dias-Neto, A. C.; SILVA JUNIOR, W. S.. Participação em banca de Francisco de Assis Pereira Januário. BMCLua: Metodologia para Verificação de Códigos Lua Utilizando Bounded Model Checking. 2015. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas.

7.
Barreto, R. S.; CORDEIRO, L. C.; Matias Junior, R.. Participação em banca de Rawlinson da Silva Gonçales. Integração de Características Preemptivas à Técnica Escala Dinâmica de Voltagem e Frequência Intra-Tarefa. 2015. Dissertação (Mestrado em Informática) - Universidade Federal do Amazonas.

8.
Costa Filho, C. F. F.; Netto, J. F. M.; CORDEIRO, L. C.. Participação em banca de Endrews Sznyder Souza da Silva. Proposta de um Agente para o Jogo de Dominó de 4 Pontas Utilizando o Algoritmo EXPECTMINMAX. 2015. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas.

9.
Barreto, R. S.; FROHLICH, A. A.; CORDEIRO, L. C.. Participação em banca de Diego Quintana Pinheiro. Inserção de Código DVFS-Aware em Sistemas de Tempo Real Críticos. 2015. Dissertação (Mestrado em Informática) - Universidade Federal do Amazonas.

10.
DANGELO, M. F. S. V.; Lima Filho, E. B.; CORDEIRO, L. C.. Participação em banca de Hussama Ibrahim Ismail. Verificação de Modelos Aplicada ao Projeto de Controladores Digitais Implementados em Processadores de Ponto-Fixo. 2015. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas.

11.
CORDEIRO, L. C.; da Silva, E. A. B.; Lima Filho, E. B.. Participação em banca de Renato Barbosa Abreu. Avaliação de Projetos de Filtros Digitais de Ponto-Fixo usando Teorias do Módulo da Satisfatibilidade. 2014. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas.

12.
SILVA JUNIOR, W. S.; Cordeiro, Lucas Carvalho; dos Santos, E. M.. Participação em banca de Kenny Vinente dos Santos. Detecção de Pontos Fiduciais Faciais Utilizando Filtragem Discriminativa com Análise de Componentes Principais e Alinhamento Adaptativo. 2014. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas.

13.
LUCENA JUNIOR, V. F.; BARRETO, R. S.; CORDEIRO, L. C.. Participação em banca de Victor Enrique Lauria Valenzuela. Arquitetura de Software Modular para Diagnóstico de Falhas e Monitoramento Remoto em Sistemas de Automação Industrial. 2013. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas.

14.
CORDEIRO, L. C.; BARRETO, R. S.; LUCENA JUNIOR, V. F.. Participação em banca de Mikhail Yasha Ramalho Gadelha. Verificação Baseada em Indução Matemática para Programas C++. 2013. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas.

15.
Lima Filho, E. B.; SILVA JUNIOR, W. S.; Carvalho, C. B.; CORDEIRO, L. C.. Participação em banca de Heitor Judiss Savino. Correção de PCR em Processadores de Fluxos de Transporte MPEG-2. 2012. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas.

Teses de doutorado
1.
BARRETO, R. S.; CARVALHO, J. R. H.; CORDEIRO, L. C.; AZEVEDO, C. R. B.; OLIVEIRA, R. S.; RODRIGUES, R. F.. Participação em banca de Eduardo Bezerra Valentin. Scheduling Hard Real-Time Tasks in Heterogeneous Multiprocessor Platforms subject to Energy and Temperature Constraints. 2017. Tese (Doutorado em Informática) - Universidade Federal do Amazonas.

2.
BARRETO, R. S.; CORDEIRO, L. C.; Dias-Neto, A. C.; Lettnin, D. V.; BECKER, L. B.. Participação em banca de Herbert Oliveira Rocha. Verificação de Sistemas de Software baseada em Transformações de Código usando Bounded Model Checking. 2015. Tese (Doutorado em Informática) - Universidade Federal do Amazonas.

3.
Maia, C. A.; LUCENA JUNIOR, V. F.; Martins, F. V. C.; CORDEIRO, L. C.; Pena, P. N.; Pereira, G. A. S.. Participação em banca de José Ricardo da Silva Dias. Métodos de Controle de Fluxo de Entrada para Sistemas Modelados por Grafos de Eventos Temporizados. 2014. Tese (Doutorado em Engenharia Elétrica) - Universidade Federal de Minas Gerais.

Qualificações de Doutorado
1.
BARRETO, R. S.; Lettnin, D. V.; CORDEIRO, L. C.. Participação em banca de Herbert Oliveira Rocha. Aperfeiçoamento da Verificação de Sistemas de Software usando Bounded Model Checker. 2013. Exame de qualificação (Doutorando em Informática) - Universidade Federal do Amazonas.

Qualificações de Mestrado
1.
SILVA JUNIOR, W. S.; Carvalho, C. B.; CORDEIRO, L. C.. Participação em banca de Diego Alves Amoedo. Classificação Automática de Sinais Modulados Utilizando Máquina de Vetor de Suporte. 2016. Exame de qualificação (Mestrando em Engenharia Elétrica) - Universidade Federal do Amazonas.

2.
CORDEIRO, L. C.; Lucena Jr, V. F.; Cavalcante, A. L. D.. Participação em banca de Hiram Carlos Costa Amaral. MeDSE: Metodologia para Desenvolvimento de Sistemas Evolutivos. 2015. Exame de qualificação (Mestrando em Engenharia Elétrica) - Universidade Federal do Amazonas.

3.
CORDEIRO, L. C.; CHAVES FILHO, J. E.; DANGELO, M. F. S. V.. Participação em banca de Hussama Ibrahim Ismail. Verificação de Controladores Digitais Implementados em Processadores de Ponto Fixo Utilizando Teoria do Módulo da Satisfatibilidade. 2015. Exame de qualificação (Mestrando em Engenharia Elétrica) - Universidade Federal do Amazonas.

4.
CORDEIRO, L. C.; Costa Filho, C. F. F.; Netto, J. F. M.. Participação em banca de Endrews Snyder Souza da Silva. Proposta de um Agente para o Jogo de Dominó de 4 Pontas Utilizando Algoritmo EXPECTMINIMAX. 2015. Exame de qualificação (Mestrando em Engenharia Elétrica) - Universidade Federal do Amazonas.

Trabalhos de conclusão de curso de graduação
1.
CORDEIRO, L. C.; BARRETO, R. S.; Carvalho, C. B.. Participação em banca de Erickson Higor da Silva Alves.Um Método para Localizar Falhas em Software Concorrente em C. 2016. Trabalho de Conclusão de Curso (Graduação em Engenharia da Computação) - Universidade Federal do Amazonas.

2.
CORDEIRO, L. C.; Oliveira, H.; CRUZ, C. A. M.. Participação em banca de Denis Goebel Cavalli.Desenvolvimento de um Sistemas de Hardware e Software para Monitoramento Remoto e Controle Automático do Consumo Diário de Cargas Elétricas Residenciais via Smartphones Android. 2016. Trabalho de Conclusão de Curso (Graduação em Engenharia da Computação) - Universidade Federal do Amazonas.

3.
CORDEIRO, L. C.; CRUZ, C. A. M.; Carvalho, C. B.. Participação em banca de Higo Ferreira Albuquerque.Modelo Operacional CUDA para Verificação de Programas. 2016. Trabalho de Conclusão de Curso (Graduação em Engenharia da Computação) - Universidade Federal do Amazonas.

4.
CORDEIRO, L. C.; DA SILVA, WALDIR SABINO; CRUZ, C. A. M.. Participação em banca de Luciana de Aguiar Sena.Pesquisa sobre Detectores por Produto Interno no Cenário de Detecção de Pontos Fiduciais. 2016. Trabalho de Conclusão de Curso (Graduação em Engenharia da Computação) - Universidade Federal do Amazonas.

5.
Cordeiro, L.; Barreto, R. S.; CRUZ, C. A. M.. Participação em banca de William Castro Rosa.Implementação e Avaliação de Planejamento Global de Rotas com Funções Geodésicas.. 2015. Trabalho de Conclusão de Curso (Graduação em Engenharia Elétrica - Eletrônica) - Universidade Federal do Amazonas.

6.
SILVA JUNIOR, W. S.; LUCENA JUNIOR, V. F.; CORDEIRO, L. C.. Participação em banca de Pablo Guimarães da Silva e Silva.Interface de Comunicação para Diagnóstico de um Sistema de Automação Industrial. 2014. Trabalho de Conclusão de Curso (Graduação em Engenharia Elétrica) - Universidade Federal do Amazonas.

7.
SILVA JUNIOR, W. S.; CORDEIRO, L. C.; LUCENA JUNIOR, V. F.. Participação em banca de Israel Lima Marinho.Projeto e Implementação de uma Interface de Usuário Inteligente para um Andador Automatizado. 2014. Trabalho de Conclusão de Curso (Graduação em Engenharia Elétrica) - Universidade Federal do Amazonas.

8.
BARRETO, R. S.; CORDEIRO, L. C.; CALDAS, R. B.. Participação em banca de Diego Quintana Pinheiro.Uma Metodologia para Análise Estática do Comportamento de Tarefas em Sistemas de Tempo Real Críticos com Baixo Consumo de Energia. 2013. Trabalho de Conclusão de Curso (Graduação em Ciência da Computação) - Universidade Federal do Amazonas.

9.
SILVA JUNIOR, W. S.; Dos Santos, K. V.; CORDEIRO, L. C.. Participação em banca de Felipe Batista Barbosa.Análise de Falhas em Imagens de Canetas Esferográficas Utilizando Métodos Morfológicos. 2013. Trabalho de Conclusão de Curso (Graduação em Engenharia Elétrica - Eletrônica) - Universidade Federal do Amazonas.

10.
CHAVES FILHO, J. E.; SILVA JUNIOR, W. S.; CORDEIRO, L. C.. Participação em banca de Adriano Bruno dos Santos Frutuoso.Controle de Posição dos Elos do Robô Manipulador RD5NT usando o Arduino Duemilanove e o Software MATLAB. 2012. Trabalho de Conclusão de Curso (Graduação em Engenharia Elétrica) - Universidade Federal do Amazonas.

11.
CHAVES FILHO, J. E.; SILVA JUNIOR, W. S.; CORDEIRO, L. C.. Participação em banca de André Henrique Lameira dos Santos.Desenvolvimento de um Protótipo de Placa para Acionamento do Manipulador Robótico RD5NT. 2012. Trabalho de Conclusão de Curso (Graduação em Engenharia Elétrica) - Universidade Federal do Amazonas.

12.
CHAVES FILHO, J. E.; SILVA JUNIOR, W. S.; CORDEIRO, L. C.. Participação em banca de Jonathan Cavalcante de Oliveira.Sistemas de Controle Digital para o Conversor DC-DC Buck em FPGA. 2012. Trabalho de Conclusão de Curso (Graduação em Engenharia Elétrica) - Universidade Federal do Amazonas.

13.
Souza, R. C. R.; CORDEIRO, L. C.; F.C.R Souza; Sardinha, M.. Participação em banca de Paulo Có.Aproveitamento Energético dos Resíduos Agroindustriais no Estado do Amazonas. 2012. Trabalho de Conclusão de Curso (Graduação em Engenharia Elétrica - Eletrotécnica) - Universidade Federal do Amazonas.

14.
SILVA JUNIOR, W. S.; CORDEIRO, L. C.; Dos Santos, K. V.. Participação em banca de Makoto Miyagawa.Sistemas de Venda Automática Utilizando Pagamento Eletrônico Através de Dispositivos Móveis. 2012. Trabalho de Conclusão de Curso (Graduação em Engenharia da Computação) - Universidade Federal do Amazonas.

15.
SILVA JUNIOR, W. S.; CORDEIRO, L. C.; PIMENTA, N. L.. Participação em banca de Sonny de Souza Costa Miranda.Sistema de Monitoramento de Sensores Utilizando o Protocolo ZigBee para Comunicação sem Fio. 2012. Trabalho de Conclusão de Curso (Graduação em Engenharia da Computação) - Universidade Federal do Amazonas.

16.
SILVA JUNIOR, W. S.; CHAVES FILHO, J. E.; CORDEIRO, L. C.. Participação em banca de Igor Giovanni Correa de Oliveira.Aquisição de Imagens através da Câmera C328R utilizando Plataforma de Baixo Custo. 2012. Trabalho de Conclusão de Curso (Graduação em Engenharia Elétrica - Eletrônica) - Universidade Federal do Amazonas.

17.
SILVA JUNIOR, W. S.; CORDEIRO, L. C.; SAMPAIO, V.. Participação em banca de Bruno Megnani Degan.Controle Automático de um Portão Eletrônico através do Reconhecimento de Voz em Dispositivos Móveis. 2012. Trabalho de Conclusão de Curso (Graduação em Engenharia da Computação) - Universidade Federal do Amazonas.

18.
Dias-Neto, A. C.; BARRETO, R. S.; CORDEIRO, L. C.. Participação em banca de Andreza Morgana Fonseca Viana de Castro.Extensão da Ferramenta Selenium RC para Realização de Testes Funcionais com Bases de Dados. 2012. Trabalho de Conclusão de Curso (Graduação em Engenharia da Computação) - Universidade Federal do Amazonas.

19.
Souza, R. C. R.; F.C.R Souza; CORDEIRO, L. C.; Sardinha, M.. Participação em banca de Marcelo Monteiro da Silva.Sistema informatizado para apoio a projetos de sistemas PV. 2011. Trabalho de Conclusão de Curso (Graduação em Engenharia Elétrica) - Universidade Federal do Amazonas.

20.
Souza, R. C. R.; F.C.R Souza; Sardinha, M.; CORDEIRO, L. C.. Participação em banca de Prisciane Cristina Pimentel de Paula.Cálculo de Emissões em 09 (Nove) Unidades Consumidoras participantes do Projeto Piloto Gestão Estadual Eficiente de Energia Elétrica para Redução e Controle do Consumo das Unidades Consumidoras. 2011. Trabalho de Conclusão de Curso (Graduação em Engenharia Elétrica) - Universidade Federal do Amazonas.

21.
Souza, R. C. R.; F.C.R Souza; Sardinha, M.; CORDEIRO, L. C.. Participação em banca de Guarniery Lima De Souza.Produção de etanol para uso na frota veicular da Universidade Federal do Amazonas em Manaus. 2011. Trabalho de Conclusão de Curso (Graduação em Engenharia Elétrica) - Universidade Federal do Amazonas.

22.
Souza, R. C. R.; F.C.R Souza; Sardinha, M.; CORDEIRO, L. C.. Participação em banca de Lindolfo dos Santos Rodrigues Júnior.Eficiência Elétrica via Dispositivos Eletrônicos de Partida de Motores de Indução Trifásicos. 2011. Trabalho de Conclusão de Curso (Graduação em Engenharia Elétrica) - Universidade Federal do Amazonas.

23.
Souza, R. C. R.; F.C.R Souza; Sardinha, M.; CORDEIRO, L. C.. Participação em banca de Neivaldo de Souza Mattos.Sistema Fotovoltáico e suas Aplicações: Um Estudo de Caso de Viabilidade Econômica na Cidade de Manaus. 2011. Trabalho de Conclusão de Curso (Graduação em Engenharia Elétrica) - Universidade Federal do Amazonas.

24.
CHAVES FILHO, J. E.; SILVA JUNIOR, W. S.; CORDEIRO, L. C.. Participação em banca de Thales Ruano Barros de Souza.Projeto de uma Estratégia de Controle para o Pêndulo Invertido Simples sobre Carrinho. 2011. Trabalho de Conclusão de Curso (Graduação em Engenharia Elétrica) - Universidade Federal do Amazonas.



Participação em bancas de comissões julgadoras
Concurso público
1.
CORDEIRO, L. C.; Cavalcante, A. L. D.; Guimarães, W. P. S.. Concurso Público de Carreira do Magistério Superior Edital 06/2014 - Departamento de Eletrônica e Computação - Área: Sistemas Digitais e Automação Industrial. 2014. Universidade Federal do Amazonas.

2.
Souza, R. C. R.; CORREIA, J. C.; CORDEIRO, L. C.. Concurso Público de Carreira do Magistério Superior Edital 06/2014 - Departamento de Eletricidade - Área: Sistemas Elétricos de Potência. 2014. Universidade Federal do Amazonas.



Eventos



Participação em eventos, congressos, exposições e feiras
1.
1st International KLEE Workshop on Symbolic Execution. 2018. (Encontro).

2.
21st ACM International Conference on Hybrid Systems: Computation and Control. DSValidator: An Automated Counterexample Reproducibility Tool for Digital Systems. 2018. (Congresso).

3.
30th International Conference on Computer Aided Verification. 2018. (Congresso).

4.
Chevening Cyber-Security Fellowship. 2018. (Encontro).

5.
International Summer School on Satisfiability, Satisfiability Modulo Theories, and Automated Reasoning. 2018. (Seminário).

6.
The third-annual Arm Research Summit. 2018. (Encontro).

7.
23rd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). DepthK: A k-Induction Verifier Based on Invariant Inference for C Programs. 2017. (Congresso).

8.
26th ACM SIGSOFT International Symposium on Software Testing and Analysis.Verifying digital systems with MATLAB. 2017. (Simpósio).

9.
29th International Conference on Computer-Aided Verification. Automated Formal Synthesis of Digital Controllers for State-Space Physical Plants. 2017. (Congresso).

10.
32nd IEEE/ACM International Conference on Automated Software Engineering. DSSynth: An Automated Digital Controller Synthesis Tool for Physical Plants. 2017. (Congresso).

11.
ACM Symposium on Applied Computing, Software Verification and Testing. Verifying CUDA Programs using SMT-Based Context-Bounded Model Checking. 2016. (Congresso).

12.
Community-based Sustainable Energy: Combining wireless systems, smart micro-generation and education workshop.Software Model Checking in Embedded Systems. 2016. (Outra).

13.
Intel Developer Forum. 2016. (Outra).

14.
Kent Concurrency Workshop on Concurrency Theory and related topics. 2016. (Outra).

15.
VI Brazilian Symposium on Computing Systems Engineering. 2016. (Congresso).

16.
22nd International SPIN Symposium on Model Checking of Software (SPIN 2015).DSVerifier: A Bounded Model Checking Tool for Digital Systems. 2015. (Simpósio).

17.
V Brazilian Symposium on Computing Systems Engineering. 2015. (Congresso).

18.
20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems. ESBMC 1.22 (Competition Contribution). 2014. (Congresso).

19.
IEEE 3rd Global Conference on Consumer Electronics. BMCLua: Verification of Lua Programs in Digital TV Interactive Applications. 2014. (Congresso).

20.
IV Simpósio Brasileiro de Engenharia de Sistemas Computacionais. 2014. (Congresso).

21.
19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Handling Unbounded Loops with ESBMC 1.20. 2013. (Congresso).

22.
XXXI Simpósio Brasileiro de Telecomunicações. Verificação de Códigos Lua Utilizando BMCLua. 2013. (Congresso).

23.
18th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Context-Bounded Model Checking with ESBMC 1.17. 2012. (Congresso).

24.
3rd IEEE Biosignals and Biorobotics Conference (ISSNIP). 2012. (Congresso).

25.
ACM/IEEE 33rd International Conference on Software Engineering, Technical/Research Track. Verifying Multi-threaded Software using SMT-based Context-Bounded Model Checking. 2011. (Congresso).

26.
17th IEEE International Conference and Workshops on Engineering of Computer-Based Systems. Continuous Verification of Large Embedded Software using SMT-Based Bounded Model Checking. 2010. (Congresso).

27.
8th International Workshop on Satisfiability Modulo Theories.Bounded Model Checking of Multi-threaded Software using SMT solvers. 2010. (Encontro).

28.
ACM/IEEE 32nd International Conference on Software Engineering.SMT-Based Bounded Model Checking for Multi-threaded Software in Embedded Systems. 2010. (Simpósio).

29.
DSSE 2010 Seminar.SMT-Based Bounded Model Checking for Embedded ANSI-C Software. 2010. (Seminário).

30.
DSSE 2010 Seminar.Bounded Model Checking of Multi-threaded Software using SMT solvers. 2010. (Seminário).

31.
The 6th International Conference on Embedded Software and Systems. Semiformal Verification of Embedded Software in Medical Devices Considering Stringent Hardware Constraints. 2009. (Congresso).

32.
4º Semana Acadêmica do Curso de Sistemas de Informação da Esbam.Gerenciamento de Configuração de Software. 2008. (Seminário).

33.
3º Semana Acadêmica do Curso de Sistemas de Informação da Esbam.Uma Metodologia de Desenvolvimento de HW/SW Ágil para Sistemas Embarcados. 2007. (Seminário).

34.
Semana de Ciência e Tecnologia do Estado do Amazonas.Metodologia de Desenvolvimento Ágil Scrum: O Caso XMPM. 2006. (Seminário).

35.
Software Configuration and Build Management.Software Configuration and Build Management. 2005. (Encontro).

36.
SugarLoafPLoP 2005. 5º Conferência Latino-Americana em Linguagem de Padrões para Programação. 2005. (Congresso).

37.
Ringvorlesung - Verfahren der Softwaretechnik.XML - Chancen und Möglichkeiten aus dem Blickwinkel der Automatisierungstechnik. 2003. (Seminário).

38.
Ringvorlesung - Verfahren der Softwaretechnik.Experience with Linux in Real-Time Systems. 2003. (Seminário).


Organização de eventos, congressos, exposições e feiras
1.
BRITO, A. ; MATIAS JR., R. ; BECK FILHO, A. C. S. ; GRACIOLI, G. ; CORDEIRO, L. C. . Intel Embedded Systems Contest. 2016. (Outro).

2.
LUCENA JUNIOR, V. F. ; CHAVES FILHO, J. E. ; SILVA JUNIOR, W. S. ; CORDEIRO, L. C. . 3rd ISSNIP Biosignals and Biorobotics Conference. 2012. (Congresso).



Orientações



Orientações e supervisões em andamento
Dissertação de mestrado
1.
Felipe Rodrigues Monteiro Sousa. Verificação contínua do software embarcado usando verificação de modelo. Início: 2018. Dissertação (Mestrado em Informática) - Universidade Federal do Amazonas. (Orientador).

2.
Kellen Adriely Alvarenga Guimarães. Síntese de Controladores Digitais usando Redes Neurais Artificais. Início: 2018. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas. (Orientador).

3.
Adriana Silva de Souza. Verificação de Programas Multi-tarefas Baseados no Framework Multi-plataforma Qt. Início: 2017. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, Fundação de Amparo a Pesquisa do Estado do Amazonas. (Orientador).

4.
Thiago Rodrigo Félix Cavalcante. Counterexample-Guided Inductive Synthesis of Digital Controllers for Physical Plants. Início: 2017. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas. (Orientador).

5.
Higo Ferreira Albuquerque. Sistema de transporte indoor aplicados à intralogística usando veículos aéreos não tripulados com planejamento ótimo de missão. Início: 2016. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas. (Orientador).

6.
Phillipe Arantes Pereira. Verificação de Programas Multitarefas via Sequencialização Preguiçosa. Início: 2015. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, Instituto Nokia de Tecnologia. (Orientador).

Tese de doutorado
1.
Omar Alhawi. Automatic Detection and Repair of Software Vulnerabilities in Unmanned Aerial Vehicles. Início: 2018. Tese (Doutorado em Computer Science) - University of Manchester. (Orientador).

2.
Kaled Alshmrany. Finding Vulnerabilities in Network Protocols using Fuzzing and Symbolic Execution. Início: 2018. Tese (Doutorado em Computer Science) - University of Manchester. (Orientador).

3.
Samiah Alghamdi. Using Program Synthesis for Program Repair in IoT Security. Início: 2018. Tese (Doutorado em Computer Science) - University of Manchester. (Orientador).

4.
Alessandro Bezerra Trindade. Aplicando verificação paralela de modelos baseada nas teorias do módulo da satisfabilidade para o particionamento de hardware/software em sistemas embarcados com múltiplas CPUs. Início: 2015. Tese (Doutorado em Informática) - Universidade Federal do Amazonas. (Orientador).


Orientações e supervisões concluídas
Dissertação de mestrado
1.
Lennon Corrêa Chaves. Formal Verification Applied to Attitude Control Software of Unmanned Aerial Vehicles. 2018. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, Fundação de Amparo a Pesquisa do Estado do Amazonas. Orientador: Lucas Carvalho Cordeiro.

2.
Raimundo Williame Rocha de Melo. Verificação de Programas Embarcados ANSI-C Baseada em Indução Matemática e Invariantes. 2017. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, Fundação de Amparo a Pesquisa do Estado do Amazonas. Orientador: Lucas Carvalho Cordeiro.

3.
Mário Angel Praia Garcia. Verificação de Programas C++ Baseados no Framework Cross-platform Qt. 2016. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, . Orientador: Lucas Carvalho Cordeiro.

4.
Erickson Higo da Silva Alves. Um método para localizar falhas em programas concorrentes C. 2016. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, . Coorientador: Lucas Carvalho Cordeiro.

5.
Alessandro Bezerra Trindade. Aplicando Verificação Formal Baseada nas Teorias do Módulo da Satisfabilidade para o Particionamento de Hardware/Software em Sistemas Embarcados. 2015. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, . Orientador: Lucas Carvalho Cordeiro.

6.
Hussama Ibrahim Ismail. Verificação de Modelos Aplicada ao Projeto de Controladores Digitais Implementados em Processadores de Ponto-Fixo. 2015. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, . Orientador: Lucas Carvalho Cordeiro.

7.
Francisco de A. P. Januário. BMCLua: Metodologia para Verificação de Códigos Lua Utilizando Bounded Model Checking. 2015. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. Orientador: Lucas Carvalho Cordeiro.

8.
Renato Barbosa Abreu. Avaliação de Projetos de Filtros Digitais de Ponto-Fixo usando Teorias do Módulo da Satisfatibilidade. 2014. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, . Orientador: Lucas Carvalho Cordeiro.

9.
Mikhail Yasha Ramalho Gadelha. Verificação Baseada em Indução Matemática para Programas C++. 2013. Dissertação (Mestrado em Engenharia Elétrica) - Universidade Federal do Amazonas, Fundação de Amparo a Pesquisa do Estado do Amazonas. Orientador: Lucas Carvalho Cordeiro.

10.
Jie Gao. Fault Localization of Multi-threaded C Programs using Model Checking. 2010. Dissertação (Mestrado em Software Engineering) - University of Southampton, . Coorientador: Lucas Carvalho Cordeiro.

11.
Sze Pan Ben Yiu. Model Checking Concurrent Software with SAT. 2009. Dissertação (Mestrado em Software Engineering) - University of Southampton, . Coorientador: Lucas Carvalho Cordeiro.

Tese de doutorado
1.
Herbert Oliveira Rocha. Verificação de Sistemas de Software baseada em Transformações de Código usando Bounded Model Checking. 2015. Tese (Doutorado em Informática) - Universidade Federal do Amazonas, Fundação de Amparo a Pesquisa do Estado do Amazonas. Coorientador: Lucas Carvalho Cordeiro.

Trabalho de conclusão de curso de graduação
1.
Erickson Higor da Silva Alves. Um Método para Localizar Falhas em Software Concorrente em C. 2016. Trabalho de Conclusão de Curso. (Graduação em Engenharia da Computação) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

2.
Denis Goebel Cavalli. Desenvolvimento de um Sistemas de Hardware e Software para Monitoramento Remoto e Controle Automático do Consumo Diário de Cargas Elétricas Residenciais via Smartphones Android. 2016. Trabalho de Conclusão de Curso. (Graduação em Engenharia da Computação) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

3.
Higo Ferreira Albuquerque. Modelo Operacional CUDA para Verificação de Programas. 2016. Trabalho de Conclusão de Curso. (Graduação em Engenharia da Computação) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

4.
Flávio Ipiranga de Araújo Júnior. Análise do Consumo de Energia dos Modos de Standby de um Módulo Receptor de Televisão Digital. 2016. Trabalho de Conclusão de Curso. (Graduação em Engenharia da Computação) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

5.
Alison de Oliveira Venâncio. Desenvolvimento de um Controlador para Locomoção de uma Cadeira de Rodas via Toque e Comando de Voz Uitilizando o Protocolo Android Open Acessory. 2015. Trabalho de Conclusão de Curso. (Graduação em Engenharia da Computação) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

6.
Phillipe Arantes Pereira. (Estágio Supervisionado) Desenvolvimento de um Modelo em VHDL para Avaliação de Corretude e Desempenho do Processador MIPS usando Arquiteturas Baseadas em Multiciclo e Pipeline. 2015. Trabalho de Conclusão de Curso. (Graduação em Engenharia da Computação) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

7.
William Castro Rosa. Implementação e Avaliação de Planejamento Global de Rotas com Funções Geodésicas. 2015. Trabalho de Conclusão de Curso. (Graduação em Engenharia Elétrica - Eletrônica) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

8.
Ícaro Nóbrega de Sousa. Desenvlvimento de um Sistemas de Hardware e Software para Monitoramento Remoto e Controle Automático do Consumo Diário de Cargas Elétricas Residenciais. 2014. Trabalho de Conclusão de Curso. (Graduação em Engenharia Elétrica) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

9.
Francisco Fagner do Rego Cunha. Co-Projeto de Hardware/Software de uma Rede Reural Artifical Utilizando FPGA com o Processador NIOS II. 2014. Trabalho de Conclusão de Curso. (Graduação em Engenharia da Computação) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

10.
Jefferson Dionizio Soares de Souza. Localização e Estimação de Tempo para Transporte Público Urbano usando GPS e Internet. 2013. Trabalho de Conclusão de Curso. (Graduação em Engenharia da Computação) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

11.
Marcelo Felipe Mazini dos Santos. Desenvolvimento de um Terminal para Consulta de Preços. 2013. Trabalho de Conclusão de Curso. (Graduação em Engenharia Elétrica) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

12.
George Corrêa de Araújo. Desenvolvimento de um Plug-in do Eclipse para Ferramenta ESBMC utilizando o Toolkit do ZEST. 2012. Trabalho de Conclusão de Curso. (Graduação em Engenharia da Computação) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

13.
Jhony Braga da Silva. Sistema de Medição de Temperatura Integrado a TV Digital. 2012. Trabalho de Conclusão de Curso. (Graduação em Engenharia da Computação) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

14.
Fábio de Souza Lima. Uma Arquitetura de um Sistema Supervisório Aplicada a Célula Combustível. 2011. Trabalho de Conclusão de Curso. (Graduação em Engenharia Elétrica) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

Iniciação científica
1.
Vithória dos Santos Barbosa. Verificação de Controladores Digitais de Ponto-fixo usando Realizações de Formas Diretas e Deltas. 2015. Iniciação Científica. (Graduando em Engenharia Elétrica - Eletrônica) - Universidade Federal do Amazonas, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: Lucas Carvalho Cordeiro.

2.
Valdeson Dantas de Souza. Avaliação de Projetos de Filtros Digitais de Ponto-Fixo usando Verificação de Modelos. 2015. Iniciação Científica. (Graduando em Engenharia Elétrica - Telecomunicações) - Universidade Federal do Amazonas, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: Lucas Carvalho Cordeiro.

3.
Felipe Rodrigues Monteiro Sousa. Verificação de Controladores Digitais de Ponto Fixo Representados por Espaço de Estados. 2015. Iniciação Científica. (Graduando em Engenharia da Computação) - Universidade Federal do Amazonas, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: Lucas Carvalho Cordeiro.

4.
Mateus Martínez de Lucena. Desenvolvimento de um Modelo Operacional para Verificação de Projetos de Sistemas Digitais em SystemC. 2014. Iniciação Científica. (Graduando em Engenharia da Computação) - Universidade Federal do Amazonas, Conselho Nacional de Desenvolvimento Científico e Tecnológico. Orientador: Lucas Carvalho Cordeiro.

5.
Felipe Rodrigues Monteiro Sousa. Verificação Formal de Programas C++ que Usam o Framework Multi-Plataforma QT. 2013. Iniciação Científica. (Graduando em Engenharia da Computação) - Universidade Federal do Amazonas, Coordenação de Aperfeiçoamento de Pessoal de Nível Superior. Orientador: Lucas Carvalho Cordeiro.

6.
Luciano Nunes Sobral. Verificação de Modelos de Hardware que Usam a Biblioteca do SystemC. 2013. Iniciação Científica. (Graduando em Engenharia da Computação) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

Orientações de outra natureza
1.
Felipe Rodrigues Monteiro Sousa. (Estágio Supervisionado) Verificação de Controladores Digitais de Ponto Fixo Representados por Espaço de Estados. 2018. Orientação de outra natureza. (Engenharia da Computação) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

2.
Luciana de Aguiar Sena. (Estágio Supervisionado) Desenvolvimento de uma Página Web para o Centro de Tecnologia Eletrônica e da Informação. 2016. Orientação de outra natureza. (Engenharia da Computação) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

3.
Flávio Ipiranga de Araújo Júnior. (Estágio Supervisionado) Desenvolvimento de uma Página Web para o Programa de Pós-Graduação em Engenharia Elétrica. 2016. Orientação de outra natureza. (Engenharia da Computação) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

4.
Thiago Rodrigo Félix Cavalcante. (Estágio Supervisionado) Simulação de Algoritmos e Aplicações em Redes Veiculares para o Programa de Capacitação de Recursos Humanos em Tecnologias da Informação e Computação e em Sistemas e Aplicativos para Plataformas Tecnológicas Portáteis, Móveis e Distribuídas. 2016. Orientação de outra natureza. (Engenharia da Computação) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

5.
Phillipe Arantes Pereira. Conversão de programas C concorrente em sequencial. 2015. Orientação de outra natureza. (Engenharia da Computação) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

6.
Higo Ferreira Albuquerque. (Estágio Supervisionado) Verificação de Programas C/C++ Baseado em Processadores de Vários Núcleos (CUDA). 2015. Orientação de outra natureza. (Engenharia da Computação) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

7.
William Castro da Rosa. (Estágio Supervisionado) Desenvolvimento de Algoritmo de Controle de Obturação Rolante para um Sensor de Imagem com Largo Alcance Dinâmico. 2014. Orientação de outra natureza. (Engenharia Elétrica) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

8.
Lissiane Melo Jacinto. (Estágio Supervisionado) Sala de Multimídia da Biblioteca Comunitária Vilma Palheta. 2013. Orientação de outra natureza. (Engenharia Elétrica - Eletrônica) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

9.
Jefferson Dionizio Soares de Souza. (Estágio Supervisionado) Controle e Manutenção do Laboratório de Informática da Escola Municipal João Alfredo. 2013. Orientação de outra natureza. (Engenharia da Computação) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.

10.
Fábio de Souza Lima. (Estágio Supervisionado) Manutenções Preventivas e corretivas em Equipamentos nos Laboratórios de Eletrônica e Mecatrônica da Fundação Nokia de Ensino. 2011. Orientação de outra natureza. (Engenharia Elétrica - Eletrônica) - Universidade Federal do Amazonas. Orientador: Lucas Carvalho Cordeiro.



Inovação



Projetos de pesquisa



Página gerada pelo Sistema Currículo Lattes em 19/12/2018 às 8:25:35