Master Seminar Software Verification (IN2107)

Summer 2013

Corneliu Popeea and Andrey Rybalchenko

News

28.05.2013: Homepage updated with the slides from the students' presentations.
9.04.2013: Homepage updated with details on dates for the seminar and grading (discussed previously during Vorbesprechung).
29.01.2013: First meeting at 10am in 03.09.014.
28.01.2013: Homepage online.

Sylabus

Software verification is a broader and more complex discipline of software engineering whose goal is to assure that software fully satisfies all the expected requirements. We will read and discuss papers on formal methods of software verification.

Dates

First version of the slides: 15th of April.
Final version of the slides and the summary (3-5 pages): the Monday before the presentation days.
Presentation days: 25-26th of April (15:00-18:00), room 03.09.014.

Grading

Grading will be based on:

Preparation phase
Writing a summary (3-5 pages)
Giving a talk, answering questions related to the talk (30-40 minutes)
Active participation during (most of) the talks

Presentation

All participants are expected to give a decent lecture. During and after every lecture there will be (a) discussion(s).

Please prepare enjoyable slides! Use a clean layout and font and include appropriate figures. Feel free to use the blackboard or projector e.g. for highlighting important facts or developing examples.

If you want to use LaTeX for your slides or summary (we encourage you to do so) you can find some useful sources here:

LaTeX-Introduction in 157 minutes (in english)
LaTeX-Introduction Fernuni Hagen (in german):
- LaTeX - Fortgeschrittene Anwendungen
- Verschlungene Anwendungen (Das X-Team: Xtem XEmacs LaTeX 2e AucTeX)
LaTeX-package to prepare slides: Beamer

Your supervisor will be happy to answer questions and provide guidance on how to give a good presentation.

List of topics

Extended static checking for Java - assigned to Lukas Erlacher (pdf)
Mathematizing C++ concurrency - assigned to Salomon Sickert (pdf)
Floyd/Hoare logic - assigned to Thomas Parsch
Hindley-Milner typing - assigned to Navketan Verma
Liquid types - assigned to Manuel Eberl (pdf)

List of summary papers and presentation slides

Extended static checking for Java - assigned to Lukas Erlacher (summary), (slides)
Mathematizing C++ concurrency - assigned to Salomon Sickert (summary), (slides)
Floyd/Hoare logic - assigned to Thomas Parsch (summary), (slides)
Hindley-Milner typing - assigned to Navketan Verma (summary), (slides)
Liquid types - assigned to Manuel Eberl (summary), (slides)