Hide menu

Satisfiability Modulo Theory (SMT) and Optimization

2017VT

Status Active - open for registrations
School National Graduate School in Computer Science (CUGS)
Division ESLAB
Owner Ahmed Rezine

  Log in  




Course plan

Approximately 4-6 lectures, 2-3 seminars and 3-4 computer labs

Recommended for

PhD students in Computer Science and related engineering sciences

The course was last given

Never before

Goals

Learning about theories, algorithms and applications of (Optimization subject to) Satisfiability Modulo Theory constraints.

Prerequisites

* Basic notions in logic.
* Good programming skills.

Organization

Lectures, computer labs and seminars

Contents

* Theories: e.g., linear arithmetic of the integers/reals, bitvectors, uninterpreted functions, arrays, strings
* Algorithms: e.g., Davis–Putnam–Logemann–Loveland (DPLL), MaxSMT
* Applications: e.g., scheduling, verification, static analysis, planning

Literature

Research articles

Lecturers

Ahmed Rezine (IDA)

Examiner

Ahmed Rezine (IDA)

Examination

* Lab assignments
* Active participation in research seminars
* Individual project

Credit

6hp

Comments


Page responsible: Director of Graduate Studies