# 185.A52 Automated Reasoning and Program Verification This course is in all assigned curricula part of the STEOP.\$(function(){PrimeFaces.cw("Tooltip","widget_j_id_21",{id:"j_id_21",showEffect:"fade",hideEffect:"fade",target:"isAllSteop"});});This course is in at least 1 assigned curriculum part of the STEOP.\$(function(){PrimeFaces.cw("Tooltip","widget_j_id_23",{id:"j_id_23",showEffect:"fade",hideEffect:"fade",target:"isAnySteop"});}); 2015S 2014S 2013S 2012S

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

## Properties

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

## Aim of course

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.

## 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;

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

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

Not necessary

## Curricula

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

## Literature

No lecture notes are available.

English