Description
In this course we address a fundamental question in computer science: How do we specify what program written in an imperative program language does, and more specifically how can we prove that the program does what it is supposed to do. In this lecture we learn how to use predicate logic to specify correctness conditions, and introduce a formal proof system in which we can formally verify behaviour of imperative programs.
Recommended prior courses are Foundations of Computer Science (4031FDCX6), Logic 1 (4031LOGX1) and Logic 2 ( 4032LOGX2) and Concepts of Programming Languages (4032CPL3X).
Course objectives
The main objective of this course is to gain knowledge and experience in the theory of semantics and formal verification of basic imperative programming concepts.
At the end of the course the student will have:
learned to use predicate logic to specify arithmetic relations between program variables,
basic knowledge of the proof theory for the correctness of simple imperative programs,
basic knowledge of the proof theory for the correctness of recursive imperative programs,
learned to apply the proof theory to construct correctness proofs,
learned to show the incorrectness of programs by providing concrete counter-examples,
basic knowledge about meta-theoretical concepts of proof systems like soundness, completeness, en decidability,
experience with computer-assisted proving.
Timetable
In MyTimetable, you can find all course and programme schedules, allowing you to create your personal timetable. Activities for which you have enrolled via MyStudyMap will automatically appear in your timetable.
Additionally, you can easily link MyTimetable to a calendar app on your phone, and schedule changes will be automatically updated in your calendar. You can also choose to receive email notifications about schedule changes. You can enable notifications in Settings after logging in.
Questions? Watch the video, read the instructions, or contact the ISSC helpdesk.
Note: Joint Degree students from Leiden/Delft need to combine information from both the Leiden and Delft MyTimetables to see a complete schedule. This video explains how to do it.
Mode of Instruction
Each week there will be a lecture (2 hours per week), and an exercise class (2 hours per week).
Assessment Method
The final grade will be calculated from the following components:
mid-term exam (20%)
2nd examination (20%)
final exam (60%)
Reading list
Verification of Sequential and Concurrent Programs, Apt, Krzysztof R., de Boer, Frank S., Olderog, Ernst-Rüdiger, Series: Texts in Computer Science. Springer, 3rd edition, ISBN: 978-1-84882-744-8
In this course we follow this book, additional reading material may be provided.
Registration
As a student, you are responsible for enrolling on time through MyStudyMap.
In this short video, you can see step-by-step how to enrol for courses in MyStudyMap.
Extensive information about the operation of MyStudyMap can be found here.
There are two enrolment periods per year:
Enrolment for the fall opens in July
Enrolment for the spring opens in December
See this page for more information about deadlines and enrolling for courses and exams.
Note:
It is mandatory to enrol for all activities of a course that you are going to follow.
Your enrolment is only complete when you submit your course planning in the ‘Ready for enrolment’ tab by clicking ‘Send’.
Not being enrolled for an exam/resit means that you are not allowed to participate in the exam/resit.
Contact
For general enquiries, please contact the Education Coordinator.
Remarks
Software
Starting from the 2024/2025 academic year, the Faculty of Science will use the software distribution platform Academic Software. Through this platform, you can access the software needed for specific courses in your studies. For some software, your laptop must meet certain system requirements, which will be specified with the software. It is important to install the software before the start of the course. More information about the laptop requirements can be found on the student website.