Bachelorseminar: Cooperative Verification

• Prüfungen
  • Seminarnote

Beschreibung

There is no silver bullet for software verification, although there are many tools and techniques with different strengths. Cooperative verification aims to combine the strengths of different verification tools and techniques.

In cooperative verification, different tools cooperate with each other by exchanging information–artifacts–to solve a verification task. This seminar aims to introduce students to cooperative verification.

In this seminar, students will be assigned a topic and will be given a scientific article on that topic. They are expected to read the paper, understand the idea, and research related material on their own. At the end, each student has to write a report and give a presentation explaining what they have learnt.

Organization:

This seminar give 3 ECTS points.
The language of communication is English. Students are expected to communicate with the mentors, give the presentation, and write the report in English.
We will meet every week to discuss the progress and issues faced by students. In this context, students are required to actively participate and present their progress on a weekly basis.
We aim to do the meetings in presence if the situation allows. Otherwise the meetings will be online.

Prerequisite courses:

FSV: Formale Spezifikation und Verifikation

Schedule:

• 28 27 Apr: Introductory meeting to discuss seminar organization
• 21 Jul: Submission of the final report
• 21-23 or 28-30 Jul: Block seminar. Final dates will be announced by the end of June.

Requirements to pass the course:

• Presentation of around 25 minutes
• Written report of 6-8 pages in a given format, without bibliography.

Each student is responsible on their own to follow the rules of good scientific practice. Please ask mentors in case of a doubt. Plagiarism will lead to failing the seminar.

List of topics

1. Hybrid concolic testing:
   - https://www.cs.toronto.edu/~chechik/courses07/csc410/hybrid.pdf
2. Abstraction-driven concolic testing:
   - https://link.springer.com/chapter/10.1007/978-3-662-49122-5_16
3. Cooperative verifier-based testing with CoVeriTest:
   - https://www.doi.org/10.1007/s10009-020-00587-8
4. Collaborative Verification and Testing with Explicit Assumptions:
   - https://doi.org/10.1007/978-3-642-32759-9_13
5. Reducer based construction of conditional model checking:
   - https://doi.org/10.1145/3180155.3180259
6. Decomposing Software Verification into Off-the-Shelf Components: An Application to CEGAR
   - https://www.sosy-lab.org/research/pub/2022-ICSE.Decomposing_Software_Verification_into_Off-the-Shelf-Components.pdf
7. Conditional Testing
   - https://doi.org/10.1007/978-3-030-31784-3_11
8. Witness Validation and Stepwise Testification across Software Verifiers
   - https://doi.org/10.1145/2786805.2786867
9. Correctness Witnesses
   - https://doi.org/10.1145/2950290.2950351
10. A Hybrid Directed Test Suite Augmentation Technique
    - https://ieeexplore.ieee.org/abstract/document/6132963
    - https://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.707.3377&rep=rep1&type=pdf
11. CoVEGI: Cooperative Verification via Externally Generated Invariants
    - https://doi.org/10.1007/978-3-030-71500-7_6

Institut

Institut für Informatik

Dozent:in

• Univ.Prof.Dr. Dirk Beyer

Assistent:in

• Henrik Wachowitz

Kursadministration

• Sudeep Kanav

Kursteilnehmer:innen

6 von 8

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			Mi 27 Jul 2022 14:00 – Fr 29 Jul 2022 16:00	Nicht zur Prüfung angemeldet

Termine

Art	Zeit	Regulärer Raum	Notiz
Seminar Meeting	Mi 27 Apr 2022 16:00–18:00	U139
Weekly Meetings	Mi 16:00–18:00	Raum wird nur Kurs-assoziierten Personen (Teilnehmer:innen, Tutor:innen, Korrektor:innen, etc.) angezeigt