Iniciou na segunda-feira (4), a 26ª edição do Simpósio Brasileiro de Métodos Formais (SBMF 2023), que acontece no Auditório 1 do Instituto de Computação da Universidade Federal do Amazonas (IComp/Ufam), até dia 8, sexta-feira. O destaque do primeiro dia de evento foi a 8ª edição da Escola Teoria de Ciência da Computação e Métodos Formais (ETMF), que incluiu palestras do professor Gustavo Carvalho, da Universidade Federal de Pernambuco (UFPE), e do professor Lucas Cordeiro, da Ufam e da Universidade de Manchester (UoM), no Reino Unido.
Nesse encontro científico que reúne especialistas, estudantes e profissionais de diversas partes do mundo para discutir a importância do desenvolvimento de sistemas computacionais com garantia de funcionamento correto, segurança e confiabilidade em sistemas de inteligência artificial, o professor Gustavo Carvalho apresentou exemplos de métodos formais utilizando diversas linguagens e ferramentas, como a de especificação Gallina, álgebra de processos CSP, verificação interativa e automatizada, e geração de código, na palestra intitulada “Métodos Formais: o que são e para que servem?”.
O professor da Ufam/UoM, Lucas Cordeiro, na palestra “Segurança de Sistemas de Software: explorando estratégias automatizadas de teste, verificação e síntese”, explorou os conceitos de segurança, as noções tradicionais e vulnerabilidades exclusivas dos sistemas de software de baixo nível, para estabelecer uma base robusta à construção de softwares seguros. Embora muitas pessoas não estejam cientes, os métodos formais desempenham um papel crucial no cotidiano, influenciando de maneira significativa diversas áreas.
Diante de um mundo mais conectado, a segurança se tornou um ponto crucial. “A gente vive em uma sociedade onde, cada vez mais, o software influencia nossas vidas, e esses softwares precisam operar corretamente. Portanto, é importante que a gente utilize técnicas baseadas em métodos formais nos contextos em que esperamos que o software funcione de maneira confiável, quase sempre, já que depositamos alta confiança nele. Empresas como Amazon, Google e Meta (Facebook) e várias outras têm investido no desenvolvimento nessa área”, explicou o professor Gustavo Carvalho.
Para ilustrar a presença cotidiana dos métodos formais, Carvalho trouxe um exemplo muito conhecido e que a maioria das pessoas utiliza. “Até mesmo o WhatsApp, utilizado diariamente por quase todos, se destaca por sua atenção especial à privacidade dos dados. Na Meta, uma equipe dedicada trabalha na verificação do código do WhatsApp, utilizando métodos formais para identificar e corrigir potenciais vulnerabilidades de privacidade. Este processo de análise é conduzido por meio de técnicas avançadas de métodos formais”, explicou Carvalho.
Outro exemplo da presença e utilização dos métodos formais está na utilização dos sistemas bancários, em especial, os digitais. “Os métodos formais são aplicados no sistema bancário de várias maneiras para garantir a segurança e a confiabilidade das operações. Todo aplicativo bancário usa um sistema de comunicação baseado em um esquema que chamamos de protocolo, se houver uma quebra nesses protocolos, eles indicam que houve uma invasão. Por isso, às vezes é preciso identificar o dispositivo correto, número de celular e e-mail ”, reforçou o coordenador geral do SBMF 2023, professor Edjard Mota.
A crescente presença de sistemas de inteligência artificial em diversos aspectos da vida humana destaca a urgência de investir ainda mais nos métodos formais. “A ampla influência desses sistemas nos expõe a desafios significativos, como a capacidade de transformar imagens em vídeos, muitas vezes passando despercebido como um conteúdo original. Esse fenômeno, se não abordado com segurança adequada, pode resultar em riscos como golpes ou disseminação de Fake News. Diante da proximidade crescente desses sistemas com nossas interações diárias, garantir a segurança e a confiabilidade é essencial para enfrentar os desafios emergentes e promover o uso responsável da inteligência artificial em nossa sociedade”, frisou o coordenador.
SOBRE O EVENTO
Esta edição marca o retorno presencial do evento, que ocorreu virtualmente nos últimos três anos. Os palestrantes principais incluem o professor Artur D’avila Garcez, da Universidade da Cidade de Londres, abordando a IA Neurosimbólica para Alcançar uma IA Confiável, e a professora Chantal Keller, da Université Paris-Saclay, com enfoque no Raciocínio Automatizado para a Teoria dos Tipos.
Simultaneamente ao SBMF 2023, o IComp sedia, nesta terça-feira (5), a segunda edição do Workshop Internacional Sobre Raciocínio Formal Automatizado Para Garantir Sistemas de IA Confiáveis (AFRITS 2023). Originado em Manchester, Inglaterra, este workshop discutirá os desafios e principais problemas relacionados à IA confiável, seu processo automatizado, segurança cibernética, bem como a relação entre segurança e inteligência artificial.
O workshop é aberto ao público, abrangendo alunos, professores, pesquisadores, empresas e instituições interessadas. Além das apresentações, o evento contará com palestras, exposição de pôsteres e uma mesa redonda com o tema “Raciocínio Formal Automatizado para Sistemas de IA Confiáveis”.
