Your course grade will be based on two written homework assignments.
Each homework assignment will count for 50% of the course grade.
The reasoning power that computational logic offers brings new perspectives in the field of program verification. This course is about computational logic, with focus on its applications to program verification.
This course will be divided in two parts:
1. Foundations - where syntax and semantics of first-order logic will be briefly discussed.
2. Automated reasoning - where the focus will be on specialised algorithms for reasoning in various fragments of first-order logics, such as propositional logic, combination of ground theories, and full first-order logic with equality. We will address both the theoretical and practical aspects for using and implementing decisions procedures of various logics.
The tentative list of topics covered by the course is below:
- propositional and first-order logic;
- satisfiability checking in propositional logic (splitting, DPLL, randomized algorithms);
- satisfiability checking in the theory of arithmetic, uninterpreted functions and arrays;
- satisfiability checking the the combination of theories (SMT);
- satisfiability checking in first-order logic;