4 posts
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…
Differential testing permite encontrar bugs sem saber a resposta correta. O problema é que erros correlacionados parecem concordância. Veja como identificar os pontos cegos.
Você pode confiar em differential testing sem uma prova formal, mas apenas se entender exatamente onde ele falha. A fraqueza se chama common-mode failure.…
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…