Collaboration avec le laboratoire LSL du CEA Saclay
Abstract
L'objectif des travaux de ce projet est d'étendre les capacités du solveur SMT Alt-Ergo pour qu'il fournisse des certificats (explications et traces de preuve), des modèles et des interpolants afin qu'il puisse être interfacé avec des outils de méthodes formelles, et en particulier avec ceux développés par le projet
ProVal, l'équipe ForTesSe et le laboratoire LSL.
Context
Les équipes ProVal et ForTeSE et le laboratoire LSL proposent des méthodes formelles et outils de développement logiciel basés sur des techniques de preuves déductives, de tests et d'analyses statiques.
Afin d'envisager leur utilisation dans un cadre industriel, ces approches exigent notamment l'utilisation de démonstrateurs automatiques efficaces pour traiter les nombreuses formules logiques qu'elles engendrent.
Cette intégration repose sur la capacité du démonstrateur automatique à produire des modèles ou des interpolants pour les formules logiques qui lui sont soumises en entrée. Les avancées récentes des solveurs SMTen font aujourd'hui les outils les plus adaptés à ces approches.
Objectives
L'équipe ProVal développe le solveur SMT Alt-Ergo. Ce démonstrateur est aujourd'hui capable de traiter des formules dans une logique du premier ordre multi-sortée et polymorphe incluant des théories prédéfinies.
D'un point de vue théorique, l'objectif de cette thèse est, tout d'abord, d'étudier comment instrumenter les procédures de décision utilisées dans le solveur Alt-Ergo pour la production de certificats, de modèles et d'interpolants. Ensuite, il faudra proposer un mécanisme générique pour combiner ces résultats dans les deux schémas CC(X) et AC(X). Enfin, il conviendra d'étendre ces techniques aux autres parties du solveur (modules SAT et matching).
D'un point de vue pratique, il s'agira d'implémenter ces mécanismes dans Alt-Ergo et de vérifier leur pertinence en connectant Alt-Ergo aux outils de preuve déductive, de test et d'analyses statiques
développés par l'équipe ProVal et le laboratoire LSL.
Work program
Extra information
Prerequisite
Détails
Expected funding
Institutional funding
Status of funding
Expected
Candidates
Alain Mebsout
Actuellement Ingénieur Jeune Chercheur à l'INRIA
Titulaire d'un master recherche de l'université d'Oklahoma et d'un diplôme d'ingénieur de l'ISIMA
Utilisateur
Créé
Lundi 02 mai 2011 11:47:38 CEST
dernière modif.
Lundi 02 mai 2011 11:48:08 CEST
Fichiers joints
filename
créé
hits
filesize
Aucun fichier joint à cette fiche
Connexion
Ecole Doctorale Informatique Paris-Sud
Directrice
Nicole Bidoit Assistante
Stéphanie Druetta Conseiller aux thèses
Dominique Gouyou-Beauchamps
ED 427 - Université Paris-Sud
UFR Sciences Orsay
Bat 650 - aile nord - 417
Tel : 01 69 15 63 19
Fax : 01 69 15 63 87
courriel: ed-info à lri.fr