Software Verification

• Prüfungen
  • Main Exam
  • Second Exam

Aktuelles

• Exam

  Second Exam: 2023-10-09 (register until 2023-10-02, see here for how to register)

  Zuletzt verändert: Mi 13 Sep 2023 14:04

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 a hybrid format, including lecturing, reading groups, tutorials, 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

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

Dates

• Wednesday, 10:00-12:00: Plenary discussion (Prof. Dr. Beyer)
• Thursday, 14:15-15:45: Exercise tutoring (Niann-Tzer Li)

First lecture: Wednesday, April 19th, at 10:15 in Amalienstr. 73A, 220
First tutorial: Thursday, April 20th, at 14:15 in HGB, D Z001

Communication

Important announcements are sent via Uni2Work mail to your campus addresses.
Students could use this Zulip stream to discuss exercises.

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. Verification Witnesses
10. Test-Case Generation and Symbolic Execution
11. Cooperative Verification
12. Implementation of learned concepts: Project for implementation of a verifier
    
    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:in

• Niann-Tzer Li

Kursteilnehmer:innen

164

Anmeldung

Fr 10 Mär 2023 10:31

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
Main Exam	Fr 30 Jun 2023 15:43	Di 01 Aug 2023 10:00	Do 03 Aug 2023 10:00 – 12:00	Nicht zur Prüfung angemeldet
Second Exam	Mo 04 Sep 2023 14:00	Mo 02 Okt 2023 15:00	Mo 09 Okt 2023 10:00 – 12:00	Nicht zur Prüfung angemeldet