Pesquisa
Meus interesses de pesquisa e áreas de foco.
Sistemas de Cibersegurança
Pesquisa sobre métodos formais aplicados à cibersegurança, análise de protocolos de segurança e desenvolvimento de técnicas de verificação para sistemas seguros.
Sistemas Ciberfísicos
Modelagem e verificação de sistemas que integram processos computacionais e físicos, garantindo segurança e confiabilidade em aplicações críticas.
Sistemas Distribuídos
Modelagem e verificação de sistemas distribuídos, focando em protocolos, algoritmos e técnicas de verificação formal para sistemas concorrentes.
Sistemas em Tempo Real
Pesquisa sobre modelagem, verificação e análise de sistemas em tempo real utilizando autômatos temporizados e especificações de lógica temporal.
Sistemas Embarcados Críticos
Desenvolvimento de técnicas de verificação formal para sistemas embarcados em domínios críticos de segurança, garantindo correção e confiabilidade.
Autômatos Temporizados
Pesquisa fundamental sobre autômatos temporizados com relógios parcialmente independentes, desenvolvendo novos modelos e algoritmos de verificação para sistemas em tempo real.
Lógicas Temporais
Pesquisa sobre lógicas temporais para especificar e verificar propriedades de sistemas em tempo real e distribuídos, incluindo TCTL e outros formalismos temporais.
Simulação e Bissimulação
Desenvolvimento de relações de equivalência e técnicas de refinamento para sistemas temporizados e distribuídos utilizando teoria de simulação e bissimulação.
Verificação de Modelos
Aplicação de técnicas de verificação de modelos utilizando ferramentas como UPPAAL e SCADE para verificar a correção de sistemas em tempo real e distribuídos.
Métodos Formais
Aplicação de técnicas matemáticas e especificações formais para projetar, desenvolver e verificar sistemas de software e hardware com garantias rigorosas de correção.
Prova de Teoremas
Pesquisa sobre prova interativa de teoremas e assistentes de prova para verificar propriedades complexas de sistemas em tempo real e modelos de autômatos.
Testes Baseados em Modelos
Desenvolvimento de metodologias de teste derivadas de modelos formais para gerar automaticamente casos de teste para sistemas complexos e linhas de produtos de software.
Testes de Mutação
Pesquisa sobre técnicas de testes de mutação para avaliar a qualidade de conjuntos de testes e melhorar a eficácia dos testes em sistemas altamente configuráveis.
Linhas de Produtos de Software
Pesquisa sobre modelagem de variabilidade, teste de sistemas altamente configuráveis e escalabilidade de análise de variabilidade em linhas de produtos de software.
Análise e Representação Simbólica
Desenvolvimento de técnicas simbólicas e estruturas de dados para análise e verificação eficiente de grandes espaços de estados em sistemas temporizados e distribuídos.