Module Handbook

  • Dynamischer Default-Fachbereich geändert auf INF

Course INF-59-51-K-6

Automated Reasoning (4V+2U, 8.0 LP)

Course Type

SWS Type Course Form CP (Effort) Presence-Time / Self-Study
- K Lecture with exercise classes (V/U) 8.0 CP 156 h
4 V Lecture 56 h
2 U Exercise class (in small groups) 28 h
(4V+2U) 8.0 CP 84 h 156 h

Basedata

SWS 4V+2U
CP, Effort 8.0 CP = 240 h
Position of the semester 1 Sem. in SuSe
Level [6] Master (General)
Language [EN] English
Lecturers
Area of study [INF-ALG] Algorithmics and Deduction
Livecycle-State [NORM] Active

Possible Study achievement

  • Verification of study performance: proof of successful participation in the exercise classes (ungraded)
  • Details of the examination (type, duration, criteria) will be announced at the beginning of the course.

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

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 (informal)

None

Requirements for attendance (formal)

None

References to Course [INF-59-51-K-6]

Module Name Context
[INF-59-51-M-6] Automated Reasoning P: Obligatory 4V+2U, 8.0 LP
Course-Pool Name
[INF-Alg_V-KPOOL-6] Lectures of the teaching area Algorithmics and Deduction