Automated Reasoning (4V+2U, 8.0 LP)
|SWS||Type||Course Form||CP (Effort)||Presence-Time / Self-Study|
|-||K||Lecture with exercise classes (V/U)||8.0 CP||156 h|
|2||U||Exercise class (in small groups)||28 h|
|(4V+2U)||8.0 CP||84 h||156 h|
|CP, Effort||8.0 CP = 240 h|
|Position of the semester||1 Sem. in SuSe|
|Level|| Master (General)|
|Area of study||[INF-ALG] Algorithmics and Deduction|
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.
- 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
- 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.