4 posts
Les bounded model checkers comme Kani et les relational model finders comme Alloy permettent de vérifier des propriétés avec des assertions et des contraintes ordinaires. Vous renoncez aux preuves de liveness pour une courbe d'apprentissage mesurée en heures.
Vous n'avez pas besoin d'apprendre la logique temporelle linéaire pour utiliser un model checker. Des outils comme Kani, CBMC et Alloy vous permettent de…
Des outils de model checking comme Kani permettent de vérifier des propriétés Rust avec des assertions au lieu de preuves formelles. Le hic, c'est ce qui se passe quand vos boucles n'ont pas de petites bornes.
Vous pouvez prouver votre code Rust correct sans écrire une seule preuve. L'outil qui le fait s'appelle un model checker, et pour Rust le plus pratique en ce…
Le differential testing permet de trouver des bugs sans connaître la réponse correcte. Le problème est que des erreurs corrélées ressemblent à un accord. Voici comment repérer les angles morts.
Vous pouvez faire confiance au differential testing sans preuve formelle, mais seulement si vous comprenez exactement où il s'effondre. La faiblesse s'appelle…
La programmation N-version part du principe que vos implémentations sont d'accord. Nous voyons pourquoi les tests ne suffisent pas, comment les solveurs SMT peuvent prouver l'équivalence, et où tracer la ligne entre 'suffisamment bon' et 'formellement vérifié'.
Vous avez construit un système N-version. Trois implémentations indépendantes de la même fonction critique, un votant qui choisit le résultat majoritaire, et…