Module Import 04IN2033 - Decision Procedures for Verification

Status: Published
Workload6 ECTS = 180 hrs
Credits, Weight6 ECTS, (n.s.)
Language of Instruction German or English
Semester (n.s.)
Duration1 Sem.
M/E Elective
Courses
Course No. Type Name MA/EL Workload Credits Contact Hours Selfstudy Group Size
04IN2033-1 Lecture Decision Procedures for Verification EL 3 ECTS = 90 hrs - 2 hrs/week = 30 hrs 60 hrs 30
04IN2033-2 Exercise Decision Procedures for Verification EL 3 ECTS = 90 hrs - 2 hrs/week = 30 hrs 60 hrs 30
Learning Outcomes

The students know theories which are important in computer science (for instance theories related to data structures) and decision procedures for satisfiability in (fragments of) such theories. They can apply the decision procedures and understand how they can be used e.g. for program verification.

Content

(not specified)

04IN2033-1 - Decision Procedures for Verification

1. Introduction, motivation

2. Preliminaries: Logic

  • Propositional Logic: Resolution, DPLL
  • Predicate Logic: Resolution; Resolution as a decision procedure

3. Logical theories; Decision procedures

  • Equality
  • Theories of real/rational/integer numbers; real/rational/integer arithmetic;

4. Combinations of theories, Combinations of decision procedures

5. SMT: DPLL(T)

6. Applications

  • Decision Procedures for lists and arrays
  • Verification
04IN2033-2 - Decision Procedures for Verification

In the exercises for the lecture "Decision Procedures for Verification" the material presented in the lectures is repeated in order to achieve a thorough understanding. Solutions to exercises related to the topics of the lectures are presented and discussed by the students.

Teaching Methods

Lecture with interactive elements.

Exercise: The students present the results of their work; Discussions.

Prerequisites

Basic knowledge of logic: Propositional logic and predicate logic as taught in the lecture "Logic for computer scientists".

The book of Uwe Schöning "Logik für Informatiker", 5. Auflage. Spektrum Akademischer Verlag, 2000 covers the prerequisites sufficiently.

Examination Methods

Oral or written exam, depending on the number of participants

Weight of the grade in the final grade for Lehramt Gymnasium: 5% corresponding to LP (6:120); for Lehramt Realschule: 10% corresponding to LP (6:60)

Credit Requirements

Voraussetzung für die Vergabe von Leistungspunkten: regelmäßige und qualifizierte Teilnahme

References

(not specified)

04IN2033-1 - Decision Procedures for Verification

Melvin Fitting: First-Order Logic and Automated Theorem Proving. Springer-Verlag, New York, 1996.

Uwe Schöning: Logik für Informatiker. Spektrum Akademischer Verlag, 2000

A. Bradley and Z. Manna: The Calculus of Computation. Decision Procedures with Applications to Verification. Springer 2007.

Daniel Kroening and Ofer Strichman: Decision Procedures An Algorithmic Point of View, Springer 2008.

Use of this Module
  1. unmodified as Elective  -    BSc Computer Science 2017  -    Mandatory elective courses Computer Science  -    Decision Procedures for Verification
  2. unmodified as Elective  -    BSc Computational Visualistics 2017  -    Mandatory elective courses Computer Science  -    Decision Procedures for Verification
  3. unmodified as Elective  -    BSc Computational Visualistics 2017  -    Mandatory elective courses in Computational Visualistics or computer science  -    Decision Procedures for Verification
  4. unmodified as Elective  -    MSc Computer Science 2017  -    Mandatory elective courses in mathematics and theoretical computer science  -    Decision Procedures for Verification
  5. unmodified as Elective  -    MSc Computer Science 2017  -    Mandatory elective courses Computer Science  -    Decision Procedures for Verification
  6. unmodified as Elective  -    MSc Computer Science 2017  -    Major subject computer science  -    Data and Knowledge Engineering  -    Decision Procedures for Verification
  7. unmodified as Elective  -    MSc Computer Science 2017  -    Major subject computer science  -    Software Engineering  -    Decision Procedures for Verification
  8. unmodified as Elective  -    MSc Computational Visualistics 2017  -    Mandatory elective courses Computer Science  -    Decision Procedures for Verification
  9. unmodified as Elective  -    MSc Computational Visualistics 2017  -    Mandatory elective courses in Computational Visualistics or computer science  -    Decision Procedures for Verification
  10. unmodified as Elective  -    MSc Computational Visualistics 2017  -    Mandatory elective courses in theoretical computer science and mathematics  -    Decision Procedures for Verification
  11. unmodified as Elective  -    MSc Computational Visualistics 2017  -    Mandatory elective courses in theoretical computer science and mathematics or natural and social sciences  -    Decision Procedures for Verification
Responsible / Organizational Unit
Sofronie-Stokkermans, Viorica / Institute for Computer Science
Additional Information

(not specified)

Last change
Apr 24, 2018 by Frey, Johannes
Last Change Module
Sep 28, 2018 by Frey, Johannes