Module Handbook

  • Dynamischer Default-Fachbereich geändert auf INF

Module INF-59-51-M-6

Automated Reasoning (M, 8.0 LP)

Module Identification

Module Number Module Name CP (Effort)
INF-59-51-M-6 Automated Reasoning 8.0 CP (240 h)

Basedata

CP, Effort 8.0 CP = 240 h
Position of the semester 1 Sem. in SuSe
Level [6] Master (General)
Language [EN] English
Module Manager
Lecturers
Area of study [INF-ALG] Algorithmics and Deduction
Reference course of study [INF-88.79-SG] M.Sc. Computer Science
Livecycle-State [NORM] Active

Courses

Type/SWS Course Number Title Choice in
Module-Part
Presence-Time /
Self-Study
SL SL is
required for exa.
PL CP Sem.
4V+2U INF-59-51-K-6
Automated Reasoning
P 84 h 156 h
U-Schein
ja PL1 8.0 SuSe
  • About [INF-59-51-K-6]: Title: "Automated Reasoning"; Presence-Time: 84 h; Self-Study: 156 h
  • About [INF-59-51-K-6]: The study achievement "[U-Schein] proof of successful participation in the exercise classes (ungraded)" must be obtained.
    • It is a prerequisite for the examination for PL1.

Examination achievement PL1

  • Form of examination: oral examination (30-45 Min.)
  • Examination Frequency: each summer semester
  • Examination number: 65951 ("Automated Reasoning")

Evaluation of grades

The grade of the module examination is also the module grade.


Contents

Constraint-solving
  • SAT-solvers: DPLL and CDCL.
  • Satisfiability modulo various logical theories including bitvectors, arrays, integers, reals, rationals, strings,
  • Combining Decision Procedures: Nelson-Oppen Method
  • Reasoning about quantifiers

Applications to program verification

  • Modeling programs in first-order theories
  • Reasoning about programs via constraint-solving problem
  • Synthesis of invariants and ranking function: interpolation, computational learning, IC3, etc.
  • Interactive theorem proving

Competencies / intended learning achievements

After the successful completion of the course, student will be able to:
  • explain the basic automated reasoning problems, and techniques for solving them,
  • explain the strengths and limitations of existing automated reasoning techniques,
  • explain some state-of-the-art automated reasoning tools including Z3,
  • apply the right automated reasoning methods to a given program reasoning problem.

Literature

  • Aaron R. Bradley and Zohar Manna. The Calculus of Computation. Springer, 2007.
  • John Harrison. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, 2009.
  • Daniel Kröning and Ofer Strichman. Decision Procedures: An Algorithmic Point of View. Springer, 2016.

Requirements for attendance of the module (informal)

Modules:

Requirements for attendance of the module (formal)

None

References to Module / Module Number [INF-59-51-M-6]

Course of Study Section Choice/Obligation
[INF-88.79-SG] M.Sc. Computer Science [Core Modules (non specialised)] Computer Science Theory [WP] Compulsory Elective
[INF-88.79-SG] M.Sc. Computer Science [Core Modules (non specialised)] Formal Fundamentals [WP] Compulsory Elective
[INF-88.79-SG] M.Sc. Computer Science [Specialisation] Specialization 1 [WP] Compulsory Elective
Module-Pool Name
[INF-Alg_Ba_V-MPOOL-4] Specialization Bachelor TA Algorithmics and Deduction