185.A52 Automated Reasoning and Program Verification
This course is in all assigned curricula part of the STEOP.
This course is in at least 1 assigned curriculum part of the STEOP.

2015S, VU, 2.0h, 3.0EC, to be held in blocked form


  • Semester hours: 2.0
  • Credits: 3.0
  • Type: VU Lecture and Exercise

Aim of course


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.


Subject of course

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;

Additional information

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.



Examination modalities

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

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

Course registration

Not necessary


Study CodeObligationSemesterPrecon.Info
066 931 Computational Intelligence Mandatory elective
066 937 Software Engineering & Internet Computing Mandatory elective


No lecture notes are available.