David Monniaux on Nostr: Tenez, je me demande si cela a encore du sens, en termes pratiques, les recherches ...

Tenez, je me demande si cela a encore du sens, en termes pratiques, les recherches sur les méthodes d'inférence d'invariants style interprétation abstraite pour faire de la preuve de programmes (méthodes qui sont de toute façon heuristiques, sans garantie de trouver des invariants, et souvent assez instables, notamment tout ce qui utilise du CEGAR).

Tu fais tourner un LLM, il te met des annotations Frama-C ou équivalent, tu les vérifies.