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
  • Number of hours

    • Lectures : 18.0
    • Tutorials : -
    • Laboratory works : -
    • Projects : -
    • Internship : -
    • Written tests : -
    ECTS : 3.0
  • Officials : David MONNIAUX

Goals

Understanding how decision procedures for SAT (Boolean satisfiability) and SMT (SAT enriched with arithmetic etc.) work, and how to use them in practice.

These procedures can be used in automatic analysis of software or hardware, in combinatorial optimisation or in search for solutions in operation research.

Content

  • Basics in logic
  • SAT algorithms: DPLL, CDCL
  • BDD (binary decision diagrams) algorithmics
  • SMT (satisfiability modulo theory) algorithmics
  • Lab classes: using a SMT solver

Prerequisites

Basic mathematical logic: Boolean operators, quantifiers
Algorithmics
Programming

Tests

Small practical development work + written final exam

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

The exam is given in english only FR

Calendar

The course exists in the following branches:

  • Curriculum - Master in Computer Science - Semester 9 (this course is given in english only EN)
see the course schedule for 2022-2023

Additional Information

Course ID : WMM9MO46
Course language(s): FR

You can find this course among all other courses.

Bibliography

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

Date of update March 10, 2020

Université Grenoble Alpes