Bachelorseminar Tools for Software Verification

• Prüfungen
  • Seminarnote

Beschreibung

In this seminar you will have the opportunity to try out modern tools for automatic program analysis, testing, and verification of software systems.

The tools will be chosen from the participants in software verification competition and testing competition:

• https://sv-comp.sosy-lab.org
• https://test-comp.sosy-lab.org/

Organization

The seminar will be in hybrid mode: in presence and online streaming at the same time.
The language of communication will be English.
This means that the communication with mentors, presentation, and the written report should be in the English language.
In case you cannot do it in English, please contact us by email.

Please note that all the communication with mentors will be in English.

Content and schedule

• Oct 21: We will meet to discuss organizational issues (in presence and online streaming)
• Jan 20: Submission of the final report and presentation draft
• Jan 27-28: Block seminar (hybrid)

Requirements

• Presentation (25 minutes)
• Report: 7000-14000 characters (about 8-10 pages of in LNCS style, without bibliography)
• Practical part: trying out the respective tool on sample programs
• You are responsible to follow the rules of good scientific practice as well as the correct citation (we will discuss this in detail, in case of doubt just ask).

The seminar gives 3 ECTS points.

General Instruction:

Each topic in this seminar is based on a tool.
The tools are chosen from the participants in either software verification or testing competition.
The information about the tools is available on the competition web sites:

• https://sv-comp.sosy-lab.org
• https://test-comp.sosy-lab.org/

The links for more information about the tools, and tool archives to execute the tools are available on the following links:

• https://sv-comp.sosy-lab.org/2021/systems.php
• https://test-comp.sosy-lab.org/2021/systems.php

List of topics:

Tool Archive	References
2LS	Ref. 1, Ref. 2
CBMC	Ref. 1
CPAchecker	Ref. 1, Ref. 2
Dartagnan	Ref. 1, Ref. 2
DIVINE	Ref. 1, Ref. 2
ESBMC-incr, ESBMC-kind	Ref. 1, Ref. 2, Ref. 3, Ref. 4
Frama-C	Ref. 1
Gazer-Theta	Ref. 1
Goblint	Ref. 1, Ref. 2
Korn	Ref. 1
Lazy-CSeq	Ref. 1, Ref. 2
PredatorHP	Ref. 1, Ref. 2
SMACK	Ref. 1, Ref. 2
Symbiotic	Ref. 1, Ref. 2
UAutomizer	Ref. 1, Ref. 2
CoVeriTest	Ref. 1, Ref. 2
FuSeBMC	Ref. 1, Ref. 2
KLEE	Ref. 1, Ref. 2
Legion	Ref. 1
TracerX	Ref. 1, Ref. 2
NonDex	Ref. 1, Ref. 2
Mart	Ref. 1
EvoSuite	Ref. 1, Ref. 2

Institut

Institut für Informatik

Dozierende

• Sudeep Kanav
• Niann-Tzer Li
• Stefan Winter

Kursadministration

• Gidon Ernst

Kursteilnehmer:innen

16 von 20

Zentralanmeldung

Bachelorseminare

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
Seminarnote			Do 21 Okt 2021 00:00 – Fr 28 Jan 2022 00:00	Nicht zur Prüfung angemeldet

Termine

Art	Zeit	Regulärer Raum	Notiz
Kick-Off Meeting	Do 21 Okt 2021 16:00–18:00	Raum wird nur Kurs-assoziierten Personen (Teilnehmer:innen, Tutor:innen, Korrektor:innen, etc.) angezeigt	We will have a hybrid session on 21 Oct: both in presence and streamed online to discuss the organizational matters.
Introduction to Scientific Writing	Do 18 Nov 2021 16:00–18:00	Raum wird nur Kurs-assoziierten Personen (Teilnehmer:innen, Tutor:innen, Korrektor:innen, etc.) angezeigt	We will have an online only session on 18 Nov. Make sure to register with your full name. Attendance is mandatory. The Zoom link is the same as for the kick-off meeting (see “News” on this page).