Ce qui est dommage c'est que la communauté Linux s'intéresse très peu à ces sujets-là.
Parce que ce sont des bricoleurs. Ce n'est pas péjoratif pour moi.
ACSL, que tu cites, semble parfaitement utilisable et très intéressant. On pourrait même générer certaines descriptions à partir des "asserts" déjà dans le code.
J'ai vu une conférence sur sqlite. Ils font des choses assez poussées dans ce domaine mais ce n'est pas du "formel" (des tests de couverture).
En fait, il faudrait utiliser clang et LLVM pour faire des choses en automatique sur l'AST directement. Les projets dont tu parles sont antérieurs. Ca va arriver.
[^] # Re: Virtualisation par défaut
Posté par keyser.dyson . En réponse à la dépêche Capsicum dans Linux : ça bouge !. Évalué à 0.
Parce que ce sont des bricoleurs. Ce n'est pas péjoratif pour moi.
ACSL, que tu cites, semble parfaitement utilisable et très intéressant. On pourrait même générer certaines descriptions à partir des "asserts" déjà dans le code.
J'ai vu une conférence sur sqlite. Ils font des choses assez poussées dans ce domaine mais ce n'est pas du "formel" (des tests de couverture).
En fait, il faudrait utiliser clang et LLVM pour faire des choses en automatique sur l'AST directement. Les projets dont tu parles sont antérieurs. Ca va arriver.