Verification Techniques (WS 2014/15)

Research Group Computer Science 2

Dept. of Computer Science

Seminar: Verification Techniques
(S2, WS 2014/15)
LuFG Informatik 2

Instructors

Prof. Dr. Jürgen Giesl, Cornelius Aschermann, Florian Frohn, Jera Hensel, Thomas Ströder

Several techniques and methods for program verification will be presented in this seminar.

Times

The seminar will take place at the end of the lecture period. Precise dates will be determined via a doodle poll and then announced. Before the block seminar itself we have the following deadlines

31.10.2012: Contact your supervisor to obtain and discuss the literature.
30.11.2012: Read and understand your primary sources, if needed, obtain more literature. Discuss a rough sketch of your seminar paper with your supervisor.
28.12.2014: Complete your seminar paper (10 pages including title and references) and send it to your supervisor.
19/20.2.2015Bring (enough) copies of your seminar paper to the actual seminar. Also remember to send a digital copy of your final version to Cornelius Aschermann two days before.

Requirements

Your seminar paper should have 10 pages and be written in either English or German. Do not provide an index or table of contents, but attach a list of references. More than 5 spelling or grammar mistakes on a single page will lead to an immediate rejection of your paper, so please use an automated spell checker!

Prerequisites

Participants should have knowledge in program verification or related areas (for example "functional programming", "logic programming", "term rewriting", etc.).

Topics

Date Time Place Topic Supervisor Student

19.2 09:00-09:45 4201b Safety by Interpolation T. Ströder Spinrath, Christopher

19.2 09:45-10:30 4201b Heap Representation with Separation Logic C. Aschermann Kehler, Thibaud

19.2 10:30-11:15 4201b Abstract Regular Tree Model Checking F. Frohn Janson, Tom

19.2 11:15-12:00 4201b Forest Automata for Verification of Heap Manipulation F. Frohn Lekane Nimpa, Junior

19.2 13:30-14:15 4201b Liquid Types C. Aschermann Beaumont, Michael

19.2 14:15-15:00 4201b Finding Hard Bugs in C with Bounded Model Checking C. Aschermann Anwer, Meshkatul

20.2 09:00-09:45 4201b Deciding Bitvector Arithmetic with Abstraction J. Hensel Krueger, Andreas

20.2 09:45-10:30 4201b Termination Analysis using Bitvector Arithmetic J. Hensel Henn, Thomas

20.2 10:30-11:15 4201b Proving Termination of Imperative Programs Using MAX-SMT J. Giesl Karoff, Johannes

20.2 13:30-14:15 4201b Termination Analysis for Concurrent Programs J. Giesl Strothmann, Thies Yannik

20.2 14:15-15:00 4201b Complexity Analysis for Integer Programs J. Giesl Kielmann, Sabrina

Date	Time	Place	Topic	Supervisor	Student
19.2	09:00-09:45	4201b	Safety by Interpolation	T. Ströder	Spinrath, Christopher
19.2	09:45-10:30	4201b	Heap Representation with Separation Logic	C. Aschermann	Kehler, Thibaud
19.2	10:30-11:15	4201b	Abstract Regular Tree Model Checking	F. Frohn	Janson, Tom
19.2	11:15-12:00	4201b	Forest Automata for Verification of Heap Manipulation	F. Frohn	Lekane Nimpa, Junior
19.2	13:30-14:15	4201b	Liquid Types	C. Aschermann	Beaumont, Michael
19.2	14:15-15:00	4201b	Finding Hard Bugs in C with Bounded Model Checking	C. Aschermann	Anwer, Meshkatul
20.2	09:00-09:45	4201b	Deciding Bitvector Arithmetic with Abstraction	J. Hensel	Krueger, Andreas
20.2	09:45-10:30	4201b	Termination Analysis using Bitvector Arithmetic	J. Hensel	Henn, Thomas
20.2	10:30-11:15	4201b	Proving Termination of Imperative Programs Using MAX-SMT	J. Giesl	Karoff, Johannes
20.2	13:30-14:15	4201b	Termination Analysis for Concurrent Programs	J. Giesl	Strothmann, Thies Yannik
20.2	14:15-15:00	4201b	Complexity Analysis for Integer Programs	J. Giesl	Kielmann, Sabrina