Recursos
Artigos técnicos, estudos de caso industriais e documentação de ferramentas para ajudar você a começar com a verificação formal de software.
Blog
Uma introdução acessível à verificação limitada de modelos; o que ela prova dentro de um limite de verificação, como difere da análise estática e dos testes, e por que os reguladores cada vez mais a recomendam como parte do caso de garantia.
Artigo completo em breve; entre em contato para ser notificado.
O ESBMC-Python identificou uma divisão por zero no helper integer_squareroot da especificação de consenso do Ethereum; a correção foi incorporada upstream como ethereum/consensus-specs PR #3600. Publicado no ACM SIGSOFT ISSTA 2024.
Artigo completo em breve; entre em contato para ser notificado.
Em nossa colaboração SAS 2024 com engenheiros da Arm, o ESBMC identificou 23 violações de propriedade adicionais no Realm Management Monitor além daquelas já detectadas pelo CBMC, e contribuiu com uma correção confirmada do modelo de memória upstream.
Artigo completo em breve; entre em contato para ser notificado.
Como a verificação formal baseada em ESBMC se integra aos fluxos de trabalho da ISO 26262, desde a geração de evidências classificadas por ASIL até a conformidade com MISRA C e a verificação de componentes AUTOSAR, combinada com nosso serviço de Qualificação de Ferramentas e Suporte à Certificação para os artefatos de qualificação que seu avaliador espera.
Artigo completo em breve; entre em contato para ser notificado.
Modelos de linguagem de grande porte aceleram a entrega, mas introduzem dívida de segurança em escala. O ESBMC-AI revela o que o LLM deixou passar e propõe correções candidatas para revisão do engenheiro, uma rede de segurança de métodos formais para equipes que adotam LLMs em seu fluxo de desenvolvimento.
Artigo completo em breve; entre em contato para ser notificado.
Ferramentas e referências
