Program Correctness
Faculteit  Science and Engineering 
Jaar  2021/22 
Vakcode  WBCS02405 
Vaknaam  Program Correctness 
Niveau(s)  propedeuse 
Voertaal  Engels 
Periode  semester II a 
ECTS  5 
Rooster  rooster.rug.nl 
Uitgebreide vaknaam  Program Correctness  
Leerdoelen  At the end of the course, the student is able to: 1) derive (small) correct program fragments for problems that are given by a formal specification 2) formally prove the correctness of given program fragments 

Omschrijving  Our society critically relies on software that is errorfree and works as intended. Developing errorfree software can be very difficult, even for experienced programmers and small programs. Although testing can be very useful to detect errors before programs reach users, it is not the case that a program that passes all tests is correct. A failed test can only show that a program is incorrect, but a passed test does not ensure that a program is correct. To prove that a program is correct, we need a much more rigorous tool. This course introduces basic principles of deductive program verification: it uses (Floyd)Hoare logic to formally demonstrate the correctness of (small) imperative programs. The focus is on logical rules for programs with assignments, conditional statements, and loops; using these rules, we can prove that a program that satisfies a given specification. The course introduces the basic principles of Hoare logic, and demonstrate their application to small but representative classes of programs. Special attention is paid to the derivation of efficient search algorithms (like saddleback search). Connections between theory and practice, in the form of tools and frameworks for deductive program verification, are also covered. 

Uren per week  
Onderwijsvorm  Hoorcollege (LC), Werkcollege (T)  
Toetsvorm 
Opdracht (AST), Schriftelijk tentamen (WE)
(Homework 40% and Exam 60%  The final grade must be equal or above 5.75 for students to pass the course.  If the exam is digital, it will be a pass/fail instead of a numerical grade  In case of a reexamination the final grade is the grade obtained during the reexamination. That is, the homework grade does not count at the reexamination.) 

Vaksoort  propedeuse  
Coördinator  prof. dr. J.A. Perez Parra  
Docent(en)  D. Düstegör, PhD. ,prof. dr. J.A. Perez Parra  
Verplichte literatuur 


Entreevoorwaarden  Logic  
Opmerkingen  All CS bachelor courses have limited enrollment:  CS students can always enter each course, regardless of whether the course is mandatory for them or not.  A maximum of only 20 places per course is available for nonCS students. These places are filled on a firstcomefirstserved basis, with priority given to students with a strong CSrelated background (e.g., CS exchange students, AI students, etc.). These students need to meet the course prerequisite requirements as mentioned on Ocasys. Six weeks before the course starts, the 20 students that can join are selected and added to the course. If you enroll after this date, you will be placed on the waiting list. For more info about the enrollment procedure, see https://student.portal.rug.nl/infonet/studenten/fse/programmes/bsccs/general/vakintekeningprocedure#cap 

Opgenomen in 
