Nouveau prouveur automatique pour l'analyse de programmes – SOPRANO

Notre société moderne s'appuie sur des infrastructures logiciels de
manière très importante et il devient clair que des logiciels sûres
ne peuvent être obtenues qu'avec l'aide de véritable outils de
vérification logicielle. Actuellement la plupart d'entre eux sont
basés sur des prouveurs automatiques extérieurs. Cependant ces prouveurs ne
répondent pas complètement aux attentes actuelles et futures pour la
vérification: manque de génération satisfaisante de modèles, manque
de raisonnement sur des théories difficiles (e.g. arithmétique à
virgule flottante), manque d'extensibilité pour des besoins nouveaux
ou spécifiques. Le projet SOPRANO vise à résoudre ces problèmes et
préparer la prochaine génération de prouveurs spécialisés pour la preuve
de programmes en rassemblant des experts académiques et industriels.
Nous concevrons un nouveau système pour la coopération de solvers,
focalisé sur la génération de modèle et empruntant des principes de
SMT (norme actuelle) et CP (connu en optimisation). Nous concevrons
de nouvelles procédures de décisions pour des théories difficiles à
résoudre et utile dans l'industrie tel que arithmétique à virgule
flottante, arithmétique non-linéaire, et tableaux. Ces idées seront
implémentées dans une plateforme libre, dont des évaluations
régulières par les partenaires industriels assureront l'adéquation
avec les problématiques industrielles.