Institute for Computer Languages
Compilers and Languages Group

Automated Reasoning and Program Verification (SS 2015)

Course code: 185.A52
Course acronym: ARV
Course type: VU, 3 ETCS
Lecturer: Laura Kovács

Course organization and calendar:

The course is held blocked between 10-19 March, 2015, as follows:

Lecture Date and time Room Topic Online material
1 Tuesday, March 10, 10:00-11:30 Library E185.1
Argentinierstr. 8, 4th floor
Course introduction
Satisfibility in propositional logic
Slides
2 Wednesday, March 11, 10:00-11:30 Library E185.1 Splitting
Pure atom optimization
Slides
3 Wednesday, March 11, 14:00-15:30 Library E185.1 CNF/Clausal normal form transformation
DPLL
Slides
4 Thursday, March 12, 10:00-11:30 Library E185.1 Running a SAT solver
Satisfiability and Randomization
Slides
5 Thursday, March 12, 14:00-15:30 Library E185.1 Randomized Algorithms for SAT Slides
Thursday, March 12, 21:00 Online Midterm assignment
(see due dates below)
Assignment
6 Tuesday, March 17, 10:00-11:30 Library E185.1 First-order logic
Satisfiability modulo theories (SMT)
Slides
7 Tuesday, March 17, 14:00-15:30 Library E185.1 Theory of rationals
Bound propagation
Slides
No lecture on Wednesday, March 18, 10:00-11:30
8 Wednesday, March 18, 14:00-15:30 Library E185.1 Theory of Equality
Congruence Closure

Congruence Closure and DAGs (optional reading material)
Slides
9 Thursday, March 19, 10:00-11:30 Library E185.1 Theory of Arrays
SMT and Non-Unit Clauses, DPLL(T)
Slides
10 Thursday, March 19, 14:00-15:30 Library E185.1 Combination of Theories Slides
Thursday, March 19, 21:00 Online Final assignment
(see due dates below)
Assignment

Homework:

There will be two homework assignments, handed out online.

The first homework will be handed out online, as a midterm assignmet, on March 12, with due date Tuesday, March 17.

The second homework assignment will be handed out online, as a final assignment, on March 19, with due date Friday, March 27.

You may turn in your homework either personally or via email.

Problem set Handed out on Due on
Midterm assignment March 12, 2015 March 17, 2015
Final assignment March 19, 2015 March 27, 2015

Further Course Information

Course type

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:

Lecture notes:

Lecture notes, that is slides, will be distributed online, at the beginning of each lecture.

Grading and Exam:

Your course grade will be based on your homework assignments.

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

Course Topics:

The tentative list of topics covered by the course is below:
Complang
Laura Kovács
   ARV
   ATCS
   Student-Projects
   Vinter
   Cade-Vampire-Tutorial
   SYNASC-Tutorial
   CATPVS
Sitemap
Faculty of Informatics
Vienna University of Technology
top | HTML 4.01 | last update: 2015-03-19 (Webmaster)