COURSE OVERVIEW:

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;

The course is held blocked in March, more precisely between 9-20 March 2015, starting with March 10. 

In this period, there will be:

• 1 introductory lecture on Tuesday, March 10, 10:00-12:00, Library E185.1;
• 2-2 lectures on Wednesday and Thursday, March 11 and March 12, 10:00-12:00 and 14:00-16:00, Library E185.1;
• 2-2 lectures on Tuesdya, Wednesday and Thursday, March 17-March 19, 10:00-12:00 and 14:00-16:00, Library E185.1;
• 1 concluding lecture on Friday, March 20, 10:00-12:00, Library E185.1.

The first  homework assignment will be handed out online on March 12, with due date Tuesday, March 17.

The second homework assignment will be handed out online on March 19, with due date Tuesday, March 24.

Your course grade will be based on two written homework assignments.

Each homework assignment will count for 50% of the course grade.