JKU

TNF / INF

team
contact
software
publications
teaching
jobs


GI-Dissertation Award 2020

FMCAD'20 Student Forum Best Student Contribution

SAT'20 Best Presentation Award

GCAI'19 Post and Interaction Award

IJCAI-JAIR 2019 Award

SAT'19 Best Student Paper

CAV'18 Award

HVC'17 Best Paper

ETAPS'17 Test of Time Award

HVC'15 Award

FMCAD'17 Best Paper

CADE'17 Best Paper

BMC

Handbook of Satisfiability

UML@Classroom

UML@Classroom

www.digitaltechnik.org

Special Topics

Satisfiability Modulo Theory

Spezielle Kapitel in Informatik (3KV)

Summer Semester 2016

Organizers

Prof. Armin Biere, Dr. Martina Seidl

Overview

SMT (Satisfiability Modulo Theories) extends logic formulas by theories of various kinds. Examples of such theories are integer arithmetic, bit vectors, arrays, etc. On this basis, many SMT solvers have been implemented which are successfully used in applications like verification, testing, program analysis and scheduling.

This lecture is about algorithms for SMT and their practical implementation.

Organization

First, we will start with three lectures, where an introduction to the topic is given. Then each group (about two people) will select an individual SMT-related topic which they will work on during the semester. In most cases, this will be an implementation project. During the semester there will be multiple individual meetings where feedback is provided. At the end of the semester, the results of the project will be presented to all course participants.

Resources