Program Verification (Lecture)
Course Type |
Lecture |
---|---|
Instructors | Prof. Dr. Andreas Podelski, Dr. Matthias Heizmann, Christian Schilling |
Lecture |
Tuesday 17:00-18:00 c.t. in building 101-00-036 Wednesday 16:00-18:00 c.t. in building 101-00-036 |
Exercise |
Tuesday 16:00-17:00 s.t. in building 101-00-036 |
Language | English |
Exam |
Oral exam, on September 14 and September 19, building 052, room 00-017 |
Course Catalog |
Program Verification (Lecture) Program Verification (Exercise) |
News
- July 25: There was an error in the slides from July 24 on pp. 16-17 that is now corrected in the non-annotated version.
- July 24: This week we will swap lecture and tutorial. On Tuesday we will have a recap. On Wednesday we will continue, followed by the tutorial.
- July 21: We fixed the dates for the examination (see box above) and published the last exercise sheet.
- July 19: In the final lecture on July 26 we will recapitulate and answer questions. If you already have specific questions, send them to Christian.
- July 18: In the tutorial we discussed the solution for Exercise 3 on Exercise Sheet 11 and did not conclude properly due to time constraints. We added the solution that was presented in the Exercises section.
- July 10: We added some literature on trace abstraction/interpolant automata.
- June 26: Exercise Sheet 8 has been updated (notes in Ex. 1 and Ex. 3, typos in Ex. 4).
- June 2: Exercise 1 on Exercise Sheet 6 now only gives 1 point.
- May 25: Exercise Sheet 5 has been finalized.
- May 11: We removed an exercise from Exercise Sheet 3 because the respective theory was not discussed in the lecture.
- May 11: We moved the deadline for the exercise ranking from Friday 7 p.m. to Sunday 8 p.m. Furthermore, the assignment results will be made available on Monday 9 a.m. (instead of 7 a.m.).
- May 5: We added the exercise ranking form for Exercise Sheet 2 with some delay.
- May 3: We clarified the examination admission requirement.
- April 29: The ranking form for Exercise Sheet 1 has been added.
- April 28: This week the deadline for submitting the exercise rankings was extended to Sunday.
Contents
Often computers are used in embedded, networked, safety critical applications. The cost of failure is high.
In this lecture we introduce the basis of automatic tools for ensuring that a system does not have bad behaviors.
We start with a short introduction to propositional logic and first-order reasoning.
We then go on to establish a setting for the verification of programs whose correctness is specified by a kind of program comments. In this setting, the correctness of the program is reduced to the validity of logical formulas. The validity is proven automatically by a new generation of powerful reasoning engines.
Finally, we connect verification with static analysis methods that have been developed originally in compiler optimization and which are formalized by Patrick and Radhia Cousot's framework of abstract interpretation.
Example of a verification problem. Technical documentation, for example of device driver programs for Windows and Linux operating systems, contains rules that specify the order of certain operations and file accesses. A violation of such a rule can lead to system crashes, deadlocks, unexpected exceptions, or the failure of runtime checks. We can formalize such rules, for example by a finite automaton. Below is a small program for which we would like to know whether it obeys the rule "calls to lock and unlock must alternate" (an attempt to re-acquire an acquired lock or release a released lock will cause a deadlock). The rule can be formalized by the automaton shown next to the program (the red state is the accepting state of the automaton, i.e., the automaton accepts exactly the words that correspond to a bad behavior). Is the program correct? Today tools exist that can answer this question automatically.
|
Example() { 1: do{ lock(); old = new; q = q->next; 2: if (q != NULL){ 3: q->data = new; unlock(); new ++; } 4: } while(new != old); 5: unlock (); return; } |
|
Slides
Slides are found here.
Exercises
Exercise sheet |
Ranking form |
---|---|
Sheet 1 | Ranking form 1 |
Sheet 2 | Ranking form 2 |
Sheet 3 |
Ranking form 3 |
Sheet 4 |
Ranking form 4 |
Sheet 5 Full proof tree |
Ranking form 5 |
Sheet 6 |
Ranking form 6 |
Sheet 7 |
Ranking form 7 |
Sheet 8 Diagram 1, Diagram 2 |
Ranking form 8 |
Sheet 9 |
Ranking form 9 |
Sheet 10 |
Ranking form 10 |
Sheet 11 Solution Ex. 3 |
Ranking form 11 |
Sheet 12 |
- |
Bonus sheet 13 |
- |
If you do not want to use the Google form, you can alternatively send your rankings via email to Christian.
In order to incite active discussions in the exercise group, we will organize the exercise group in a new way. The main novelty lies in the fact that, for each exercise, the solution will be presented by a team of two students.
- Solutions of exercises will be neither corrected nor graded.
- You can only achieve exercise points for presenting solutions in the exercise group.
- Each Wednesday, we will upload an exercise sheet on this website.
- Furthermore, there will be a link to a form in which each student should rank each exercises according to his or her willingness to present the exercise in the next exercise group.
- Until Sunday 20:00 everyone has to submit his or her rankings.
- Over the weekend we will assign (randomly if necessary) two students to each exercise.
- The assignment results will be made available before Monday 9:00.
- The two students that are assigned to an exercise have to coordinate and present a solution together in the exercise group on Tuesday.
- It is not necessary to present a perfect solution, but we expect that you are able to present an approach for finding a solution that we can discuss together.
- We expect that everyone participates actively in the discussion of the solution.
Exam
There will be an oral exam during the examination period. Prerequisite for admission to the exam is an active participation in the exercises. A sufficient criterion for an active participation is that you received 8 exercise points.
Literature
- Almeida, J.B., Frade, M.J., Pinto, J.S., Melo de Sousa, S., Rigorous Software Development - An Introduction to Program Verification, Springer 2011, ISBN 978-0-85729-017-5
- Andrey Rybalchenko: Constraint Solving for Program Verification: Theory and Practice by Example. CAV 2010:57-71
- Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model Checking for People Who Love Automata. CAV 2013