5 posts
Cleanroom software engineering prometeu incrementos zero-defect através de mathematical verification em vez de debugging. Analisamos os dados reais do projeto da IBM para ver se a afirmação se sustentou.
A média da indústria de software na década de 1980 era de 30 a 60 defeitos por mil linhas de código. A equipe Cleanroom da IBM entregou um incremento de…
AutoVerus utiliza uma rede de agents LLM para gerar proofs de correção Verus para código Rust, automatizando mais de 90% das proof obligations por meio de um loop gerar-reparar-discharge impulsionado pelo feedback do solver SMT.
A parte mais difícil da verificação formal nunca foi o verificador. É escrever o proof. Dê a um engenheiro sênior de Rust o Verus, o verificador baseado em SMT…
Bounded model checkers como Kani e relational model finders como Alloy permitem verificar propriedades com assertions e constraints ordinários. Você abre mão de provas de liveness por uma curva de aprendizado medida em horas, não em semanas.
Você não precisa aprender lógica temporal linear para usar um model checker. Ferramentas como Kani, CBMC e Alloy permitem verificar propriedades com assertions…
Ferramentas de model checking como Kani permitem verificar propriedades de Rust com assertions em vez de provas formais. O problema é o que acontece quando seus loops não têm limites pequenos.
Você pode provar que seu código Rust está correto sem escrever uma única prova. A ferramenta que faz isso se chama model checker, e para Rust o mais prático no…
A programação N-version assume que suas implementações concordam. Veja por que os testes não são suficientes, como os solvers SMT podem de fato provar equivalência, e onde traçar a linha entre bom o suficiente e formalmente verificado.
Você construiu um sistema n-version. Três implementações independentes da mesma função crítica, um voter que escolhe o resultado da maioria, e uma sensação de…