Obtaining insight how various problems can be transformed to formulas, and can be solved automatically by computer programs manipulating these formulas. |
|
Many problems, in particular in the area of verification of computer systems, can be expressed as proving that some big formula is always true. In this course we will concentrate on various methods for treating this kind of problems. Not only correctness and completeness of these methods will be considered, also efficiency and usability. In particular we will consider:
- Satisfiability of propositions: resolution and the main ingredients of modern satisfiability provers.
- Satisfiability modulo theories, in particular using linear inequalities, and the underlying simplex algorithm.
- Binary Decision Diagrams as efficient representation of boolean expressions, as the basis of symbolic model checking.
- Unification; resolution on predicates.
- Reasoning modulo equations, term rewriting.
|
|
|
Basic knowledge of logic.
Basic programming skills.
|
|
Written examination plus practical assignment, see website.
Both parts should be at least 5; for the final grade they both count for 50 %.
|
|
|