Software Verification

• Prüfungen
  • Oral Exam

Aktuelles

• Oral exam

  The oral exam for this lecture will be online and on Tuesday, 2022-02-22, from 13 to 16. Registration is now open and needs to be finished until 2022-02-16, but we appreciate early registration as that simplifies our planning.

  Update: Depending on the number of registrations, we might not fit all participants into the 13:00-16:00 time slot. This means some exams can be at different times on the same day. If you know that you will not attend, please make sure to deregister.

  Zuletzt verändert: Di 01 Feb 2022 13:55

• Lecture will be online

  As discussed in the lecture, most people prefer online sessions, so lecture and exercises will continue via Zoom. There will be the possibility to meet in presence, contact us via Zulip if you are interested.

  Zuletzt verändert: Di 02 Nov 2021 13:44

Beschreibung

Software Verification

This course covers advanced techniques for automatic software verification,
especially techniques belonging to the field of program analysis or software model checking.
The course continues the bachelor course Formal Verification and Specification 1 (FSV 1).
Knowledge from FSV 1 is helpful, but not mandatory.

The course is organized in reversed classroom format as reading groups with exercises and plenary discussions.
This course can be used for the specialization “Programming, Software Verification, and Logic”
in the MSc computer science. (cf. German site on specializations)

Organization

Workflow

Work is organized in reading groups of 4-5 students. There will be weekly exercise sheets, each of which comes with a list of reading material.

• On Friday of the previous week, students get the reading material and exercises to work on (via Uni2Work).
• During the week, students read the material and work on the exercises in their groups. Everyone is responsible on their own to plan enough study time for the lecture - it is not enough to just attend the lecture and exercise slots!
• On Thursday, students can synchronize, ask questions to the tutors and get help on the exercises.
• On Monday of the following week, students can submit exercise solutions for feedback via Uni2Work. There is no grading/bonus points for these submissions.
• On Tuesday of the following week, students can discuss remaining questions in a plenary discussion with the professor. Although there is a 3h slot for the lecture in LSF, this will typically take about 1h. The remaining time can be used to study the next reading material and work on the exercises.

The first plenary discussion (Tuesday, October 19th) will be about the detailed course organization and expectations.

Dates

• Tuesday, 13:00-16:00: Plenary discussion (Prof. Dr. Beyer)
• Thursday, 14:00-16:00: Exercise tutoring (Philipp Wendler, Niann-Tzer Li)

First meeting: Tuesday, October 19th, at 13:00 via Zoom (link will be announced in the room details on Uni2Work)
On Thursday, October 21st will be the first exercise session with an introduction to Jupyter.

We are open for having the lecture and exercise sessions in presence or in a hybrid format if possible. However, in the first three weeks (until November 4th), all meetings will be online via Zoom. Afterwards we may switch to presence or a hybrid format depending on number of participants and feedback from students.

Communication

All written communication will be through Zulip in stream SoSy-21W-SV. Important announcements are also sent via Uni2Work mail to your campus addresses.
We are also happy to answer questions through Zulip at any time, so feel free to ask questions there.

The meetings will first be via Zoom and might happen in presence later on.

Topics

Here is a preliminary schedule of the topics that the course will cover over time:

1. Lattices: Handbook on Model Checking, Sect. 16.3.1 Preliminaries
2. CPAs, Constant-Propagation, Reaching Definitions: Handbook on Model Checking, Sect. 16.3.2–16.4.3
3. Bounded Model Checking: Section 2.1 from A Unifying View on SMT-Based Software Verification.pdf
4. Predicate Abstraction / Predicate Analysis: section 2B (Predicate Abstraction) from Software Model Checking via Large-Block Encoding
   and section 16.4.4 (Predicate Analysis) from Combining Model Checking and Data-Flow Analysis
5. Interpolation / Precision Refinement / CEGAR for Value Analysis
6. Precision Refinement / CEGAR for Predicate Analysis
7. Recap LTL; Observer Automata and Observer-Automaton CPA
8. k-Induction
9. Implementation of learned concepts: Project for implementation of a verifier
10. Verification Witnesses
11. Test-Case Generation and Symbolic Execution
12. Cooperative Verification
    
    The list of reading material for each week is specified on the exercise sheet.

Institut

Institut für Informatik

Dozent:in

• Univ.Prof.Dr. Dirk Beyer

Assistent:innen

• Po-Chun Chien
• Niann-Tzer Li
• Philipp Wendler

Korrektor:innen

• Niann-Tzer Li
• Philipp Wendler

Kursteilnehmer:innen

67

Anmeldung

Mi 29 Sep 2021 00:00 – Do 31 Mär 2022 23:59

Abmeldung nur bis Do 31 Mär 2022 23:59

Material

Das Kursmaterial ist nur für Mitglieder des Kurses einsehbar, also z.B. für Teilnehmer:innen, Tutor:innen, Korrektor:innen und Verwalter:innen.

Prüfungen

Name	Anmeldung ab	Anmeldung bis	Termin	Prüfungsanmeldung
Oral Exam	Di 18 Jan 2022 00:00	Mi 16 Feb 2022 23:59	Di 22 Feb 2022 00:00 – 00:00	Nicht zur Prüfung angemeldet

Termine

Art	Zeit	Regulärer Raum	Notiz
Lecture	Di 13:00–16:00	Raum wird nur Kurs-assoziierten Personen (Teilnehmer:innen, Tutor:innen, Korrektor:innen, etc.) angezeigt
Exercise Course	Do 14:00–16:00	Raum wird nur Kurs-assoziierten Personen (Teilnehmer:innen, Tutor:innen, Korrektor:innen, etc.) angezeigt