Shortcuts


Top of this page
Description
Lectures
Exercises
Timetable
Calendar
Correspondences
Grading
Material
Prerequisites
Newsgroup tut.ot.ohjtod
Course Catalog

OHJ-2506 Program Verification, 2012 (P1, P2)


Description

The general goal of the course is to learn to use mathematically rigorous methods in software engineering, especially predicate logic and set theory. Learning outcomes are ability to verify parts of programs, algorithms and data structures using logic and set theory. We also study fundamental and practical limitations of the formal methods.

In the course we practise how to do logical calculations which can be little hard in the beginning if the student does not have any previous experience.

In the beginning of the course we repeat some things learned in the course OHJ-2100 Ohjelmistotieteen perustyökaluja (Basic Tools for Software Science) like predicate logic, set theory, and writing state predicates.

The course is valid for post-graduate studies.

Lectures

Lectures are given twice a week, on the 1. period two hours at a time, and on the 2. period the first lecture two hours and at the second lecture one hour.

Exercises

Exercises are obligatory and probably the grades will be determined on the exercises (it depends on the number of participants). That will be decided during the first lectures.

Exercises are given on the 1. period two hours a week and on the 2. period three hours a week. There are no exercises on the first week.

The weekly exercises will be notified on this page:

11
Exercise #
Week
Date
Problems
1
36
6.9.2012
1-6
2
37
13.9.2012
6 from group 1, 7-12 from group 2
3
38
20.9.2012
6 from group 1 as a personal task, 11-12 from group 2, 13-16 from group 3
4
39
27.9.2012
(12 from group 2), 15-16 from group 3, 17-20 from group 4
5
39
4.10.2012
19-20 from group 4, 21-24 from group 5
6
40
11.10.2012
22-24 from group 5, 25-29 from group 6
7
42
25.10.2012
26-29 from group 6, 30-31 from group 7
8
43
1.11.2012
31 from group 7, 32-36 from group 8
9
44
8.11.2012
37-44 from group 9
10
45
15.11.2012
43-44 from group 9, 45-50 from group 10. Please notice that this exercise session begins at 16.05 and ends earlier than usually.
11
46
22.11.2012
44 from group 9, 44,46-50 from group 10. 51 from group 11
12
47
29.11.2012
44 from group 9 (please notice that I fixed it) , 48-50 from group 10. 51 from group 11, and 52-58 from group 12. This is more than we can go through but we go throgh as many as we have time.

A link to the exercises in pdf form. Exercise groups in pdf:

Links are going to be here.
(1-1) (1)
(1-2) (2)
(1-3) (3)
(1-4) (4)
(1-5) (5)
(1-6) (6)
(1-7) (7)
(1-8) (8)
(1-9) (9)
(1-10) (10)
(1-11) (11)
(1-12) (12)

The exercises will be given in the following way:

Be prepared to present your answers. It is better to do less carefully than much "poorly". The grade is not determined directly by the number of presented problems, but by solving only a few of the problems it is not possible to show what you have learned.

Timetable

The lectures begin on 28.8.2011 and the exercises on 6.9.2011

Timetable for period P1

  ma ti ke to pe
8–9          
9–10          
10–11          
11–12          
12–13   Lecture
TC210
  Lecture
TC210
 
13–14      
14–15          
15–16          
16–17       Exercise
TC103
 
17–18        
18–19          

Timetable for period P2

  ma ti ke to pe
8–9          
9–10          
10–11          
11–12          
12–13   Lecture
TC210
  Lecture TC210  
13–14          
14–15          
15–16          
16–17       Exercise
TC103
 
17–18        
18–19        

Calendar


Week 35: 27.8.–2.9.2012. Period P1 begins
  Tu 28.8.2012 Lecture 12–14 TC210
  Th 30.8.2012 Lecture 12–14 TC210
Week 36: 3.9.–9.9.2012
  Tu 4.9.2012 Lecture 12–14 TC210
  Th 6.9.2012 Lecture 12–14 TC210
  Th 6.9.2012 Exercise 1 16–18 TC103
Week 37: 10.9.–16.9.2012
  Tu 11.9.2012 Lecture 12–14 TC210
  Th 13.9.2012 Lecture 12–14 TC210
  Th 13.9.2012 Exercise 2 16–18 TC103
Week 38: 17.9.–23.9.2012
  Tu 18.9.2012 Lecture 12–14 TC210
  Th 20.9.2012 Lecture 12–14 TC210
  Th 20.9.2012 Exercise 3 16–19 TC103
Week 39: 24.9.–30.9.2012
  Tu 25.9.2012 Lecture 12–14 TC210
  Th 27.9.2012 Lecture 12–14 TC210
  Th 27.9.2012 Exercise 4 16–19 TC103
Week 40: 1.10.–7.10.2012
  Tu 2.10.2012 Lecture 12–14 TC210
  Th 4.10.2012 Lecture 12–14 TC210
  Th 4.10.2012 Exercise 5 16–18 TC103
Week 41: 8.10.–14.10.2012
  Tu 9.10.2012 Lecture 12–14 TC210
  Th 11.10.2012 Lecture 12–14 TC210
  Th 11.10.2012 Exercise 6 16–18 TC103
Week 42: 15.10.–21.10.2011
Exam week – no lectures, no exercises
Week 43: 22.10.–28.10.2011. Period P2 begins
  Tu 23.10.2012 Lecture 12–14 TC210
  Th 25.10.2012 Lecture 12–13 TC210
  Th 25.10.2012 Exercise 7 16–19 TC103
Week 44: 29.10.–4.11.2012
  Tu 30.10.2012 Lecture 12–14 TC210
  Th 1.11.2012 Lecture 12–13 TC210
  Th 1.11.2012 Exercise 8 16–19 TC103
Week 45: 5.11.–11.11.2012
  Tu 6.11.2012 Lecture 12–14 TC210
  Th 8.11.2012 Lecture 12–13 TC210
  Th 8.11.2012 Exercise 9 16–19 TC103
Week 46: 12.11.–18.11.2012
  Tu 13.11.2012 Lecture 12–14 TC210
  Th 15.11.2012 Lecture 12–13 TC210
  Th 15.11.2012 Exercise 10 16–19 TC103
Week 47: 19.11.–25.11.2012
  Tu 20.11.2012 Lecture 12–14 TC210
  Th 22.11.2012 Lecture 12–13 TC210
  Th 22.11.2012 Exercise 11 16–19 TC103
Week 48: 26.11.–2.12.2012
  Tu 27.11.2012 Lecture 12–14 TC210
  Th 29.11.2012 Lecture 12–13 TC210
  Th 29.11.2012 Exercise 12 16–19 TC103
Week 49: 3.12.–9.12.2012
  Tu 4.12.2012 Lecture 12–14 TC210
  Th 6.12.2012 Independende Day - no lectures, no exercises

The corresponding former courses

The course is exchangable in both directions with the older courses 8101160 Ohjelmien todistaminen and OHJ-2500 Ohjelmien todistaminen.

Grading

Evaluation criteria for the course are determined in the beginning of the course. The idea is that if there are not too many participants the grading can be determined by the exercises. Otherwise there will be an exam.

Grading will be determined by exercises and therefore there will be no exam.

Material

The English material can be found here

The exercise problems will be delivered in this page, see Exercises.

Possible extra material will also be delivered in this page.

In the course we use the same notations as in course OHJ-2100 Ohjelmistotieteen perustyökaluja (Basic Tools for Software Science). Here are the descriptions of notations in English and in Finnish in PDF format.

Prerequisites

OHJ-2100 Ohjelmistotieteen perustyökaluja (Basic Tools for Software Science).