Aller au menu Aller au contenu
Une voie, plusieurs choix
Informatique et Mathématiques appliquées
Une voie, plusieurs choix

> Formation > Cursus ingénieur

SAT/SMT Solving - WMM9MO46

A+Augmenter la taille du texteA-Réduire la taille du texteImprimer le documentEnvoyer cette page par mail cet article Facebook Twitter Linked In
  • Volumes horaires

    • CM : 18.0
    • TD : -
    • TP : -
    • Projet : -
    • Stage : -
    • DS : -
    Crédits ECTS : 3.0
  • Responsables : David MONNIAUX

Objectifs

Acquérir la théorie et la pratique des procédures de décision SAT (satisfiabilité booléenne) et SMT (enrichies avec des théories: arithmétique entière, rationnelle, etc.).

Ces procédures sont utilisables aussi bien en analyse automatique de logiciels et matériels qu'en optimisation combinatoire ou recherche de solutions en recherche opérationelle.

Contenu

  • Bases de logique
  • Algorithmique SAT: DPLL, CDCL
  • Algorithmique BDD (binary decision diagrams)
  • Algorithmique SMT (satisfiability modulo theory)
  • Travaux pratiques: utilisation d'un SMT-solveur

Prérequis

Logique mathématique de base: opérateurs logiques, quantificateurs
Algorithmique
Programmation

Contrôles des connaissances

Mini-projet + examen écrit

70% exam at the end of the course
30% practical assignment

L'examen existe uniquement en anglais FR

Calendrier

Le cours est programmé dans ces filières :

  • Cursus ingénieur - Master Informatique - Semestre 9 (ce cours est donné uniquement en anglais EN)
cf. l'emploi du temps 2022/2023

Informations complémentaires

Code de l'enseignement : WMM9MO46
Langue(s) d'enseignement : FR

Vous pouvez retrouver ce cours dans la liste de tous les cours.

Bibliographie

Kroening & Strichman, Decision procedures
Bradley & Manna, The calculus of computation
Biere et al, ed., The Handbook of Satisfiability

A+Augmenter la taille du texteA-Réduire la taille du texteImprimer le documentEnvoyer cette page par mail cet article Facebook Twitter Linked In

mise à jour le 10 mars 2020

Université Grenoble Alpes