verification

5 posts

cleanroom-correctnesszero-defectsverificationcase-study

Quelqu'un a-t-il vraiment vérifié 10 000 lignes avec zéro défaut ? IBM l'a fait, et la méthodologie est plus étrange que le résultat.

Cleanroom software engineering promettait des incréments zero-defect grâce à la mathematical verification au lieu du debugging. Nous examinons les données réelles du projet IBM pour voir si l'affirmation tenait debout.

La moyenne de l'industrie logicielle dans les années 1980 était de 30 à 60 défauts par millier de lignes de code. L'équipe Cleanroom d'IBM a livré un incrément…
model-checkingautoverusrustverification

AutoVerus transforme 40 heures d'écriture de proof en 3 appels LLM. L'astuce consiste à savoir quand abandonner.

AutoVerus utilise un réseau d'agents LLM pour générer des proofs de correction Verus pour du code Rust, automatisant plus de 90% des proof obligations via une boucle générer-réparer-discharger pilotée par le feedback du solveur SMT.

La partie la plus difficile de la vérification formelle n'a jamais été le vérificateur. C'est l'écriture du proof. Donnez à un ingénieur Rust senior Verus, le…
model-checkingtemporal-logicformal-methodsverification

Vous pouvez vérifier du code par model checking sans apprendre la temporal logic

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…
model-checkingrustverificationformal-methods

Vous pouvez prouver votre code Rust correct sans écrire une seule preuve, mais l'espace d'états est la facture

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…
n-version-programmingequivalence-testingformal-methodsverification

Les Tests Ne Prouveront Jamais Que Deux Fonctions Sont Équivalentes. Voici Ce Qui Le Peut.

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…