Verificação e reconstrução eficientes de certificados SMT
O projeto Efficient checking and reconstruction of SMT proofs busca resolver o problema de não haver um verificador de certificados para solucionadores SMT que seja independente, eficiente e fácil de ser utilizado, pois os existentes são muito específicos, tem limitações de escalabilidade, são difíceis de serem utilizados, ou uma combinação destes.
O projeto se enquadra no contexto da pesquisa em resolução SMT, um campo ativo e de extrema importância para as grandes áreas de automatização de raciocínio e verificação formal, como subáreas de métodos formais e linguagens de programação.
O objetivo esperado é produzir um verificador de certificados de solucionadores SMT contendo novas técnicas de detalhamento e de compressão de certificados e que aceite o formato de certificados Alethe, já adotado pelos solucionadores SMT veriT (https://verit.loria.fr/) e cvc5 (https://cvc5.github.io/), permitirá a extensão do formato Alethe para elementos específicos de certificados de outros sistemas, assim aumentando as chances deste formato ser adotado como padrão pela comunidade, o que levaria a uma maior adoção da produção de certificados na comunidade de SMT e de seus usuários.
O prêmio é de uma uma doação irrestrita de U$40.000, além de U$20.000 em créditos para computação na nuvem da AWS.
O Amazon Research Award (ARA) financia propostas em diversas áreas de pesquisa relevantes para a Amazon, como robótica, machine learning, segurança, sustentabilidade e muito mais. Juntos, a ARA e a MLRA financiaram mais de 400 prêmios de pesquisa em 150 universidades em 28 países ao redor do mundo.
Visite o site do Amazon Research Award
