Frequently Asked Questions
Table of contents
Organization
Q: What are the preliminaries for the course? How should I prepare?
A: We expect all participants to be familiar with first-order predicate logic and the basics of program semantics. The necessary background can, for example, be obtained in the DTU courses 02141 and 02156.
A brief recap of the necessary theoretical background is found on the preliminaries page.
Moreover, we expect fluency in at least one functional or object-oriented programming language.
Q: What should I do before the weekly class on Thursday?
A: There will be homework, published on this webpage, which typically consists of a reading assignment and a few exercises to work on.
Q: Why does the course not cover topic X?
A: Obviously, some choices had to be made to fit the course into the usual 13 week schedule. I would be happy if you let me know why you think that topic X is particularly relevant for program verification (and what should be removed).
Q: What are the learning objectives of the course?
A student who has met the objectives of the course will be able to:
- specify functional correctness properties of imperative programs;
- use automated verification tools to develop formally verified software;
- justify why a program meets its specification based on sound reasoning principles;
- explain the technology stack involved in building automated verification tools;
- compare deductive program verification to other methods aiming at increasing confidence in software correctness;
- encode verification-related decision problems to SMT (satisfiability modulo theories);
- identify potential bottlenecks in existing SMT encodings;
- construct sound methodologies for program verification problems, automate these methodologies via encodings to SMT, and justify the involved design decisions;
- achieve the above goals in a group effort while at the same time maintaining individual accountability; and
- communicate solutions to problems in a clear and precise manner.
Examination
Q: How is this course graded?
A: Your grade is determined by:
- The completeness and quality of group projects (size: 2-3).
- 15% Homework: preparation for projects
- 40% Project A: build a verification tool from scratch
- 60% Project B: design a new verification methodology
- An individual oral exam
- Project presentation (ca. 7min, no slides needed)
- Discussion of projects and course content (ca. 20 min)
Q: Why do the percentages for the projects and homework submissions add up to 115%?
A: For the final grade, we will assume the total percentage is 100%. The additional 15% can be seen as a potential reward for actively working on the homework tasks.
Q: Are there old exams or other material from previous years that I can check out?
A: No, because this is the first time this course is running at DTU.
Reading material
Q: Is there a book on which the course is based?
A: No. All material required for the course will be made available online via this webpage. We will occasionally provide further references but reading them is optional.
Tools and technical difficulties
Q: Which programming language do we have to use in our projects?
A: That is your choice. You can, however, ask us for recommendations :)
Q: I have problems installing one of the tools used in the course.
A: If you have followed all installation instructions step by step and still encounter issues, please contact the teacher as soon as possible.
Q: While working on one of the assignments or projects, I get strange looking errors from one of the tools. What should I do?
A: First, try to reduce your code to a minimal example that fails. If the problem persists, contact the teaching staff with that minimal example and the error.
Other Questions
You are always welcome to ask questions during the lectures. You can, of course, also contact the teacher.