Sites Inria

Soutenance de thèse

Le Model Checking et preuve de théorèmes

Le model checking est une technique de vérification automatique de propriétés de correction de systèmes finis. Normalement, les outils de model checking ont deux caractéristiques remarquables : ils sont automatisés et ils produisent un contre-exemple si le système ne satisfait pas la propriété. La Déduction Modulo est une reformulation de la logique des prédicats où certains axiomes---possiblement tous---sont remplacés par des règles de réécriture.

  • Date : 25/09/2015
  • Lieu : 10h00 Salle 1006 - Bât. "Sophie-Germain" - Paris Diderot - 8, place Aurélie Nemours, 75013 Paris
  • Intervenant(s) : Kailiang Ji (Deducteam)

Le but de cette dissertation est de donner un encodage de propriétés temporelles exprimées en CTL en des formules du premier ordre, en exprimant l’équivalence logique entre les opérateurs temporels avec des règles de réécriture. De cette manière, les algorithmes de recherche de preuve conçus pour la Déduction Modulo, tels que la Résolution Modulo ou les Tableaux Modulo, peuvent être utilisés pour vérifier des propriétés temporelles de systèmes de transition finis.

Afin d’accomplir le but de résoudre des problèmes de model checking avec un prouveur automatique quelconque, trois travaux sont inclus dans cette dissertation. Premièrement, nous abordons le problème de parcours de graphes en model checking avec des prouveurs automatiques. Nous proposons comment traduire certains problèmes de parcours de graphes comme de la résolution. Nous présentons ensuite comment formuler les problèmes de model checking comme des formules du premier ordre en Déduction Modulo. La correction et la complétude de notre méthode montre que résoudre des problèmes de model checking CTL avec des prouveurs automatiques est faisable. Enfin, en nous appuyant sur la base théorique du deuxième travail, nous proposons une méthode de model checking symbolique. Cette méthode est implantée dans \tool{iProver Modulo}, qui est un prouveur automatique du premier ordre qui utilise la Résolution Modulo Polarisée.

Jury:

  • Philippe Schnoebelen (reviewers),
  • Sylvain Conchon (reviewers),
  • Gilles Dowek (supervisor),
  • Ying Jiang (examiner),
  • Francois Laroussinie (examiner).

Mots-clés : Soutenance Thèse Deducteam Model Checking Théorèmes

Haut de page

Suivez Inria