Institute for Computer Languages
Compilers and Languages Group

Automated Reasoning and Program Verification (Summer 2013)

Course code: 185.A52

Course acronym: ARV

Course type: VU, 3 ETCS

Course news and calendar:

Course is helded blocked between 6-21 March, 2013.
During this period, there will be 2-2 lectures on each Wednesday and Thursday.

ARV lectures

Wednesdays and Thursdays, 10:00-11:30 and 12:30-14:00, Library of E185.1, Argentinierstrasse 8/4

---

Course Schedule

Registration:

Please register to the course via the
CompLang registration system (this link).

Lectures:

Wednesdays and Thursdays,
10:00 - 11:30 and 12:30-14:00,
Library of E185.1, Argentinierstrasse 8/4,
Lecturer: Laura Kovács, office E185.1/04 07A.

The staff is always glad to help you. Whenever you get lost, desire help, or just want to talk, please contact us - don't let yourself fall behind! If you can't come to our office hours, send us email to set up an individual appointment.

Homework:

Number	Problem set	Handed out on	Due on	Solution

Mailing List

We will maintain the following mailing list:
arv13 at complang dot tuwien dot ac dot at
starting from March 6th, 2013.

Course Information

Course type

• Course type: VU (lecture with exercises)
• Lecture: 2 x 45 minutes; 4 lectures/week
• Course credits: 3 ETCS
• Course language: English

Prerequisites:

The course is recommended for master students in Computer Science.

Students are expected to have attended or be familiar with the topics covered by the Formal Methods lectures.

Summary:

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:

• Foundations - where syntax and semantics of first-order logic will be briefly discussed.

• 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.

Lecture notes:

Lecture notes (slides) will be distributed online, at the beginning of each lecture.

Homework:

A problem set is handed out online on each Thursday, at the end of the last Thursday lecture, and is due on Wednesday on the following week. You may turn in your homework to our office or via email.

Model solutions are handed out and discussed during the lectures. The checked problem sets will be returned a week later.

There will be a total of 3 homeworks.

If you have questions about course material or homework problems, please talk to us as soon as possible.

Grading and Exam:

Your course grade will be based on your homework and final exam scores.

Homeworks will count for 30% of the course grade. The final exam will count for 70% of the course grade.

The final exam will take place during the regularly scheduled exam period. You will be allowed to bring one A4-size sheet of hand-written notes to the exam. No other material is allowed.

Course Topics:

The tentative list of topics covered by the course is below:

• propositional and first-order logic;
• satisfiability checking in propositional logic (DPLL, randomized algorithms);
• binary decision diagrams (BDDs);
• satisfiability checking in combination of theories (SMT);
• satisfiability checking in first-order logic;
.

Course Outline:

• Lecture 1 (2013-03-06, introduction):
• Motivation and course outline
• Introduction to propositional logic and satisfiability

• Lecture 2 (2013-03-06):
• Satisfiability: splitting and optimisations

---