Bachelor-/Masterseminar Softwareverifikation

Inhalte

In diesem Seminar werden ausgewählte Themen aus dem Bereich Softwareverifikation behandelt. Im Detail beschäftigen wir uns mit Invarianten, insbesondere ihrer Generierung.

Invarianten sind ein zentraler Bestandteil von Softwareverifikation. Sie kennen Invarianten wahrscheinlich in Form von assert-Anweisungen, die Sie in Ihr Programm schreiben und die in der Regel bei der Ausführung überprüft werden. Die Gültigkeit von assert-Anweisungen kann aber auch statisch von Verifikationstools geprüft werden. Neben der Spezifikation von (Sicherheits)eigenschaften werden Invarianten aber auch als Hilfsmittel in der Verifikation genutzt. So benötigen deduktive Verifikationsverfahren z.B. Schleifeninvarianten, um die Korrektheit von Programmen bezüglich einer Eigenschaft zu zeigen. Ebenso kann man die Überapproximation der erreichbaren Programmzustände, die viele Verifikationstools berechnen, als eine Form der Invariante verstehen.

Themen

Themen für Bachelor- und Masterseminar

• CEGIR: Counterexample Guided Invariant Generation
• Computing Invariants for P-solvable Loops
• Dynamically Inferring Likely Invariants
• ICE: Implication CounterExamples for Invariant Generation
• Invariant Generation with Farkas Lemma
• Theorem Prover-based Invariant Synthesis

Themen beschränkt auf das Bachelorseminar

• Abstract Interpretation
• DySy: Dynamic Symbolic Execution for Invariant Inference
• FiB: Squeezing Loop Invariants by Interpolation between Forward/Backward Predicate Transformers
• Inductive Invariant Generation via Abductive Inference
• k-Induction
• The Houdini Algorithm

Organisatorisches

Veranstalter

• Dr. Marie-Christine Jakobs
• Prof. Dr. Dirk Beyer

Bitte kontaktieren Sie bei Fragen Dr. Marie-Christine Jakobs.

Termine

Mi 10-12 Uhr c.t., Oettingenstr. 67, 033

Beginn: Mittwoch, 11.04.2018
Ende: Mittwoch, 11.07.2018

Die Anwesenheit bei allen Terminen ist obligatorisch. Fehlzeiten sind mit ärztlichem Attest (Arbeitnehmerkrankenschein) zu belegen.

Details zum genauen Ablauf folgen Das Seminar besteht aus zwei Teilen, einem Vortrag über Ihr Thema und eine schriftlichen Ausarbeitung Ihres Themas. Vortrag und Ausarbeitung können wahlweise auf Deutsch oder Englisch sein. Aufgrund der Internationalität des Informatikfachs empfehlen wir Ihnen, das Seminar zu nutzen und Ihr Englisch zu üben. Um das Seminar zu bestehen, müssen beide Teile einzeln bestanden werden.

1. Bachelorseminar
   • Vortrag: von 35 Minuten Dauer und anschließender 5-10 minütiger Diskussion
   • Ausarbeitung: 7.000- Zeichen - max. 14.000 Zeichen
2. Masterseminar
   • Vortrag: von 35 Minuten Dauer und anschließender 5-10 minütiger Diskussion
   • Ausarbeitung: 20.000 - max. 30.000 Zeichen (entspricht ca. 7-10 Seiten in der Vorlage, abhängig von Grafiken, Tabellen, etc. ggfs. mehr)

Hörerkreis

Bachelor Informatik
Master Informatik

Vorlagen

Ausarbeitung

Hinweise

Bitte beachten Sie auch die Lehrstuhlregeln und unsere Hinweise zur Anfertigung von Seminararbeiten sowie unsere Schreibtipps.

Anmeldung