4 posts
Los bounded model checkers como Kani y los relational model finders como Alloy permiten verificar propiedades con assertions y constraints ordinarios. Renuncias a las pruebas de liveness a cambio de una curva de aprendizaje medida en horas, no en semanas.
No necesitas aprender lógica temporal lineal para usar un model checker. Herramientas como Kani, CBMC y Alloy te permiten verificar propiedades con assertions…
Herramientas de model checking como Kani te permiten verificar propiedades de Rust con assertions en lugar de pruebas formales. El problema es lo que ocurre cuando tus bucles no tienen límites pequeños.
Puedes probar que tu código Rust es correcto sin escribir una sola prueba. La herramienta que lo hace se llama model checker, y para Rust el más práctico en…
El testing diferencial te permite encontrar bugs sin conocer la respuesta correcta. El problema es que los errores correlacionados parecen acuerdo. Así es como detectar los puntos ciegos.
Puedes confiar en el testing diferencial sin una prueba formal, pero solo si entiendes exactamente dónde se desmorona. La debilidad se llama common-mode…
La programación en N versiones asume que tus implementaciones coinciden. Analizamos por qué las pruebas no bastan, cómo los solucionadores SMT pueden demostrar equivalencia realmente y dónde trazar la línea entre lo suficientemente bueno y lo formalmente verificado.
Construiste un sistema de N versiones. Tres implementaciones independientes de la misma función crítica, un votante que elige el resultado mayoritario y una…