Software Verification

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 as reading groups with exercises and plenary discussions.
It can be used for the specialization “Programming, Software Verification, and Logic”
in the MSc computer science. (cf. German site on specializations)

Organization

Until further notice, all meetings will be conducted virtually via Zoom.

Workflow

Work is organized in reading groups of 4-5 students.

  • Each Monday, all students get reading material and exercises to work on.
  • On Thursday, students can synchronize, ask questions to the tutors and get help on the exercises.
  • On Tuesday, students can discuss remaining questions in a plenary discussion with the Professor.

The first plenary discussion (Tuesday, 3rd November ) will be about the detailled course organization and expectations.

Exercise submissions

In addition to the online meetings, students can submit exercise solutions for feedback each Monday. There is no grading/bonus points for these submissions.

Communication

  • Meetings: Until further notice, all meetings will be conducted virtually via Zoom.
  • Written Communication: All written communication (announcements etc.) through Zulip Stream SoSy-20W-SV.
    We are also happy to answer questions through Zulip at any time, so feel free to ask questions there.

Dates

  • Tuesday, 13:00–14:00: Plenary discussion (Prof. Beyer)
  • Thursday, 08:00-10:00: Exercise tutoring (Thomas Lemberger, Martin Spiessl)

First meeting: Tuesday, 3. November, 13:00

Schedule

Below is a preliminary schedule of the course that will be updated over time.

  1. 2020-11-02 Lattices: Handbook on Model Checking, Sect. 16.3.1 Preliminaries
  2. 2020-11-09 CPAs, Constant-Propagation, Reaching Definitions: Handbook on Model Checking, Sect. 16.3.2–16.4.3
  3. 2020-11-16 Bounded Model Checking: Section 2.1 from A Unifying View on SMT-Based Software Verification.pdf
  4. 2020-11-23 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. 2020-11-30 Interpolation / Precision Refinement / CEGAR: siehe sheet05
  6. 2020-12-07 Recap LTL; Observer Automata and Observer-Automaton CPA
  7. 2020-12-14 Implementation of learned concepts
  8. 2020-12-21 Implementation of learned concepts
  9. 2020-01-11 k-Induction
  10. 2020-01-18 Verification Witnesses
  11. 2020-01-25 Test-Case Generation and Symbolic Execution
  12. 2020-02-01 Cooperative Verification
  13. 2020-02-08 No new reading material, but:
  14. 2020-02-11 (Exercise on Thursday) Isabelle Tutorial by Prof. Gidon Ernst

* The chapter from the “Handbook on Model Checking” can be found here

Institut
Institut für Informatik
Dozent:in
Assistent:innen
Kursadministration
Korrektor:in
Kursteilnehmer:innen
53
Anmeldung

Do 01 Okt 2020 00:00 – Mi 31 Mär 2021 23:59

Abmeldung nur bis Mi 31 Mär 2021 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
NameAnmeldung abAnmeldung bisTerminPrüfungsanmeldung
Oral Exam
Di 22 Dez 2020 00:00
Fr 05 Feb 2021 23:55
Mo 15 Feb 2021 08:00 – 16:00
Nicht zur Prüfung angemeldet
Oral Exam II
Mo 15 Feb 2021 00:00
Fr 19 Mär 2021 12:00
Di 23 Mär 2021 13:00 – 16:00
Nicht zur Prüfung angemeldet
Termine
ArtZeitRegulärer RaumNotiz
Plenary discussion
  • Di 13:00–14:00
Virtual
Exercise
  • Do 08:00–10:00
Virtual
Tutorien
8 passende Einträge insgesamt
ArtBezeichnungTutorenRegulärer RaumZeitAnmeldungen abAnmeldungen bisAbmeldungen bisFreie Plätze
reading/exercise group
group01
    online
    • Di 13:00–14:00
    • Do 08:00–10:00
    Di 03 Nov 2020 00:00
    0
    reading/exercise group
    group02
      online
      • Di 13:00–14:00
      • Do 08:00–10:00
      Di 03 Nov 2020 00:00
      0
      reading/exercise group
      group03
        online
        • Di 13:00–14:00
        • Do 08:00–10:00
        Di 03 Nov 2020 00:00
        2
        reading/exercise group
        group04
          online
          • Di 13:00–14:00
          • Do 08:00–10:00
          Di 03 Nov 2020 00:00
          0
          reading/exercise group
          group05
            online
            • Di 13:00–14:00
            • Do 08:00–10:00
            Di 03 Nov 2020 00:00
            2
            reading/exercise group
            group06
              online
              • Di 13:00–14:00
              • Do 08:00–10:00
              Di 03 Nov 2020 00:00
              5
              reading/exercise group
              group07
                online
                • Di 13:00–14:00
                • Do 08:00–10:00
                Di 03 Nov 2020 00:00
                5
                reading/exercise group
                group08
                  online
                  • Di 13:00–14:00
                  • Do 08:00–10:00
                  Di 03 Nov 2020 00:00
                  4
                  8 passende Einträge insgesamt