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 Exam	Thursday, April 11, 11am-1pm Library of E185.1
ARV lectures	Wednesdays and Thursdays, 10:00-11:30 and 12:30-14:00, Library of E185.1, Argentinierstrasse 8/4
Introductory ARV lecture	March 6, 10:00-11:30, Library of E185.1
Joint presentation of CompLang lectures	March 6, 13:00-14:00, Lecture room EI 4
First (regular) ARV lecture	March 7, 10:00-11:30, Library of E185.1

---

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:

Problem set	Handed out on	Due on	Solution
Homework assignment	March 14, 2013	March 20, 2013	Solution

Mailing List

We will maintain the following mailing list:
arv13 at complang dot tuwien dot ac dot at
starting from March 7th, 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, that is slides, will be distributed online, at the beginning of each lecture.

Homework:

There will be ONE assignment in the middle of the course period.

This assignmemt will be handed out online after the last lecture on Thursday, March 14.

The assignment will be due on Wednesday, March 20. You may turn in your homework at the beginning of the Wednesday lecture or via email.

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 assignment and final exam scores.

The homework assignment 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);
• satisfiability checking in combination of theories (SMT);
• satisfiability in first-order theories.

Course Outline:

• Lecture 1 (2013-03-06, introduction) --- (slides):
• Motivation and course outline

• Lectures 2 and 3 (2013-03-07) --- (slides):
• Propositional logic and satisfiability
• Satisfiability: splitting and optimisations

• Lectures 4 and 5 (2013-03-13) --- (slides):
• Splitting and optimisations (continued on slides from Lectures 2 and 3)
• CNF, definitional clause form translation, DPLL

• Lectures 6 and 7 (2013-03-14) --- (slides):
• First-order logic and theories - lecture given by Prof. Andrei Voronkov
• Satisfiability modulo theories

• Lectures 8 and 9 (2013-03-20) --- (slides):
• Theory of Equality
• Theory of Arrays
• Reasoning in combination of theories

• Lecture 10 (2013-03-21) --- (slides):
• Theory of Rationals
• Concluding remarks

---